ForMatUS: Pruebas en Lean de que la identidad es biyectiva
He añadido a la lista Lógica con Lean el vídeo en el que se comentan pruebas en Lean de que la identidad es biyectiva 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 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 |
import tactic open function variables {X : Type} -- #print injective -- #print surjective -- #print bijective -- ---------------------------------------------------- -- Ej. 1. Demostrar que la identidad es inyectiva. -- ---------------------------------------------------- -- 1ª demostración example : injective (@id X) := begin intros x₁ x₂ h, exact h, end -- 2ª demostración example : injective (@id X) := λ x₁ x₂ h, h -- 3ª demostración example : injective (@id X) := λ x₁ x₂, id -- 4ª demostración example : injective (@id X) := assume x₁ x₂, assume h : id x₁ = id x₂, show x₁ = x₂, from h -- 5ª demostración example : injective (@id X) := --by library_search injective_id -- 6ª demostración example : injective (@id X) := -- by hint by tauto -- 7ª demostración example : injective (@id X) := -- by hint by finish -- ---------------------------------------------------- -- Ej. 2. Demostrar que la identidad es suprayectiva. -- ---------------------------------------------------- -- 1ª demostración example : surjective (@id X) := begin intro x, use x, exact rfl, end -- 2ª demostración example : surjective (@id X) := begin intro x, exact ⟨x, rfl⟩, end -- 3ª demostración example : surjective (@id X) := λ x, ⟨x, rfl⟩ -- 4ª demostración example : surjective (@id X) := assume y, show ∃ x, id x = y, from exists.intro y rfl -- 5ª demostración example : surjective (@id X) := -- by library_search surjective_id -- 6ª demostración example : surjective (@id X) := -- by hint by tauto -- ---------------------------------------------------- -- Ej. 3. Demostrar que la identidad es biyectiva. -- ---------------------------------------------------- -- 1ª demostración example : bijective (@id X) := and.intro injective_id surjective_id -- 2ª demostración example : bijective (@id X) := ⟨injective_id, surjective_id⟩ -- 3ª demostración example : bijective (@id X) := -- by library_search bijective_id |