ForMatUS: Reglas de eliminación del bicondicional en P ↔ Q, P ∨ Q ⊢ P ∧ Q
He añadido a la lista Lógica con Lean el vídeo en el que se comentan 9 pruebas en Lean de
|
1 |
P ↔ Q, 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 |
-- ---------------------------------------------------- -- Ej. 1. (p. 18) Demostrar -- P ↔ Q, P ∨ Q ⊢ P ∧ Q -- ---------------------------------------------------- import tactic variables (P Q : Prop) -- 1ª demostración example (h1 : P ↔ Q) (h2 : P ∨ Q) : P ∧ Q := or.elim h2 ( assume h3 : P, have h4 : P → Q, from iff.elim_left h1, have h5 : Q, from h4 h3, show P ∧ Q, from and.intro h3 h5 ) ( assume h6 : Q, have h7 : Q → P, from iff.elim_right h1, have h8 : P, from h7 h6, show P ∧ Q, from and.intro h8 h6 ) -- 2ª demostración example (h1 : P ↔ Q) (h2 : P ∨ Q) : P ∧ Q := or.elim h2 ( assume h3 : P, have h4 : P → Q := h1.1, have h5 : Q := h4 h3, show P ∧ Q, from ⟨h3, h5⟩ ) ( assume h6 : Q, have h7 : Q → P := h1.2, have h8 : P := h7 h6, show P ∧ Q, from ⟨h8, h6⟩ ) -- 3ª demostración example (h1 : P ↔ Q) (h2 : P ∨ Q) : P ∧ Q := or.elim h2 ( assume h3 : P, show P ∧ Q, from ⟨h3, (h1.1 h3)⟩ ) ( assume h6 : Q, show P ∧ Q, from ⟨h1.2 h6, h6⟩ ) -- 4ª demostración example (h1 : P ↔ Q) (h2 : P ∨ Q) : P ∧ Q := or.elim h2 (λh, ⟨h, (h1.1 h)⟩) (λh, ⟨h1.2 h, h⟩) example (h1 : P ↔ Q) (h2 : P ∨ Q) : P ∧ Q := h2.elim (λh, ⟨h, (h1.1 h)⟩) (λh, ⟨h1.2 h, h⟩) -- 5ª demostración example (h1 : P ↔ Q) (h2 : P ∨ Q) : P ∧ Q := begin cases h2 with h3 h4, { split, { exact h3, }, { apply h1.mp, exact h3, }}, { split, { apply h1.mpr, exact h4, }, { exact h4, }}, end -- 6ª demostración example (h1 : P ↔ Q) (h2 : P ∨ Q) : P ∧ Q := begin cases h2 with h3 h4, { split, { exact h3, }, { rw ← h1, exact h3, }}, { split, { rw h1, exact h4, }, { exact h4, }}, end -- 7ª demostración example (h1 : P ↔ Q) (h2 : P ∨ Q) : P ∧ Q := -- by hint by tauto -- 8ª demostración example (h1 : P ↔ Q) (h2 : P ∨ Q) : P ∧ Q := by finish -- 9ª demostración example (h1 : P ↔ Q) (h2 : P ∨ Q) : P ∧ Q := begin simp [h1] at h2 |-, assumption, end |