ForMatUS: Pruebas en Lean de ∃x∃y P(x,y) ↔ ∃y∃x P(x,y)
He añadido a la lista Lógica con Lean el vídeo en el que se comentan pruebas en Lean de la propiedad
1 |
∃x∃y P(x,y) ↔ ∃y∃x P(x,y) |
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 |
import tactic section variable {U : Type} variable {P : U -> U -> Prop} -- ------------------------------------------------------ -- Ej. 1. Demostrar que -- ∃x∃yP(x,y) → ∃y∃xP(x,y) -- ------------------------------------------------------ -- 1ª demostración example : (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) := assume h1 : ∃ x, ∃ y, P x y, exists.elim h1 ( assume x₀ (h2 : ∃ y, P x₀ y), exists.elim h2 ( assume y₀ (h3 : P x₀ y₀), have h4 : ∃ x, P x y₀, from exists.intro x₀ h3, show ∃ y, ∃ x, P x y, from exists.intro y₀ h4)) -- 2ª demostración example : (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) := assume ⟨x₀, y₀, (h1 : P x₀ y₀)⟩, have h2 : ∃ x, P x y₀, from ⟨x₀, h1⟩, show (∃ y, ∃ x, P x y), from ⟨y₀, h2⟩ -- 3ª demostración example : (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) := assume ⟨x₀, y₀, (h1 : P x₀ y₀)⟩, show (∃ y, ∃ x, P x y), from ⟨y₀, ⟨x₀, h1⟩⟩ -- 4ª demostración example : (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) := assume ⟨x₀, y₀, (h1 : P x₀ y₀)⟩, show (∃ y, ∃ x, P x y), from ⟨y₀, x₀, h1⟩ -- 5ª demostración example : (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) := assume ⟨x₀, y₀, (h1 : P x₀ y₀)⟩, ⟨y₀, x₀, h1⟩ -- 6ª demostración example : (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) := λ ⟨x₀, y₀, h1⟩, ⟨y₀, x₀, h1⟩ -- 7ª demostración example : (∃ x y, P x y) → (∃ y x, P x y) := -- by library_search exists_comm.mp -- 8ª demostración example : (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) := begin intro h1, cases h1 with x₀ h2, cases h2 with y₀ h3, use y₀, use x₀, exact h3, end -- 9ª demostración example : (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) := begin intro h1, cases h1 with x₀ h2, cases h2 with y₀ h3, use [y₀, x₀], exact h3, end -- 10ª demostración example : (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) := begin intro h1, rcases h1 with ⟨x₀, y₀, h2⟩, use [y₀, x₀], exact h2, end -- 11ª demostración example : (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) := begin intro h1, rcases h1 with ⟨x₀, y₀, h2⟩, exact ⟨y₀, x₀, h2⟩, end -- 12ª demostración example : (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) := begin rintro ⟨x₀, y₀, h2⟩, exact ⟨y₀, x₀, h2⟩, end -- 13ª demostración example : (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) := -- by hint by tauto -- 14ª demostración lemma aux : (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) := by finish -- ------------------------------------------------------ -- Ej. 2. Demostrar que -- ∃x∃yP(x,y) ↔ ∃y∃xP(x,y) -- ------------------------------------------------------ -- 1ª demostración example : (∃ x y, P x y) ↔ (∃ y x, P x y) := iff.intro aux aux -- 2ª demostración example : (∃ x y, P x y) ↔ (∃ y x, P x y) := ⟨aux, aux⟩ -- 3ª demostración example : (∃ x y, P x y) ↔ (∃ y x, P x y) := -- by library_search exists_comm -- 4ª demostración example : (∃ x y, P x y) ↔ (∃ y x, P x y) := -- by hint by tauto end |