La semana en Calculemus (2 de marzo de 2024)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. s \ (t ∪ u) ⊆ (s \ t) \ u
- 2. s ∩ t = t ∩ s
- 3. s ∩ (s ∪ t) = s
- 4. s ∪ (s ∩ t) = s
- 5. (s \ t) ∪ t = s ∪ t
A continuación se muestran las soluciones.
1. s \ (t ∪ u) ⊆ (s \ t) \ u
Demostrar con Lean4 que
\[ s \setminus (t ∪ u) ⊆ (s \setminus t) \setminus u \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t u : Set α) example : s \ (t ∪ u) ⊆ (s \ t) \ u := by sorry |
1. Demostración en lenguaje natural
Sea \(x ∈ s \setminus (t ∪ u)\). Entonces,
\begin{align}
&x ∈ s \tag{1} \\
&x ∉ t ∪ u \tag{2} \\
\end{align}
Tenemos que demostrar que \(x ∈ (s \setminus t) \setminus u\); es decir, que se verifican las relaciones
\begin{align}
&x ∈ s \setminus t \tag{3} \\
&x ∉ u \tag{4}
\end{align}
Para demostrar (3) tenemos que demostrar las relaciones
\begin{align}
&x ∈ s \tag{5} \\
&x ∉ t \tag{6}
\end{align}
La (5) se tiene por la (1). Para demostrar la (6), supongamos que \(x ∈ t\); entonces, \(x ∈ t ∪ u\), en contracción con (2). Para demostrar la (4), supongamos que \(x ∈ u\); entonces, \(x ∈ t ∪ u\), en contracción con (2).
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 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 |
import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t u : Set α) -- 1ª demostración -- =============== example : s \ (t ∪ u) ⊆ (s \ t) \ u := by intros x hx -- x : α -- hx : x ∈ s \ (t ∪ u) -- ⊢ x ∈ (s \ t) \ u constructor . -- ⊢ x ∈ s \ t constructor . -- ⊢ x ∈ s exact hx.1 . -- ⊢ ¬x ∈ t intro xt -- xt : x ∈ t -- ⊢ False apply hx.2 -- ⊢ x ∈ t ∪ u left -- ⊢ x ∈ t exact xt . -- ⊢ ¬x ∈ u intro xu -- xu : x ∈ u -- ⊢ False apply hx.2 -- ⊢ x ∈ t ∪ u right -- ⊢ x ∈ u exact xu -- 2ª demostración -- =============== example : s \ (t ∪ u) ⊆ (s \ t) \ u := by rintro x ⟨xs, xntu⟩ -- x : α -- xs : x ∈ s -- xntu : ¬x ∈ t ∪ u -- ⊢ x ∈ (s \ t) \ u constructor . -- ⊢ x ∈ s \ t constructor . -- ⊢ x ∈ s exact xs . -- ¬x ∈ t intro xt -- xt : x ∈ t -- ⊢ False exact xntu (Or.inl xt) . -- ⊢ ¬x ∈ u intro xu -- xu : x ∈ u -- ⊢ False exact xntu (Or.inr xu) -- 2ª demostración -- =============== example : s \ (t ∪ u) ⊆ (s \ t) \ u := fun _ ⟨xs, xntu⟩ ↦ ⟨⟨xs, fun xt ↦ xntu (Or.inl xt)⟩, fun xu ↦ xntu (Or.inr xu)⟩ -- 4ª demostración -- =============== example : s \ (t ∪ u) ⊆ (s \ t) \ u := by rintro x ⟨xs, xntu⟩ -- x : α -- xs : x ∈ s -- xntu : ¬x ∈ t ∪ u -- ⊢ x ∈ (s \ t) \ u aesop -- 5ª demostración -- =============== example : s \ (t ∪ u) ⊆ (s \ t) \ u := by intro ; aesop -- 6ª demostración -- =============== example : s \ (t ∪ u) ⊆ (s \ t) \ u := by rw [diff_diff] -- Lema usado -- ========== -- #check (diff_diff : (s \ t) \ u = s \ (t ∪ u)) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
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 |
theory Diferencia_de_diferencia_de_conjuntos_2 imports Main begin (* 1ª demostración *) lemma "(s - t) - u ⊆ s - (t ∪ u)" proof (rule subsetI) fix x assume hx : "x ∈ (s - t) - u" then show "x ∈ s - (t ∪ u)" proof (rule DiffE) assume xst : "x ∈ s - t" assume xnu : "x ∉ u" note xst then show "x ∈ s - (t ∪ u)" proof (rule DiffE) assume xs : "x ∈ s" assume xnt : "x ∉ t" have xntu : "x ∉ t ∪ u" proof (rule notI) assume xtu : "x ∈ t ∪ u" then show False proof (rule UnE) assume xt : "x ∈ t" with xnt show False by (rule notE) next assume xu : "x ∈ u" with xnu show False by (rule notE) qed qed show "x ∈ s - (t ∪ u)" using xs xntu by (rule DiffI) qed qed qed (* 2ª demostración *) lemma "(s - t) - u ⊆ s - (t ∪ u)" proof fix x assume hx : "x ∈ (s - t) - u" then have xst : "x ∈ (s - t)" by simp then have xs : "x ∈ s" by simp have xnt : "x ∉ t" using xst by simp have xnu : "x ∉ u" using hx by simp have xntu : "x ∉ t ∪ u" using xnt xnu by simp then show "x ∈ s - (t ∪ u)" using xs by simp qed (* 3ª demostración *) lemma "(s - t) - u ⊆ s - (t ∪ u)" proof fix x assume "x ∈ (s - t) - u" then show "x ∈ s - (t ∪ u)" by simp qed (* 4ª demostración *) lemma "(s - t) - u ⊆ s - (t ∪ u)" by auto end |
2. s ∩ t = t ∩ s
Demostrar con Lean4 que
\[ s ∩ t = t ∩ s \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t : Set α) example : s ∩ t = t ∩ s := by sorry |
1. Demostración en lenguaje natural
Tenemos que demostrar que
\[ (∀ x)[x ∈ s ∩ t ↔ x ∈ t ∩ s] \]
Demostratemos la equivalencia por la doble implicación.
Sea \(x ∈ s ∩ t\). Entonces, se tiene
\begin{align}
&x ∈ s \tag{1} \\
&x ∈ t \tag{2}
\end{align}
Luego \(x ∈ t ∩ s\) (por (2) y (1)).
La segunda implicación se demuestra análogamente.
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 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 |
import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t : Set α) -- 1ª demostración -- =============== example : s ∩ t = t ∩ s := by ext x -- x : α -- ⊢ x ∈ s ∩ t ↔ x ∈ t ∩ s simp only [mem_inter_iff] -- ⊢ x ∈ s ∧ x ∈ t ↔ x ∈ t ∧ x ∈ s constructor . -- ⊢ x ∈ s ∧ x ∈ t → x ∈ t ∧ x ∈ s intro h -- h : x ∈ s ∧ x ∈ t -- ⊢ x ∈ t ∧ x ∈ s constructor . -- ⊢ x ∈ t exact h.2 . -- ⊢ x ∈ s exact h.1 . -- ⊢ x ∈ t ∧ x ∈ s → x ∈ s ∧ x ∈ t intro h -- h : x ∈ t ∧ x ∈ s -- ⊢ x ∈ s ∧ x ∈ t constructor . -- ⊢ x ∈ s exact h.2 . -- ⊢ x ∈ t exact h.1 -- 2ª demostración -- =============== example : s ∩ t = t ∩ s := by ext -- x : α -- ⊢ x ∈ s ∩ t ↔ x ∈ t ∩ s simp only [mem_inter_iff] -- ⊢ x ∈ s ∧ x ∈ t ↔ x ∈ t ∧ x ∈ s exact ⟨fun h ↦ ⟨h.2, h.1⟩, fun h ↦ ⟨h.2, h.1⟩⟩ -- 3ª demostración -- =============== example : s ∩ t = t ∩ s := by ext -- x : α -- ⊢ x ∈ s ∩ t ↔ x ∈ t ∩ s exact ⟨fun h ↦ ⟨h.2, h.1⟩, fun h ↦ ⟨h.2, h.1⟩⟩ -- 4ª demostración -- =============== example : s ∩ t = t ∩ s := by ext x -- x : α -- ⊢ x ∈ s ∩ t ↔ x ∈ t ∩ s simp only [mem_inter_iff] -- ⊢ x ∈ s ∧ x ∈ t ↔ x ∈ t ∧ x ∈ s constructor . -- ⊢ x ∈ s ∧ x ∈ t → x ∈ t ∧ x ∈ s rintro ⟨xs, xt⟩ -- xs : x ∈ s -- xt : x ∈ t -- ⊢ x ∈ t ∧ x ∈ s exact ⟨xt, xs⟩ . -- ⊢ x ∈ t ∧ x ∈ s → x ∈ s ∧ x ∈ t rintro ⟨xt, xs⟩ -- xt : x ∈ t -- xs : x ∈ s -- ⊢ x ∈ s ∧ x ∈ t exact ⟨xs, xt⟩ -- 5ª demostración -- =============== example : s ∩ t = t ∩ s := by ext x -- x : α -- ⊢ x ∈ s ∩ t ↔ x ∈ t ∩ s simp only [mem_inter_iff] -- ⊢ x ∈ s ∧ x ∈ t ↔ x ∈ t ∧ x ∈ s simp only [And.comm] -- 6ª demostración -- =============== example : s ∩ t = t ∩ s := ext (fun _ ↦ And.comm) -- 7ª demostración -- =============== example : s ∩ t = t ∩ s := by ext ; simp [And.comm] -- 8ª demostración -- =============== example : s ∩ t = t ∩ s := inter_comm s t -- Lemas usados -- ============ -- variable (x : α) -- variable (a b : Prop) -- #check (And.comm : a ∧ b ↔ b ∧ a) -- #check (inter_comm s t : s ∩ t = t ∩ s) -- #check (mem_inter_iff x s t : x ∈ s ∩ t ↔ x ∈ s ∧ x ∈ t) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
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 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 |
theory Conmutatividad_de_la_interseccion imports Main begin (* 1ª demostración *) lemma "s ∩ t = t ∩ s" proof (rule set_eqI) fix x show "x ∈ s ∩ t ⟷ x ∈ t ∩ s" proof (rule iffI) assume h : "x ∈ s ∩ t" then have xs : "x ∈ s" by (simp only: IntD1) have xt : "x ∈ t" using h by (simp only: IntD2) then show "x ∈ t ∩ s" using xs by (rule IntI) next assume h : "x ∈ t ∩ s" then have xt : "x ∈ t" by (simp only: IntD1) have xs : "x ∈ s" using h by (simp only: IntD2) then show "x ∈ s ∩ t" using xt by (rule IntI) qed qed (* 2ª demostración *) lemma "s ∩ t = t ∩ s" proof (rule set_eqI) fix x show "x ∈ s ∩ t ⟷ x ∈ t ∩ s" proof assume h : "x ∈ s ∩ t" then have xs : "x ∈ s" by simp have xt : "x ∈ t" using h by simp then show "x ∈ t ∩ s" using xs by simp next assume h : "x ∈ t ∩ s" then have xt : "x ∈ t" by simp have xs : "x ∈ s" using h by simp then show "x ∈ s ∩ t" using xt by simp qed qed (* 3ª demostración *) lemma "s ∩ t = t ∩ s" proof (rule equalityI) show "s ∩ t ⊆ t ∩ s" proof (rule subsetI) fix x assume h : "x ∈ s ∩ t" then have xs : "x ∈ s" by (simp only: IntD1) have xt : "x ∈ t" using h by (simp only: IntD2) then show "x ∈ t ∩ s" using xs by (rule IntI) qed next show "t ∩ s ⊆ s ∩ t" proof (rule subsetI) fix x assume h : "x ∈ t ∩ s" then have xt : "x ∈ t" by (simp only: IntD1) have xs : "x ∈ s" using h by (simp only: IntD2) then show "x ∈ s ∩ t" using xt by (rule IntI) qed qed (* 4ª demostración *) lemma "s ∩ t = t ∩ s" proof show "s ∩ t ⊆ t ∩ s" proof fix x assume h : "x ∈ s ∩ t" then have xs : "x ∈ s" by simp have xt : "x ∈ t" using h by simp then show "x ∈ t ∩ s" using xs by simp qed next show "t ∩ s ⊆ s ∩ t" proof fix x assume h : "x ∈ t ∩ s" then have xt : "x ∈ t" by simp have xs : "x ∈ s" using h by simp then show "x ∈ s ∩ t" using xt by simp qed qed (* 5ª demostración *) lemma "s ∩ t = t ∩ s" proof show "s ∩ t ⊆ t ∩ s" proof fix x assume "x ∈ s ∩ t" then show "x ∈ t ∩ s" by simp qed next show "t ∩ s ⊆ s ∩ t" proof fix x assume "x ∈ t ∩ s" then show "x ∈ s ∩ t" by simp qed qed (* 6ª demostración *) lemma "s ∩ t = t ∩ s" by (fact Int_commute) (* 7ª demostración *) lemma "s ∩ t = t ∩ s" by (fact inf_commute) (* 8ª demostración *) lemma "s ∩ t = t ∩ s" by auto end |
3. s ∩ (s ∪ t) = s
Demostrar con Lean4 que
\[ s ∩ (s ∪ t) = s \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable {α : Type} variable (s t : Set α) example : s ∩ (s ∪ t) = s := by sorry |
1. Demostración en lenguaje natural
Tenemos que demostrar que
\[ (∀ x)[x ∈ s ∩ (s ∪ t) ↔ x ∈ s] \]
y lo haremos demostrando las dos implicaciones.
(⟹) Sea \(x ∈ s ∩ (s ∪ t)\). Entonces, \(x ∈ s\).
(⟸) Sea \(x ∈ s\). Entonces, \(x ∈ s ∪ t\) y, por tanto, \(x ∈ s ∩ (s ∪ t)\).
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 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 |
import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable {α : Type} variable (s t : Set α) -- 1ª demostración -- =============== example : s ∩ (s ∪ t) = s := by ext x -- x : α -- ⊢ x ∈ s ∩ (s ∪ t) ↔ x ∈ s constructor . -- ⊢ x ∈ s ∩ (s ∪ t) → x ∈ s intros h -- h : x ∈ s ∩ (s ∪ t) -- ⊢ x ∈ s exact h.1 . -- ⊢ x ∈ s → x ∈ s ∩ (s ∪ t) intro xs -- xs : x ∈ s -- ⊢ x ∈ s ∩ (s ∪ t) constructor . -- ⊢ x ∈ s exact xs . -- ⊢ x ∈ s ∪ t left -- ⊢ x ∈ s exact xs -- 2ª demostración -- =============== example : s ∩ (s ∪ t) = s := by ext x -- x : α -- ⊢ x ∈ s ∩ (s ∪ t) ↔ x ∈ s constructor . -- ⊢ x ∈ s ∩ (s ∪ t) → x ∈ s intro h -- h : x ∈ s ∩ (s ∪ t) -- ⊢ x ∈ s exact h.1 . -- ⊢ x ∈ s → x ∈ s ∩ (s ∪ t) intro xs -- xs : x ∈ s -- ⊢ x ∈ s ∩ (s ∪ t) constructor . -- ⊢ x ∈ s exact xs . -- ⊢ x ∈ s ∪ t exact (Or.inl xs) -- 3ª demostración -- =============== example : s ∩ (s ∪ t) = s := by ext -- x : α -- ⊢ x ∈ s ∩ (s ∪ t) ↔ x ∈ s exact ⟨fun h ↦ h.1, fun xs ↦ ⟨xs, Or.inl xs⟩⟩ -- 4ª demostración -- =============== example : s ∩ (s ∪ t) = s := by ext -- x : α -- ⊢ x ∈ s ∩ (s ∪ t) ↔ x ∈ s exact ⟨And.left, fun xs ↦ ⟨xs, Or.inl xs⟩⟩ -- 5ª demostración -- =============== example : s ∩ (s ∪ t) = s := by ext x -- x : α -- ⊢ x ∈ s ∩ (s ∪ t) ↔ x ∈ s constructor . -- ⊢ x ∈ s ∩ (s ∪ t) → x ∈ s rintro ⟨xs, -⟩ -- xs : x ∈ s -- ⊢ x ∈ s exact xs . -- ⊢ x ∈ s → x ∈ s ∩ (s ∪ t) intro xs -- xs : x ∈ s -- ⊢ x ∈ s ∩ (s ∪ t) use xs -- ⊢ x ∈ s ∪ t left -- ⊢ x ∈ s exact xs -- 6ª demostración -- =============== example : s ∩ (s ∪ t) = s := by apply subset_antisymm . -- ⊢ s ∩ (s ∪ t) ⊆ s rintro x ⟨hxs, -⟩ -- x : α -- hxs : x ∈ s -- ⊢ x ∈ s exact hxs . -- ⊢ s ⊆ s ∩ (s ∪ t) intros x hxs -- x : α -- hxs : x ∈ s -- ⊢ x ∈ s ∩ (s ∪ t) exact ⟨hxs, Or.inl hxs⟩ -- 7ª demostración -- =============== example : s ∩ (s ∪ t) = s := inf_sup_self -- 8ª demostración -- =============== example : s ∩ (s ∪ t) = s := by aesop -- Lemas usados -- ============ -- variable (a b : Prop) -- #check (And.left : a ∧ b → a) -- #check (Or.inl : a → a ∨ b) -- #check (inf_sup_self : s ∩ (s ∪ t) = s) -- #check (subset_antisymm : s ⊆ t → t ⊆ s → s = t) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
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 |
theory Interseccion_con_su_union imports Main begin (* 1ª demostración *) lemma "s ∩ (s ∪ t) = s" proof (rule equalityI) show "s ∩ (s ∪ t) ⊆ s" proof (rule subsetI) fix x assume "x ∈ s ∩ (s ∪ t)" then show "x ∈ s" by (simp only: IntD1) qed next show "s ⊆ s ∩ (s ∪ t)" proof (rule subsetI) fix x assume "x ∈ s" then have "x ∈ s ∪ t" by (simp only: UnI1) with ‹x ∈ s› show "x ∈ s ∩ (s ∪ t)" by (rule IntI) qed qed (* 2ª demostración *) lemma "s ∩ (s ∪ t) = s" proof show "s ∩ (s ∪ t) ⊆ s" proof fix x assume "x ∈ s ∩ (s ∪ t)" then show "x ∈ s" by simp qed next show "s ⊆ s ∩ (s ∪ t)" proof fix x assume "x ∈ s" then have "x ∈ s ∪ t" by simp then show "x ∈ s ∩ (s ∪ t)" using ‹x ∈ s› by simp qed qed (* 3ª demostración *) lemma "s ∩ (s ∪ t) = s" by (fact Un_Int_eq) (* 4ª demostración *) lemma "s ∩ (s ∪ t) = s" by auto |
4. s ∪ (s ∩ t) = s
Demostrar con Lean4 que
\[ s ∪ (s ∩ t) = s \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t : Set α) example : s ∪ (s ∩ t) = s := by sorry |
1. Demostración en lenguaje natural
Tenemos que demostrar que
\[ (∀ x)[x ∈ s ∪ (s ∩ t) ↔ x ∈ s] \]
y lo haremos demostrando las dos implicaciones.
(⟹) Sea \(x ∈ s ∪ (s ∩ t)\). Entonces, \(x ∈ s\) ó \(x ∈ s ∩ t\). En ambos casos, \(x ∈ s\).
(⟸) Sea \(x ∈ s\). Entonces, \(x ∈ s ∩ t\) y, por tanto, \(x ∈ s ∪ (s ∩ t)\).
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 |
import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t : Set α) -- 1ª demostración -- =============== example : s ∪ (s ∩ t) = s := by ext x -- x : α -- ⊢ x ∈ s ∪ (s ∩ t) ↔ x ∈ s constructor . -- ⊢ x ∈ s ∪ (s ∩ t) → x ∈ s intro hx -- hx : x ∈ s ∪ (s ∩ t) -- ⊢ x ∈ s rcases hx with (xs | xst) . -- xs : x ∈ s exact xs . -- xst : x ∈ s ∩ t exact xst.1 . -- ⊢ x ∈ s → x ∈ s ∪ (s ∩ t) intro xs -- xs : x ∈ s -- ⊢ x ∈ s ∪ (s ∩ t) left -- ⊢ x ∈ s exact xs -- 2ª demostración -- =============== example : s ∪ (s ∩ t) = s := by ext x -- x : α -- ⊢ x ∈ s ∪ s ∩ t ↔ x ∈ s exact ⟨fun hx ↦ Or.elim hx id And.left, fun xs ↦ Or.inl xs⟩ -- 3ª demostración -- =============== example : s ∪ (s ∩ t) = s := by ext x -- x : α -- ⊢ x ∈ s ∪ (s ∩ t) ↔ x ∈ s constructor . -- ⊢ x ∈ s ∪ (s ∩ t) → x ∈ s rintro (xs | ⟨xs, -⟩) <;> -- xs : x ∈ s -- ⊢ x ∈ s exact xs . -- ⊢ x ∈ s → x ∈ s ∪ (s ∩ t) intro xs -- xs : x ∈ s -- ⊢ x ∈ s ∪ s ∩ t left -- ⊢ x ∈ s exact xs -- 4ª demostración -- =============== example : s ∪ (s ∩ t) = s := sup_inf_self -- Lemas usados -- ============ -- variable (a b c : Prop) -- #check (And.left : a ∧ b → a) -- #check (Or.elim : a ∨ b → (a → c) → (b → c) → c) -- #check (sup_inf_self : s ∪ (s ∩ t) = s) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
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 |
theory Union_con_su_interseccion imports Main begin (* 1ª demostración *) lemma "s ∪ (s ∩ t) = s" proof (rule equalityI) show "s ∪ (s ∩ t) ⊆ s" proof (rule subsetI) fix x assume "x ∈ s ∪ (s ∩ t)" then show "x ∈ s" proof assume "x ∈ s" then show "x ∈ s" by this next assume "x ∈ s ∩ t" then show "x ∈ s" by (simp only: IntD1) qed qed next show "s ⊆ s ∪ (s ∩ t)" proof (rule subsetI) fix x assume "x ∈ s" then show "x ∈ s ∪ (s ∩ t)" by (simp only: UnI1) qed qed (* 2ª demostración *) lemma "s ∪ (s ∩ t) = s" proof show "s ∪ s ∩ t ⊆ s" proof fix x assume "x ∈ s ∪ (s ∩ t)" then show "x ∈ s" proof assume "x ∈ s" then show "x ∈ s" by this next assume "x ∈ s ∩ t" then show "x ∈ s" by simp qed qed next show "s ⊆ s ∪ (s ∩ t)" proof fix x assume "x ∈ s" then show "x ∈ s ∪ (s ∩ t)" by simp qed qed (* 3ª demostración *) lemma "s ∪ (s ∩ t) = s" by auto end |
5. (s \ t) ∪ t = s ∪ t
Demostrar con Lean4 que
\[ (s \setminus t) ∪ t = s ∪ t \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t : Set α) example : (s \\setminus t) ∪ t = s ∪ t := by sorry |
1. Demostración en lenguaje natural
Tenemos que demostrar que
\[ (∀ x)[x ∈ (s \setminus t) ∪ t ↔ x ∈ s ∪ t] \]
y lo demostraremos por la siguiente cadena de equivalencias:
\begin{align}
x ∈ (s \setminus t) ∪ t
&↔ x ∈ (s \setminus t) ∨ (x ∈ t) \\
&↔ (x ∈ s ∧ x ∉ t) ∨ x ∈ t \\
&↔ (x ∈ s ∨ x ∈ t) ∧ (x ∉ t ∨ x ∈ t) \\
&↔ x ∈ s ∨ x ∈ t \\
&↔ x ∈ s ∪ t
\end{align}
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 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 Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t : Set α) -- 1ª demostración -- =============== example : (s \ t) ∪ t = s ∪ t := by ext x -- x : α -- ⊢ x ∈ (s \ t) ∪ t ↔ x ∈ s ∪ t calc x ∈ (s \ t) ∪ t ↔ x ∈ s \ t ∨ x ∈ t := mem_union x (s \ t) t _ ↔ (x ∈ s ∧ x ∉ t) ∨ x ∈ t := by simp only [mem_diff x] _ ↔ (x ∈ s ∨ x ∈ t) ∧ (x ∉ t ∨ x ∈ t) := and_or_right _ ↔ (x ∈ s ∨ x ∈ t) ∧ True := by simp only [em' (x ∈ t)] _ ↔ x ∈ s ∨ x ∈ t := and_true_iff (x ∈ s ∨ x ∈ t) _ ↔ x ∈ s ∪ t := (mem_union x s t).symm -- 2ª demostración -- =============== example : (s \ t) ∪ t = s ∪ t := by ext x -- x : α -- ⊢ x ∈ (s \ t) ∪ t ↔ x ∈ s ∪ t constructor . -- ⊢ x ∈ (s \ t) ∪ t → x ∈ s ∪ t intro hx -- hx : x ∈ (s \ t) ∪ t -- ⊢ x ∈ s ∪ t rcases hx with (xst | xt) . -- xst : x ∈ s \ t -- ⊢ x ∈ s ∪ t left -- ⊢ x ∈ s exact xst.1 . -- xt : x ∈ t -- ⊢ x ∈ s ∪ t right -- ⊢ x ∈ t exact xt . -- ⊢ x ∈ s ∪ t → x ∈ (s \ t) ∪ t by_cases h : x ∈ t . -- h : x ∈ t intro _xst -- _xst : x ∈ s ∪ t right -- ⊢ x ∈ t exact h . -- ⊢ x ∈ s ∪ t → x ∈ (s \ t) ∪ t intro hx -- hx : x ∈ s ∪ t -- ⊢ x ∈ (s \ t) ∪ t rcases hx with (xs | xt) . -- xs : x ∈ s left -- ⊢ x ∈ s \ t constructor . -- ⊢ x ∈ s exact xs . -- ⊢ ¬x ∈ t exact h . -- xt : x ∈ t right -- ⊢ x ∈ t exact xt -- 3ª demostración -- =============== example : (s \ t) ∪ t = s ∪ t := by ext x -- x : α -- ⊢ x ∈ (s \ t) ∪ t ↔ x ∈ s ∪ t constructor . -- ⊢ x ∈ (s \ t) ∪ t → x ∈ s ∪ t rintro (⟨xs, -⟩ | xt) . -- xs : x ∈ s -- ⊢ x ∈ s ∪ t left -- ⊢ x ∈ s exact xs . -- xt : x ∈ t -- ⊢ x ∈ s ∪ t right -- ⊢ x ∈ t exact xt . -- ⊢ x ∈ s ∪ t → x ∈ (s \ t) ∪ t by_cases h : x ∈ t . -- h : x ∈ t intro _xst -- _xst : x ∈ s ∪ t -- ⊢ x ∈ (s \ t) ∪ t right -- ⊢ x ∈ t exact h . -- ⊢ x ∈ s ∪ t → x ∈ (s \ t) ∪ t rintro (xs | xt) . -- xs : x ∈ s -- ⊢ x ∈ (s \ t) ∪ t left -- ⊢ x ∈ s \ t exact ⟨xs, h⟩ . -- xt : x ∈ t -- ⊢ x ∈ (s \ t) ∪ t right -- ⊢ x ∈ t exact xt -- 4ª demostración -- =============== example : (s \ t) ∪ t = s ∪ t := diff_union_self -- 5ª demostración -- =============== example : (s \ t) ∪ t = s ∪ t := by ext -- x : α -- ⊢ x ∈ s \ t ∪ t ↔ x ∈ s ∪ t simp -- 6ª demostración -- =============== example : (s \ t) ∪ t = s ∪ t := by simp -- Lemas usados -- ============ -- variable (a b c : Prop) -- variable (x : α) -- #check (and_or_right : (a ∧ b) ∨ c ↔ (a ∨ c) ∧ (b ∨ c)) -- #check (and_true_iff a : a ∧ True ↔ a) -- #check (diff_union_self : (s \ t) ∪ t = s ∪ t) -- #check (em' a : ¬a ∨ a) -- #check (mem_diff x : x ∈ s \ t ↔ x ∈ s ∧ x ∉ t) -- #check (mem_union x s t : x ∈ s ∪ t ↔ x ∈ s ∨ x ∈ t) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
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 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 |
theory Union_con_su_diferencia imports Main begin (* 1ª demostración *) lemma "(s - t) ∪ t = s ∪ t" proof (rule equalityI) show "(s - t) ∪ t ⊆ s ∪ t" proof (rule subsetI) fix x assume "x ∈ (s - t) ∪ t" then show "x ∈ s ∪ t" proof (rule UnE) assume "x ∈ s - t" then have "x ∈ s" by (simp only: DiffD1) then show "x ∈ s ∪ t" by (simp only: UnI1) next assume "x ∈ t" then show "x ∈ s ∪ t" by (simp only: UnI2) qed qed next show "s ∪ t ⊆ (s - t) ∪ t" proof (rule subsetI) fix x assume "x ∈ s ∪ t" then show "x ∈ (s - t) ∪ t" proof (rule UnE) assume "x ∈ s" show "x ∈ (s - t) ∪ t" proof (cases ‹x ∈ t›) assume "x ∈ t" then show "x ∈ (s - t) ∪ t" by (simp only: UnI2) next assume "x ∉ t" with ‹x ∈ s› have "x ∈ s - t" by (rule DiffI) then show "x ∈ (s - t) ∪ t" by (simp only: UnI1) qed next assume "x ∈ t" then show "x ∈ (s - t) ∪ t" by (simp only: UnI2) qed qed qed (* 2ª demostración *) lemma "(s - t) ∪ t = s ∪ t" proof show "(s - t) ∪ t ⊆ s ∪ t" proof fix x assume "x ∈ (s - t) ∪ t" then show "x ∈ s ∪ t" proof assume "x ∈ s - t" then have "x ∈ s" by simp then show "x ∈ s ∪ t" by simp next assume "x ∈ t" then show "x ∈ s ∪ t" by simp qed qed next show "s ∪ t ⊆ (s - t) ∪ t" proof fix x assume "x ∈ s ∪ t" then show "x ∈ (s - t) ∪ t" proof assume "x ∈ s" show "x ∈ (s - t) ∪ t" proof assume "x ∉ t" with ‹x ∈ s› show "x ∈ s - t" by simp qed next assume "x ∈ t" then show "x ∈ (s - t) ∪ t" by simp qed qed qed (* 3ª demostración *) lemma "(s - t) ∪ t = s ∪ t" by (fact Un_Diff_cancel2) (* 4ª demostración *) lemma "(s - t) ∪ t = s ∪ t" by auto end |