ForMatUS: Pruebas en Lean del principio del tercio excluso
He añadido a la lista Lógica con Lean el vídeo en el que se comentan 17 pruebas en Lean del principio del tercio excluso 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. 23) Demostrar que -- F ∨ ¬F -- ---------------------------------------------------- import tactic variable (F : Prop) open_locale classical -- 1ª demostración example : F ∨ ¬F := by_contradiction ( assume h1 : ¬(F ∨ ¬F), have h2 : ¬F, from assume h3 : F, have h4 : F ∨ ¬F, from or.inl h3, show false, from h1 h4, have h5 : F ∨ ¬F, from or.inr h2, show false, from h1 h5 ) -- 2ª demostración example : F ∨ ¬F := by_contradiction ( assume h1 : ¬(F ∨ ¬F), have h2 : ¬F, from assume h3 : F, have h4 : F ∨ ¬F, from or.inl h3, show false, from h1 h4, have h5 : F ∨ ¬F, from or.inr h2, h1 h5 ) -- 3ª demostración example : F ∨ ¬F := by_contradiction ( assume h1 : ¬(F ∨ ¬F), have h2 : ¬F, from assume h3 : F, have h4 : F ∨ ¬F, from or.inl h3, show false, from h1 h4, h1 (or.inr h2) ) -- 4ª demostración example : F ∨ ¬F := by_contradiction ( assume h1 : ¬(F ∨ ¬F), have h2 : ¬F, from assume h3 : F, have h4 : F ∨ ¬F, from or.inl h3, h1 h4, h1 (or.inr h2) ) -- 5ª demostración example : F ∨ ¬F := by_contradiction ( assume h1 : ¬(F ∨ ¬F), have h2 : ¬F, from assume h3 : F, h1 (or.inl h3), h1 (or.inr h2) ) -- 6ª demostración example : F ∨ ¬F := by_contradiction ( assume h1 : ¬(F ∨ ¬F), have h2 : ¬F, from λ h3, h1 (or.inl h3), h1 (or.inr h2) ) -- 7ª demostración example : F ∨ ¬F := by_contradiction ( assume h1 : ¬(F ∨ ¬F), h1 (or.inr (λ h3, h1 (or.inl h3))) ) -- 8ª demostración example : F ∨ ¬F := by_contradiction ( λ h1, h1 (or.inr (λ h3, h1 (or.inl h3))) ) -- 9ª demostración example : F ∨ ¬F := -- by library_search em F -- #print axioms em -- 10ª demostración example : F ∨ ¬F := begin by_contra h1, apply h1, right, intro h2, apply h1, left, exact h2, end -- 11ª demostración example : F ∨ ¬F := begin by_contra h1, apply h1, apply or.inr, intro h2, exact h1 (or.inl h2), end -- 12ª demostración example : F ∨ ¬F := begin by_contra h1, apply h1, apply or.inr, exact λ h2, h1 (or.inl h2), end -- 13ª demostración example : F ∨ ¬F := begin by_contra h1, apply h1, exact or.inr (λ h2, h1 (or.inl h2)), end -- 14ª demostración example : F ∨ ¬F := begin by_contra h1, exact h1 (or.inr (λ h2, h1 (or.inl h2))), end -- 15ª demostración example : F ∨ ¬F := by_contra (λ h1, h1 (or.inr (λh2, h1 (or.inl h2)))) -- 16ª demostración example : F ∨ ¬F := begin by_contra h1, apply h1, right, intro h2, apply h1, left, exact h2, end -- 17ª demostración example : F ∨ ¬F := -- by hint by tauto -- 18ª demostración example : F ∨ ¬F := by finish |