Pertenencia a su propia clase de equivalencia
Este ejercicio es el 3º de una serie cuyo objetivo es demostrar que el tipo de las particiones de un conjunto X
es isomorfo al tipo de las relaciones de equivalencia sobre X
.
Los anteriores son
1. Igualdad de bloques de una partición cuando tienen elementos comunes.
2. Pertenencia a bloques de una partición con elementos comunes.
En este empezamos con las relaciones de equivalencia, que están definidas en Lean por:
1 2 3 4 |
reflexive R := ∀ (x : A), R x x symmetric R := ∀ ⦃x y : A⦄, R x y → R y x transitive R := ∀ ⦃x y z : A⦄, R x y → R y z → R x z equivalence R := reflexive R ∧ symmetric R ∧ transitive R |
donde A
un tipo y R: A → A → Prop
es una relación binaria en A
.
Además, en Lean se puede definir la clase de equivalencia de un elemento a
respecto de una relación de equivalencia R
por
1 2 |
def clase (a : A) := {b : A | R b a} |
Demostrar que cada elemento pertenece a su clase de equivalencia.
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 11 12 13 |
import tactic variable {A : Type} variable (R : A → A → Prop) def clase (a : A) := {b : A | R b a} example {hR : equivalence R} (a : A) : a ∈ clase R a := sorry |
[expand title=»Soluciones con Lean»]
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 |
import tactic variable {A : Type} variable (R : A → A → Prop) def clase (a : A) := {b : A | R b a} -- Se usará el siguiente lema auxiliar lemma pertenece_clase_syss {a b : A} : b ∈ clase R a ↔ R b a := by refl -- 1ª demostración example {hR : equivalence R} (a : A) : a ∈ clase R a := begin rw pertenece_clase_syss, suffices h : reflexive R, { exact h a, }, { rcases hR with ⟨h2, -, -⟩, exact h2, }, end -- 1ª demostración example {hR : equivalence R} (a : A) : a ∈ clase R a := begin rw pertenece_clase_syss, suffices h : reflexive R, { exact h a, }, { exact hR.1, }, end -- 3ª demostración example {hR : equivalence R} (a : A) : a ∈ clase R a := begin rw pertenece_clase_syss, rcases hR with ⟨hrefl, -, -⟩, exact hrefl a, end -- 4ª demostración example {hR : equivalence R} (a : A) : a ∈ clase R a := begin obtain ⟨hrefl, -, -⟩ := hR, rw pertenece_clase_syss, apply hrefl, end -- 5ª demostración example {hR : equivalence R} (a : A) : a ∈ clase R a := begin rw pertenece_clase_syss, apply hR.1, end -- 6ª demostración lemma pertenece_clase_propia {hR : equivalence R} (a : A) : a ∈ clase R a := (pertenece_clase_syss R).mpr (hR.1 a) |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]