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 la propiedad
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 |
-- ---------------------------------------------------- -- Ej. 1. (p. 24) Demostrar -- P → Q ⊢ ¬P ∨ Q -- ---------------------------------------------------- import tactic variables (P Q : Prop) open_locale classical -- 1ª demostración example (h1 : P → Q) : ¬P ∨ Q := have h2 : P ∨ ¬P, from em P, or.elim h2 ( assume h3 : P, have h4 : Q, from h1 h3, show ¬P ∨ Q, from or.inr h4) ( assume h5 : ¬P, show ¬P ∨ Q, from or.inl h5) -- 2ª demostración example (h1 : P → Q) : ¬P ∨ Q := have h2 : P ∨ ¬P, from em P, or.elim h2 ( assume h3 : P, have h4 : Q, from h1 h3, show ¬P ∨ Q, from or.inr h4) ( assume h5 : ¬P, or.inl h5) -- 3ª demostración example (h1 : P → Q) : ¬P ∨ Q := have h2 : P ∨ ¬P, from em P, or.elim h2 ( assume h3 : P, have h4 : Q, from h1 h3, show ¬P ∨ Q, from or.inr h4) ( λ h5, or.inl h5) -- 4ª demostración example (h1 : P → Q) : ¬P ∨ Q := have h2 : P ∨ ¬P, from em P, or.elim h2 ( assume h3 : P, have h4 : Q, from h1 h3, or.inr h4) ( λ h5, or.inl h5) -- 5ª demostración example (h1 : P → Q) : ¬P ∨ Q := have h2 : P ∨ ¬P, from em P, or.elim h2 ( assume h3 : P, or.inr (h1 h3)) ( λ h5, or.inl h5) -- 6ª demostración example (h1 : P → Q) : ¬P ∨ Q := have h2 : P ∨ ¬P, from em P, or.elim h2 ( λ h3, or.inr (h1 h3)) ( λ h5, or.inl h5) -- 7ª demostración example (h1 : P → Q) : ¬P ∨ Q := or.elim (em P) ( λ h3, or.inr (h1 h3)) ( λ h5, or.inl h5) example (h1 : P → Q) : ¬P ∨ Q := (em P).elim ( λ h3, or.inr (h1 h3)) ( λ h5, or.inl h5) -- 8ª demostración example (h1 : P → Q) : ¬P ∨ Q := -- by library_search not_or_of_imp h1 -- 9ª demostración example (h1 : P → Q) : ¬P ∨ Q := if h3 : P then or.inr (h1 h3) else or.inl h3 -- 10ª demostración example (h1 : P → Q) : ¬P ∨ Q := begin by_cases h2 : P, { apply or.inr, exact h1 h2, }, { exact or.inl h2, }, end -- 11ª demostración example (h1 : P → Q) : ¬P ∨ Q := begin by_cases h2 : P, { exact or.inr (h1 h2), }, { exact or.inl h2, }, end -- 12ª demostración example (h1 : P → Q) : ¬P ∨ Q := begin by_cases h2 : P, { right, exact h1 h2, }, { left, exact h2, }, end -- 13ª demostración example (h1 : P → Q) : ¬P ∨ Q := -- by hint by tauto -- 14ª demostración example (h1 : P → Q) : ¬P ∨ Q := -- by hint by finish |