ForMatUS: Pruebas en Lean de la reflexividad de la inclusión de conjuntos
He añadido a la lista Lógica con Lean el vídeo en el que se comentan 11 pruebas en Lean de la propiedad reflexiva de de la inclusión de conjuntos usando los estilos declarativos, aplicativos, funcional y automático.
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 |
-- ---------------------------------------------------- -- Ej. 1. Demostrar -- A ⊆ A -- ---------------------------------------------------- import data.set variable U : Type variable x : U variables A B C : set U -- #reduce x ∈ A -- #reduce B ⊆ C -- 1ª demostración example : A ⊆ A := begin intros x h, exact h, end -- 2ª demostración example : A ⊆ A := assume x, assume h : x ∈ A, show x ∈ A, from h -- 3ª demostración example : A ⊆ A := assume x, assume h : x ∈ A, h -- 4ª demostración example : A ⊆ A := assume x, λ h : x ∈ A, h -- 5ª demostración example : A ⊆ A := assume x, id -- 6ª demostración example : A ⊆ A := λ x, id -- 7ª demostración example : A ⊆ A := -- by library_search set.subset.rfl open set -- 8ª demostración example : A ⊆ A := subset.rfl -- 9ª demostración example : A ⊆ A := -- by hint by tauto -- 10ª demostración example : A ⊆ A := by finish -- 11ª demostración example : A ⊆ A := by refl |