La dama o el tigre
En el libro de Raymond Smullyan ¿La dama o el tigre? (en inglés, The lady or the tiger? se plantea el siguiente problema
Un rey somete a un prisionero a la siguiente prueba: lo enfrenta a dos
puertas, habitación correspondiente. Se informa al prisionero que en cada una de las habitaciones puede haber un tigre o una dama. Como es natural, el prisionero debe elegir la puerta que le lleva a la dama (entre otras cosas, para no ser devorado por el tigre). Para ayudarle, en cada puerta hay un letrero. El de la puerta 1 dice «en esta habitación hay una dama y en la otra un tigre» y el de la puerta 2 dice «en una de estas habitaciones hay una dama y en una de estas habitaciones hay un tigre».Sabiendo que uno de los carteles dice la verdad y el otro no, demostrar que la dama se encuentra en la segunda habitación.
Para la formalización del problema se usarán los siguientes símbolos
- c1 que representa el contenido del cartel de la puerta 1,
- c2 que representa el contenido del cartel de la puerta 2 ,
- dp que representa hay una dama en la primera habitación,
- tp que representa hay un tigre en la primera habitación,
- ds que representa hay una dama en la segunda habitación y
- ts que representa hay un tigre en la segunda habitación.
|
1 2 3 4 5 6 7 8 9 10 11 12 |
theory La_dama_o_el_tigre imports Main begin lemma assumes "c1 ⟷ dp ∧ ts" "c2 ⟷ (dp ∧ ts) ∨ (ds ∧ tp)" "(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)" shows "ds" oops end |
Demostrar con Isabelle/HOL que el argumento anterior es correcto.
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 |
theory La_dama_o_el_tigre imports Main begin (* 1ª demostración *) lemma assumes "c1 ⟷ dp ∧ ts" "c2 ⟷ (dp ∧ ts) ∨ (ds ∧ tp)" "(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)" shows "ds" oops using assms by auto (* 2ª demostración *) lemma assumes "c1 ⟷ dp ∧ ts" "c2 ⟷ (dp ∧ ts) ∨ (ds ∧ tp)" "(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)" shows "ds" proof - note ‹(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)› then show "ds" proof assume "c1 ∧ ¬ c2" then have "c1" .. with ‹c1 ⟷ dp ∧ ts› have "dp ∧ ts" .. then have "(dp ∧ ts) ∨ (ds ∧ tp)" .. with assms(2) have "c2" .. have "¬ c2" using ‹c1 ∧ ¬ c2› .. then show "ds" using ‹c2› .. next assume "c2 ∧ ¬ c1" then have "c2" .. with assms(2) have "(dp ∧ ts) ∨ (ds ∧ tp)" .. then show "ds" proof assume "dp ∧ ts" with assms(1) have c1 .. have "¬ c1" using ‹c2 ∧ ¬ c1› .. then show ds using ‹c1› .. next assume "ds ∧ tp" then show ds .. qed qed qed (* 3ª demostración *) lemma assumes "c1 ⟷ dp ∧ ts" "c2 ⟷ (dp ∧ ts) ∨ (ds ∧ tp)" "(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)" shows "ds" proof - note ‹(c1 ∧ ¬ c2) ∨ (c2 ∧ ¬ c1)› then show "ds" proof (rule disjE) assume "c1 ∧ ¬ c2" then have "c1" by (rule conjunct1) with ‹c1 ⟷ dp ∧ ts› have "dp ∧ ts" by (rule iffD1) then have "(dp ∧ ts) ∨ (ds ∧ tp)" by (rule disjI1) with assms(2) have "c2" by (rule iffD2) have "¬ c2" using ‹c1 ∧ ¬ c2› by (rule conjunct2) then show "ds" using ‹c2› by (rule notE) next assume "c2 ∧ ¬ c1" then have "c2" by (rule conjunct1) with assms(2) have "(dp ∧ ts) ∨ (ds ∧ tp)" by (rule iffD1) then show "ds" proof (rule disjE) assume "dp ∧ ts" with assms(1) have c1 by (rule iffD2) have "¬ c1" using ‹c2 ∧ ¬ c1› by (rule conjunct2) then show ds using ‹c1› by (rule notE) next assume "ds ∧ tp" then show ds by (rule conjunct1) qed 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>
Un comentario