(P → Q) ↔ ¬P ∨ Q
Demostrar con Lean4 que
\[ (P → Q) ↔ ¬P ∨ Q \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Tactic variable (P Q : Prop) example : (P → Q) ↔ ¬P ∨ Q := by sorry |
1. Demostración en lenguaje natural
Demostraremos cada una de las implicaciones.
(==>) Supongamos que \(P → Q\). Distinguimos dos subcasos según el valor de \(P\).
Primer subcaso: suponemos \(P\). Entonces, tenemos \(Q\) (porque \(P → Q\)) y. por tanto, \(¬P ∨ Q\).
Segundo subcaso: suponemos \(¬P\). Entonces. tenemos \(¬P ∨ Q\).
(<==) Supongamos que \(¬P ∨ Q\) y \(P\) y tenemos que demostrar \(Q\). Distinguimos dos subcasos según \(¬P ∨ Q\). Primer subcaso: Suponemos \(¬P\). Entonces tenemos una contradicción con \(P\). Segundo subcaso: Suponemos \(Q\), que es lo que tenemos que demostrar.
2. Demostraciones con Lean4
|
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 |
import Mathlib.Tactic variable (P Q : Prop) -- 1ª demostración -- =============== example : (P → Q) ↔ ¬P ∨ Q := by constructor . -- ⊢ (P → Q) → ¬P ∨ Q intro h1 -- h1 : P → Q -- ⊢ ¬P ∨ Q by_cases h2 : P . -- h2 : P right -- ⊢ Q apply h1 -- ⊢ P exact h2 . -- h2 : ¬P left -- ⊢ ¬P exact h2 . -- ⊢ ¬P ∨ Q → P → Q intros h3 h4 -- h3 : ¬P ∨ Q -- h4 : P -- ⊢ Q rcases h3 with h3a | h3b . -- h : ¬P exact absurd h4 h3a . -- h : Q exact h3b done -- 2ª demostración -- =============== example : (P → Q) ↔ ¬P ∨ Q := by constructor . -- ⊢ (P → Q) → ¬P ∨ Q intro h1 -- h1 : P → Q -- ⊢ ¬P ∨ Q by_cases h2: P . -- h2 : P right -- ⊢ Q exact h1 h2 . -- h2 : ¬P left -- ⊢ ¬P exact h2 . -- ⊢ ¬P ∨ Q → P → Q intros h3 h4 -- h3 : ¬P ∨ Q -- h4 : P -- ⊢ Q cases h3 . -- h : ¬P contradiction . -- h : Q assumption done -- 3ª demostración -- =============== example (P Q : Prop) : (P → Q) ↔ ¬P ∨ Q := imp_iff_not_or -- 4ª demostración -- =============== example (P Q : Prop) : (P → Q) ↔ ¬P ∨ Q := by tauto |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 40.
3. Demostraciones con Isabelle/HOL
|
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 |
theory Implicacion_mediante_disyuncion_y_negacion imports Main begin (* 1ª demostración *) lemma "(P ⟶ Q) ⟷ (¬P ∨ Q)" proof assume "P ⟶ Q" show "¬P ∨ Q" proof - have "¬P ∨ P" by (rule excluded_middle) then show "¬P ∨ Q" proof (rule disjE) assume "¬P" then show "¬P ∨ Q" by (rule disjI1) next assume 2: "P" with `P ⟶ Q` have "Q" by (rule mp) then show "¬P ∨ Q" by (rule disjI2) qed qed next assume "¬P ∨ Q" show "P ⟶ Q" proof assume "P" note `¬P ∨ Q` then show "Q" proof (rule disjE) assume "¬P" then show Q using `P` by (rule notE) next assume "Q" then show "Q" by this qed qed qed (* 2ª demostración *) lemma "(P ⟶ Q) ⟷ (¬P ∨ Q)" proof assume "P ⟶ Q" show "¬P ∨ Q" proof - have "¬P ∨ P" by (rule excluded_middle) then show "¬P ∨ Q" proof assume "¬P" then show "¬P ∨ Q" .. next assume 2: "P" with `P ⟶ Q` have "Q" .. then show "¬P ∨ Q" .. qed qed next assume "¬P ∨ Q" show "P ⟶ Q" proof assume "P" note `¬P ∨ Q` then show "Q" proof assume "¬P" then show Q using `P` .. next assume "Q" then show "Q" . qed qed qed (* 3ª demostración *) lemma "(P ⟶ Q) ⟷ (¬P ∨ Q)" by simp end |
