DAO: La semana en Calculemus (del 18 al 23 de abril)
Esta semana he publicado en Calculemus las soluciones de los siguientes problemas:
- 1. Propiedad de monotonía de la intersección
- 2. Propiedad distributiva de la intersección sobre la unión
- 3. Diferencia de diferencia de conjuntos
A continuación se muestran las soluciones.
1. Propiedad de monotonía de la intersección
Demostrar que la intersección es monótona por la izquierda; es decir, si s ⊆ t
, entonces s ∩ u ⊆ t ∩ u
.
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 |
import data.set.basic open set variable {α : Type} variables s t u : set α example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := sorry |
Soluciones con Lean
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 |
import data.set.basic import tactic open set variable {α : Type} variables s t u : set α -- 1ª demostración -- =============== example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := begin rw subset_def, rw inter_def, rw inter_def, dsimp, intros x h1, cases h1 with xs xu, split, { rw subset_def at h, apply h, exact xs, }, { exact xu, }, end -- 2ª demostración -- =============== example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := begin rw [subset_def, inter_def, inter_def], dsimp, rintros x ⟨xs, xu⟩, rw subset_def at h, exact ⟨h x xs, xu⟩, end -- 3ª demostración -- =============== example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := begin simp only [subset_def, inter_def, inter_def], rintros x ⟨xs, xu⟩, rw subset_def at h, exact ⟨h _ xs, xu⟩, end -- 4ª demostración -- =============== example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := begin intros x xsu, exact ⟨h xsu.1, xsu.2⟩, end -- 5ª demostración -- =============== example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := begin rintros x ⟨xs, xu⟩, exact ⟨h xs, xu⟩, end -- 6ª demostración -- =============== example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := -- by library_search inter_subset_inter_left u h -- 7ª demostración -- =============== example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by tidy |
El código de las demostraciones se encuentra en GitHub y puede ejecutarse con el Lean Web editor.
La construcción de las demostraciones se muestra en el siguiente vídeo
Soluciones 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 |
theory Propiedad_de_monotonia_de_la_interseccion imports Main begin (* 1ª solución *) lemma assumes "s ⊆ t" shows "s ∩ u ⊆ t ∩ u" proof (rule subsetI) fix x assume hx: "x ∈ s ∩ u" have xs: "x ∈ s" using hx by (simp only: IntD1) then have xt: "x ∈ t" using assms by (simp only: subset_eq) have xu: "x ∈ u" using hx by (simp only: IntD2) show "x ∈ t ∩ u" using xt xu by (simp only: Int_iff) qed (* 2 solución *) lemma assumes "s ⊆ t" shows "s ∩ u ⊆ t ∩ u" proof fix x assume hx: "x ∈ s ∩ u" have xs: "x ∈ s" using hx by simp then have xt: "x ∈ t" using assms by auto have xu: "x ∈ u" using hx by simp show "x ∈ t ∩ u" using xt xu by simp qed (* 3ª solución *) lemma assumes "s ⊆ t" shows "s ∩ u ⊆ t ∩ u" using assms by auto (* 4ª solución *) lemma "s ⊆ t ⟹ s ∩ u ⊆ t ∩ u" by auto end |
2. Propiedad distributiva de la intersección sobre la unión
Demostrar que s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)
.
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 |
import data.set.basic open set variable {α : Type} variables s t u : set α example : s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) := sorry |
Soluciones con Lean
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 |
import data.set.basic import tactic open set variable {α : Type} variables s t u : set α -- 1ª demostración -- =============== example : s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) := begin intros x hx, cases hx with hxs hxtu, cases hxtu with hxt hxu, { left, split, { exact hxs, }, { exact hxt, }}, { right, split, { exact hxs, }, { exact hxu, }}, end -- 2ª demostración -- =============== example : s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) := begin rintros x ⟨hxs, hxt | hxu⟩, { left, exact ⟨hxs, hxt⟩, }, { right, exact ⟨hxs, hxu⟩, }, end -- 3ª demostración -- =============== example : s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) := begin rintros x ⟨hxs, hxt | hxu⟩, { exact or.inl ⟨hxs, hxt⟩, }, { exact or.inr ⟨hxs, hxu⟩, }, end -- 4ª demostración -- =============== example : s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) := begin intros x hx, by finish, end -- 5ª demostración -- =============== example : s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) := by rw inter_union_distrib_left |
El código de las demostraciones se encuentra en GitHub y puede ejecutarse con el Lean Web editor.
La construcción de las demostraciones se muestra en el siguiente vídeo
Soluciones 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 |
theory Propiedad_semidistributiva_de_la_interseccion_sobre_la_union imports Main begin (* 1ª demostración *) lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)" proof (rule subsetI) fix x assume hx : "x ∈ s ∩ (t ∪ u)" then have xs : "x ∈ s" by (simp only: IntD1) have xtu: "x ∈ t ∪ u" using hx by (simp only: IntD2) then have "x ∈ t ∨ x ∈ u" by (simp only: Un_iff) then show " x ∈ s ∩ t ∪ s ∩ u" proof (rule disjE) assume xt : "x ∈ t" have xst : "x ∈ s ∩ t" using xs xt by (simp only: Int_iff) then show "x ∈ (s ∩ t) ∪ (s ∩ u)" by (simp only: UnI1) next assume xu : "x ∈ u" have xst : "x ∈ s ∩ u" using xs xu by (simp only: Int_iff) then show "x ∈ (s ∩ t) ∪ (s ∩ u)" by (simp only: UnI2) qed qed (* 2ª demostración *) lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)" proof fix x assume hx : "x ∈ s ∩ (t ∪ u)" then have xs : "x ∈ s" by simp have xtu: "x ∈ t ∪ u" using hx by simp then have "x ∈ t ∨ x ∈ u" by simp then show " x ∈ s ∩ t ∪ s ∩ u" proof assume xt : "x ∈ t" have xst : "x ∈ s ∩ t" using xs xt by simp then show "x ∈ (s ∩ t) ∪ (s ∩ u)" by simp next assume xu : "x ∈ u" have xst : "x ∈ s ∩ u" using xs xu by simp then show "x ∈ (s ∩ t) ∪ (s ∩ u)" by simp qed qed (* 3ª demostración *) lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)" proof (rule subsetI) fix x assume hx : "x ∈ s ∩ (t ∪ u)" then have xs : "x ∈ s" by (simp only: IntD1) have xtu: "x ∈ t ∪ u" using hx by (simp only: IntD2) then show " x ∈ s ∩ t ∪ s ∩ u" proof (rule UnE) assume xt : "x ∈ t" have xst : "x ∈ s ∩ t" using xs xt by (simp only: Int_iff) then show "x ∈ (s ∩ t) ∪ (s ∩ u)" by (simp only: UnI1) next assume xu : "x ∈ u" have xst : "x ∈ s ∩ u" using xs xu by (simp only: Int_iff) then show "x ∈ (s ∩ t) ∪ (s ∩ u)" by (simp only: UnI2) qed qed (* 4ª demostración *) lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)" proof fix x assume hx : "x ∈ s ∩ (t ∪ u)" then have xs : "x ∈ s" by simp have xtu: "x ∈ t ∪ u" using hx by simp then show " x ∈ s ∩ t ∪ s ∩ u" proof (rule UnE) assume xt : "x ∈ t" have xst : "x ∈ s ∩ t" using xs xt by simp then show "x ∈ (s ∩ t) ∪ (s ∩ u)" by simp next assume xu : "x ∈ u" have xst : "x ∈ s ∩ u" using xs xu by simp then show "x ∈ (s ∩ t) ∪ (s ∩ u)" by simp qed qed (* 5ª demostración *) lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)" by (simp only: Int_Un_distrib) (* 6ª demostración *) lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)" by auto end |
3. Diferencia de diferencia de conjuntos
Demostrar que (s \ t) \ u ⊆ s \ (t ∪ u)
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 |
import data.set.basic open set variable {α : Type} variables s t u : set α example : (s \ t) \ u ⊆ s \ (t ∪ u) := sorry |
Soluciones con Lean
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 |
import data.set.basic open set variable {α : Type} variables s t u : set α -- 1ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := begin intros x hx, cases hx with hxst hxnu, cases hxst with hxs hxnt, split, { exact hxs }, { dsimp, by_contradiction hxtu, cases hxtu with hxt hxu, { apply hxnt, exact hxt, }, { apply hxnu, exact hxu, }}, end -- 2ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := begin rintros x ⟨⟨hxs, hxnt⟩, hxnu⟩, split, { exact hxs }, { by_contradiction hxtu, cases hxtu with hxt hxu, { exact hxnt hxt, }, { exact hxnu hxu, }}, end -- 3ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := begin rintros x ⟨⟨xs, xnt⟩, xnu⟩, use xs, rintros (xt | xu), { contradiction, }, { contradiction, }, end -- 4ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := begin rintros x ⟨⟨xs, xnt⟩, xnu⟩, use xs, rintros (xt | xu); contradiction, end -- 5ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := begin intros x xstu, simp at *, finish, end -- 6ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := begin intros x xstu, finish, end -- 7ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := by rw diff_diff -- 8ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := by tidy |
El código de las demostraciones se encuentra en GitHub y puede ejecutarse con el Lean Web editor.
La construcción de las demostraciones se muestra en el siguiente vídeo
Soluciones 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 |
theory Diferencia_de_diferencia_de_conjuntos 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 |