(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 \ 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 |
