Unión con su intersección
Demostrar que
s ∪ (s ∩ t) = s
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 : set α example : s ∪ (s ∩ t) = s := sorry |
Conmutatividad de la intersección
Demostrar que
s ∩ t = t ∩ s
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 = t ∩ s := sorry |
Notas
- En este enlace se puede escribir las soluciones en Lean.
- A continuación se muestran algunas soluciones (que se pueden probar en este enlace).
- En los comentarios se pueden publicar otras soluciones, en Lean o en otros sistemas de razonamiento.
- Para publicar las demostraciones en Lean se deben de escribir entre una línea con <pre lang="lean"> y otra con </pre>
- Para publicar las demostraciones en Isabelle/HOL se deben de escribir entre una línea con <pre lang="isar"> y otra con </pre>
2ª 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 |
Notas
- En este enlace se puede escribir las soluciones en Lean.
- A continuación se muestran algunas soluciones (que se pueden probar en este enlace).
- En los comentarios se pueden publicar otras soluciones, en Lean o en otros sistemas de razonamiento.
- Para publicar las demostraciones en Lean se deben de escribir entre una línea con <pre lang="lean"> y otra con </pre>
- Para publicar las demostraciones en Isabelle/HOL se deben de escribir entre una línea con <pre lang="isar"> y otra con </pre>
2ª propiedad semidistributiva de la intersección sobre la unión
Demostrar que
(s ∩ t) ∪ (s ∩ 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) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u):= sorry |
Notas
- En este enlace se puede escribir las soluciones en Lean.
- A continuación se muestran algunas soluciones (que se pueden probar en este enlace).
- En los comentarios se pueden publicar otras soluciones, en Lean o en otros sistemas de razonamiento.
- Para publicar las demostraciones en Lean se deben de escribir entre una línea con <pre lang="lean"> y otra con </pre>
- Para publicar las demostraciones en Isabelle/HOL se deben de escribir entre una línea con <pre lang="isar"> y otra con </pre>
Read More «2ª propiedad semidistributiva de la intersección sobre la unión»
Propiedad semidistributiva 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 |
Notas
- En este enlace se puede escribir las soluciones en Lean.
- A continuación se muestran algunas soluciones (que se pueden probar en este enlace).
- En los comentarios se pueden publicar otras soluciones, en Lean o en otros sistemas de razonamiento.
- Para publicar las demostraciones en Lean se deben de escribir entre una línea con <pre lang="lean"> y otra con </pre>
- Para publicar las demostraciones en Isabelle/HOL se deben de escribir entre una línea con <pre lang="isar"> y otra con </pre>
Read More «Propiedad semidistributiva de la intersección sobre la unión»
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 |
Notas
- En este enlace se puede escribir las soluciones en Lean.
- A continuación se muestran algunas soluciones (que se pueden probar en este enlace).
- En los comentarios se pueden publicar otras soluciones, en Lean o en otros sistemas de razonamiento.
- Para publicar las demostraciones en Lean se deben de escribir entre una línea con <pre lang="lean"> y otra con </pre>
- Para publicar las demostraciones en Isabelle/HOL se deben de escribir entre una línea con <pre lang="isar"> y otra con </pre>
Sobre Calculemus
El objetivo principal de Calculemus es proponer ejercicios de demostración de resultados matemáticos usando sistemas de demostración interactiva, fundamentalmente Lean e Isabelle/HOL.
En los enunciados de los ejercicios se da la plantilla para Lean.
Las soluciones propuestas están en la versión 3.30.0 de Lean y en la versión 2021 de Isabelle/HOL. Las distintas soluciones están ordenadas desde las más detalladas a las más automáticas. Además, las soluciones están en este repositorio de GitHub.
Es recomendable, antes de leer las soluciones propuestas, intentar escribir demostraciones propias (en el caso de Lean se pueden probar en el navegador a través de este enlace).
En los comentarios se pueden publicar demostraciones distintas de las propuestas en Lean, Isabelle/HOL u otros sistemas (como Coq, Agda o PVS.
Las reflexivas circulares son simétricas
Se dice que la relación binaria R es
- reflexiva si ∀x. R(x, x)
- circular si ∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)
- simétrica si ∀x y. R(x, y) ⟶ R(y, x)
Demostrar que las relaciones reflexivas y circulares son simétricas. Para ello, completar la siguiente teoría de Isabelle/HOL:
|
1 2 3 4 5 6 7 8 9 10 11 |
theory Las_reflexivas_circulares_son_simetricas imports Main begin lemma assumes "∀x. R(x, x)" "∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)" shows "∀x y. R(x, y) ⟶ R(y, x)" oops end |
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 |
theory Las_reflexivas_circulares_son_simetricas imports Main begin (* 1ª demostración: automática *) lemma assumes "∀x. R(x, x)" "∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)" shows "∀x y. R(x, y) ⟶ R(y, x)" using assms by blast (* 2ª demostración: estructurada *) lemma assumes "∀x. R(x, x)" "∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)" shows "∀x y. R(x, y) ⟶ R(y, x)" proof (rule allI)+ fix a b show "R (a, b) ⟶ R (b, a)" proof (rule impI) assume "R(a, b)" have "R(b, b)" using assms(1) by (rule allE) with `R(a, b)` have "R(a, b) ∧ R(b, b)" by (rule conjI) have "∀y z. R(a, y) ∧ R(y, z) ⟶ R(z, a)" using assms(2) by (rule allE) then have "∀z. R(a, b) ∧ R(b, z) ⟶R(z, a)" by (rule allE) then have "R(a, b) ∧ R(b, b) ⟶R(b, a)" by (rule allE) then show "R(b, a)" using `R(a, b) ∧ R(b, b)` by (rule mp) qed qed (* 3º demostración: detallada *) lemma assumes "∀x. R(x, x)" "∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)" shows "∀x y. R(x, y) ⟶ R(y, x)" proof (rule allI)+ fix a b show "R (a, b) ⟶ R (b, a)" proof (rule impI) assume "R(a , b)" have "R(b, b)" using assms(1) .. with `R(a, b)` have "R(a, b) ∧ R(b, b)" .. have "∀y z. R(a, y) ∧ R(y, z) ⟶ R(z, a)" using assms(2) .. then have "∀z. R(a, b) ∧ R(b, z) ⟶R(z, a)" .. then have "R(a, b) ∧ R(b, b) ⟶R(b, a)" .. then show "R(b, a)" using `R(a, b) ∧ R(b, b)` .. qed qed end |
Otras soluciones
- Se pueden escribir otras soluciones en los comentarios.
- El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>
El problema del barbero
Decidir si es cierto que
Carlos afeita a todos los habitantes de Las Chinas que no se afeitan a sí mismo y sólo a ellos. Carlos es un habitante de las Chinas. Por consiguiente, Carlos no afeita a nadie.
Se usará la siguiente simbolización:
- A(x,y) para x afeita a y
- C(x) para x es un habitante de Las Chinas
- c para Carlos
El problema consiste en completar la siguiente teoría de Isabelle/HOL:
|
1 2 3 4 5 6 7 8 9 10 |
theory El_problema_del_barbero imports Main begin lemma assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)" "C(c)" shows "¬(∃x. A(c,x))" oops end |
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 |
theory El_problema_del_barbero imports Main begin ― ‹La demostración automática es› lemma assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)" "C(c)" shows "¬(∃x. A(c,x))" using assms by auto ― ‹La demostración estructurada es› lemma assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)" "C(c)" shows "¬(∃x. A(c,x))" proof - have 1: "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" using assms(1) .. have "A(c,c)" proof (rule ccontr) assume "¬A(c,c)" with assms(2) have "C(c) ∧ ¬A(c,c)" .. with 1 have "A(c,c)" .. with ‹¬A(c,c)› show False .. qed have "¬A(c,c)" proof - have "C(c) ∧ ¬A(c,c)" using 1 ‹A(c,c)› .. then show "¬A(c,c)" .. qed then show "¬(∃x. A(c,x))" using ‹A(c,c)› .. qed ― ‹La demostración detallada es› lemma assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)" "C(c)" shows "¬(∃x. A(c,x))" proof - have 1: "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" using assms(1) by (rule allE) have "A(c,c)" proof (rule ccontr) assume "¬A(c,c)" with assms(2) have "C(c) ∧ ¬A(c,c)" by (rule conjI) with 1 have "A(c,c)" by (rule iffD2) with ‹¬A(c,c)› show False by (rule notE) qed have "¬A(c,c)" proof - have "C(c) ∧ ¬A(c,c)" using 1 ‹A(c,c)› by (rule iffD1) then show "¬A(c,c)" by (rule conjunct2) qed then show "¬(∃x. A(c,x))" using ‹A(c,c)› by (rule notE) qed end |
Otras soluciones
- Se pueden escribir otras soluciones en los comentarios.
- El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>
El problema de los infectados
Decidir si es cierto que
Existe una persona tal que si dicha persona se infecta, entonces todas las personas se infectan.
En la formalización se usará I(x) para representar que la persona x está infectada. El problema consiste en completar la siguiente teoría de Isabelle/HOL:
|
1 2 3 4 5 6 7 8 |
theory Infectados imports Main begin lemma "∃x. (I x ⟶ (∀y. I y))" by simp end |
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 |
theory Infectados imports Main begin (* 1ª solución (automática) *) lemma "∃x. (I x ⟶ (∀y. I y))" by simp (* 2ª solución (estructurada) *) lemma "∃x. (I x ⟶ (∀y. I y))" proof - have "¬ (∀y. I y) ∨ (∀y. I y)" .. then show "∃x. (I x ⟶ (∀y. I y))" proof assume "¬ (∀y. I y)" then have "∃y. ¬(I y)" by simp then obtain a where "¬ I a" .. then have "I a ⟶ (∀y. I y)" by simp then show "∃x. (I x ⟶ (∀y. I y))" .. next assume "∀y. I y" then show "∃x. (I x ⟶ (∀y. I y))" by simp qed qed (* 3ª solución (detallada con lemas auxiliares) *) lemma aux1: assumes "¬ (∀y. I y)" shows "∃y. ¬(I y)" proof (rule ccontr) assume "∄y. ¬ I y" have "∀y. I y" proof fix a show "I a" proof (rule ccontr) assume "¬ I a" then have "∃y. ¬ I y" by (rule exI) with ‹∄y. ¬ I y› show False by (rule notE) qed qed with assms show False by (rule notE) qed lemma aux2: assumes "¬P" shows "P ⟶ Q" proof assume "P" with assms show "Q" by (rule notE) qed lemma aux3: assumes "∄x. P x" shows "∀x. ¬ P x" proof fix a show "¬ P a" proof assume "P a" then have "∃x. P x" by (rule exI) with assms show False by (rule notE) qed qed lemma aux4: assumes "Q" shows "∃x. (P x ⟶ Q)" proof (rule ccontr) assume "∄x. (P x ⟶ Q)" then have "∀x. ¬ (P x ⟶ Q)" by (rule aux3) then have "¬ (P a ⟶ Q)" by (rule allE) moreover have "P a ⟶ Q" proof assume "P a" show "Q" using assms by this qed ultimately show False by (rule notE) qed lemma "∃x. (I x ⟶ (∀y. I y))" proof - have "¬ (∀y. I y) ∨ (∀y. I y)" .. then show "∃x. (I x ⟶ (∀y. I y))" proof assume "¬ (∀y. I y)" then have "∃y. ¬(I y)" by (rule aux1) then obtain a where "¬ I a" by (rule exE) then have "I a ⟶ (∀y. I y)" by (rule aux2) then show "∃x. (I x ⟶ (∀y. I y))" by (rule exI) next assume "∀y. I y" then show "∃x. (I x ⟶ (∀y. I y))" by (rule aux4) qed qed end |
Otras soluciones
- Se pueden escribir otras soluciones en los comentarios.
- El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>