ForMatUS: Pruebas en Lean de P ∧ Q ↔ Q ∧ P
He añadido a la lista Lógica con Lean el vídeo en el que se comentan 13 pruebas en Lean de
|
1 |
P ∧ Q ↔ Q ∧ P |
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 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 |
-- ---------------------------------------------------- -- Ej. 1. (p. 17) Demostrar -- P ∧ Q ↔ Q ∧ P -- ---------------------------------------------------- import tactic variables (P Q : Prop) -- 1ª demostración example : P ∧ Q ↔ Q ∧ P := iff.intro ( assume h1 : P ∧ Q, have h2 : P, from and.elim_left h1, have h3 : Q, from and.elim_right h1, show Q ∧ P, from and.intro h3 h2) ( assume h4 : Q ∧ P, have h5 : Q, from and.elim_left h4, have h6 : P, from and.elim_right h4, show P ∧ Q, from and.intro h6 h5) -- 2ª demostración example : P ∧ Q ↔ Q ∧ P := iff.intro ( assume h1 : P ∧ Q, have h2 : P, from h1.1, have h3 : Q, from h1.2, show Q ∧ P, from and.intro h3 h2) ( assume h4 : Q ∧ P, have h5 : Q, from h4.1, have h6 : P, from h4.2, show P ∧ Q, from and.intro h6 h5) -- 3ª demostración example : P ∧ Q ↔ Q ∧ P := iff.intro ( assume h1 : P ∧ Q, have h2 : P := h1.1, have h3 : Q := h1.2, show Q ∧ P, from and.intro h3 h2) ( assume h4 : Q ∧ P, have h5 : Q := h4.1, have h6 : P := h4.2, show P ∧ Q, from and.intro h6 h5) -- 4ª demostración example : P ∧ Q ↔ Q ∧ P := iff.intro ( assume h1 : P ∧ Q, show Q ∧ P, from and.intro h1.2 h1.1) ( assume h4 : Q ∧ P, show P ∧ Q, from and.intro h4.2 h4.1) -- 5ª demostración example : P ∧ Q ↔ Q ∧ P := iff.intro ( assume h1 : P ∧ Q, and.intro h1.2 h1.1) ( assume h4 : Q ∧ P, and.intro h4.2 h4.1) -- 6ª demostración example : P ∧ Q ↔ Q ∧ P := iff.intro ( assume h1 : P ∧ Q, ⟨h1.2, h1.1⟩) ( assume h4 : Q ∧ P, ⟨h4.2, h4.1⟩) -- 7ª demostración example : P ∧ Q ↔ Q ∧ P := iff.intro (λ h, ⟨h.2, h.1⟩) (λ h, ⟨h.2, h.1⟩) -- 8ª demostración example : P ∧ Q ↔ Q ∧ P := iff.intro (λ ⟨hP, hQ⟩, ⟨hQ, hP⟩) (λ ⟨hQ, hP⟩, ⟨hP, hQ⟩) -- 9ª demostración lemma aux : P ∧ Q → Q ∧ P := λ h, ⟨h.2, h.1⟩ example : P ∧ Q ↔ Q ∧ P := iff.intro (aux P Q) (aux Q P) -- 10ª demostración example : P ∧ Q ↔ Q ∧ P := -- by library_search and.comm -- 11ª demostración example : P ∧ Q ↔ Q ∧ P := begin split, { intro h1, cases h1 with h2 h3, split, { exact h3, }, { exact h2, }}, { intro h4, cases h4 with h5 h6, split, { exact h6, }, { exact h5, }}, end -- 12ª demostración example : P ∧ Q ↔ Q ∧ P := begin split, { rintro ⟨h2, h3⟩, split, { exact h3, }, { exact h2, }}, { rintro ⟨h5, h6⟩, split, { exact h6, }, { exact h5, }}, end -- 13ª demostración example : P ∧ Q ↔ Q ∧ P := begin constructor, { rintro ⟨h2, h3⟩, constructor, { exact h3, }, { exact h2, }}, { rintro ⟨h5, h6⟩, constructor, { exact h6, }, { exact h5, }}, end -- 14ª demostración example : P ∧ Q ↔ Q ∧ P := -- by hint by tauto -- 15ª demostración example : P ∧ Q ↔ Q ∧ P := by finish |