ForMatUS: Pruebas en Lean de ¬P ∨ Q ⊢ P → Q
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 ⊢ P → Q |
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 159 160 161 162 163 164 |
-- Prueba de ¬P ∨ Q ⊢ P → Q -- ======================== -- ---------------------------------------------------- -- Ej. 1. (p. 15) Demostrar -- ¬P ∨ Q ⊢ P → Q -- ---------------------------------------------------- import tactic variables (P Q : Prop) -- 1ª demostración example (h1 : ¬P ∨ Q) : P → Q := assume h2 : P, or.elim h1 ( assume h3 : ¬P, have h4 : false, from h3 h2, show Q, from false.elim h4) ( assume h5 : Q, show Q, from h5) -- 2ª demostración example (h1 : ¬P ∨ Q) : P → Q := assume h2 : P, or.elim h1 ( assume h3 : ¬P, have h4 : false, from h3 h2, show Q, from false.elim h4) ( assume h5 : Q, h5) -- 3ª demostración example (h1 : ¬P ∨ Q) : P → Q := assume h2 : P, or.elim h1 ( assume h3 : ¬P, have h4 : false, from h3 h2, show Q, from false.elim h4) ( λ h5, h5) -- 4ª demostración example (h1 : ¬P ∨ Q) : P → Q := assume h2 : P, or.elim h1 ( assume h3 : ¬P, have h4 : false, from h3 h2, show Q, from false.elim h4) id -- 5ª demostración example (h1 : ¬P ∨ Q) : P → Q := assume h2 : P, or.elim h1 ( assume h3 : ¬P, show Q, from false.elim (h3 h2)) id -- 6ª demostración example (h1 : ¬P ∨ Q) : P → Q := assume h2 : P, or.elim h1 ( assume h3 : ¬P, false.elim (h3 h2)) id -- 7ª demostración example (h1 : ¬P ∨ Q) : P → Q := assume h2 : P, or.elim h1 ( λ h3, false.elim (h3 h2)) id -- 8ª demostración example (h1 : ¬P ∨ Q) : P → Q := λ h2, or.elim h1 (λ h3, false.elim (h3 h2)) id example (h1 : ¬P ∨ Q) : P → Q := λ h2, h1.elim (λ h3, false.elim (h3 h2)) id example (h1 : ¬P ∨ Q) : P → Q := λ h2, h1.elim (λ h3, (h3 h2).elim) id -- 9ª demostración example (h1 : ¬P ∨ Q) : P → Q := -- by library_search imp_iff_not_or.mpr h1 -- 10ª demostración example (h1 : ¬P ∨ Q) : P → Q := begin intro h2, cases h1 with h3 h4, { apply false.rec, exact h3 h2, }, { exact h4, }, end -- 11ª demostración example (h1 : ¬P ∨ Q) : P → Q := begin intro h2, cases h1 with h3 h4, { exact false.elim (h3 h2), }, { exact h4, }, end -- 12ª demostración example (h1 : ¬P ∨ Q) : P → Q := begin intro h2, cases h1 with h3 h4, { exfalso, exact h3 h2, }, { exact h4, }, end -- 13ª demostración example (h1 : ¬P ∨ Q) : P → Q := -- by hint by tauto -- 14ª demostración example (h1 : ¬P ∨ Q) : P → Q := by finish |