ForMatUS: Pruebas en Lean de que las relaciones reflexivas y euclídeas son de equivalencia
He añadido a la lista Lógica con Lean el vídeo en el que se comentan pruebas en Lean de que si una relación es reflexiva y euclídea, entonces es de equivalencia. Se usan los estilos declarativos, aplicativos y funcional.
A continuación, se muestra el vídeo
|
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 78 79 80 81 82 83 84 85 |
-- ---------------------------------------------------- -- Una relación binaria (≈) es euclídea si -- ∀ {a b c}, a ≈ b → c ≈ b → a ≈ c -- -- El objetivo de esta teoría es demostrar que si una -- relación es reflexiva y euclídea, entonces es de -- equivalencia. -- ---------------------------------------------------- import tactic section parameter {A : Type} parameter (R : A → A → Prop) local infix ≈ := R parameter reflexivaR : reflexive (≈) parameter euclideaR : ∀ {a b c}, a ≈ b → c ≈ b → a ≈ c include reflexivaR euclideaR -- ---------------------------------------------------- -- Ej. 1. Demostrar que las relaciones reflexivas y -- y euclídeas son simétricas. -- ---------------------------------------------------- -- 1ª demostración example : symmetric (≈) := begin intros a b h, exact euclideaR (reflexivaR b) h, end -- 2ª demostración example : symmetric (≈) := λ a b h, euclideaR (reflexivaR b) h -- 3ª demostración lemma simetricaR : symmetric (≈) := assume a b (h1 : a ≈ b), have h2 : b ≈ b, from (reflexivaR b), show b ≈ a, from euclideaR h2 h1 -- ---------------------------------------------------- -- Ej. 2. Demostrar que las relaciones reflexivas y -- y euclídeas son transitivas. -- ---------------------------------------------------- -- 1ª demostración example : transitive (≈) := begin rintros a b c h1 h2, apply euclideaR h1, exact euclideaR (reflexivaR c) h2, end -- 2ª demostración lemma transitivaR : transitive (≈) := λ a b c h1 h2, (euclideaR h1) (euclideaR (reflexivaR c) h2) -- 3ª demostración example : transitive (≈) := assume a b c (h1 : a ≈ b) (h2 : b ≈ c), have h3 : c ≈ b, from euclideaR (reflexivaR c) h2, show a ≈ c, from euclideaR h1 h3 -- ---------------------------------------------------- -- Ej. 3. Demostrar que las relaciones reflexivas y -- y euclídeas son de equivalencia. -- ---------------------------------------------------- -- 1ª demostración example : equivalence (≈) := begin unfold equivalence, exact ⟨reflexivaR, simetricaR, transitivaR⟩, end -- 2ª demostración example : equivalence (≈) := ⟨reflexivaR, simetricaR, transitivaR⟩ end |