{"id":217,"date":"2020-03-12T06:00:23","date_gmt":"2020-03-12T04:00:23","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=217"},"modified":"2025-03-14T17:37:18","modified_gmt":"2025-03-14T15:37:18","slug":"la-dama-o-el-tigre","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/la-dama-o-el-tigre\/","title":{"rendered":"La dama o el tigre"},"content":{"rendered":"<p>En el libro de Raymond Smullyan <em>\u00bfLa dama o el tigre?<\/em> (en ingl\u00e9s, <a href=\"http:\/\/bit.ly\/2W5E4bC\">The lady or the tiger?<\/a> se plantea el siguiente  problema<\/p>\n<blockquote><p>\nUn rey somete a un prisionero a la siguiente prueba: lo enfrenta a dos<br \/>\npuertas, de las que el prisionero debe elegir una, y entrar la habitaci\u00f3n 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 \u00aben esta habitaci\u00f3n hay una dama y en la otra un tigre\u00bb y el de la puerta 2 dice \u00aben una de estas habitaciones hay una dama y en una de estas habitaciones hay un tigre\u00bb.<\/p>\n<p>Sabiendo que uno de los carteles dice la verdad y el otro no, demostrar que la dama se encuentra en la segunda habitaci\u00f3n.\n<\/p><\/blockquote>\n<p>Para la formalizaci\u00f3n del problema se usar\u00e1n los siguientes s\u00edmbolos<\/p>\n<ul>\n<li>c1 que representa <em>el contenido del cartel de la puerta 1<\/em>,<\/li>\n<li>c2 que representa <em>el contenido del cartel de la puerta 2<\/em> ,<\/li>\n<li>dp que representa <em>hay una dama en la primera habitaci\u00f3n<\/em>,<\/li>\n<li>tp que representa <em>hay un tigre en la primera habitaci\u00f3n<\/em>,<\/li>\n<li>ds que representa <em>hay una dama en la segunda habitaci\u00f3n<\/em> y<\/li>\n<li>ts que representa <em>hay un tigre en la segunda habitaci\u00f3n<\/em>.<\/li>\n<\/ul>\n<pre lang=\"isar\">\ntheory La_dama_o_el_tigre\nimports Main\nbegin\n\nlemma\n  assumes \"c1 \u27f7 dp \u2227 ts\"\n          \"c2 \u27f7 (dp \u2227 ts) \u2228 (ds \u2227 tp)\"\n          \"(c1 \u2227 \u00ac c2) \u2228 (c2 \u2227 \u00ac c1)\"\n  shows   \"ds\"\n  oops\n\nend\n<\/pre>\n<p>Demostrar con Isabelle\/HOL que el argumento anterior es correcto.<\/p>\n<h4>Soluciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory La_dama_o_el_tigre\nimports Main\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\nlemma\n  assumes \"c1 \u27f7 dp \u2227 ts\"\n          \"c2 \u27f7 (dp \u2227 ts) \u2228 (ds \u2227 tp)\"\n          \"(c1 \u2227 \u00ac c2) \u2228 (c2 \u2227 \u00ac c1)\"\n  shows   \"ds\"\n  oops\n  using assms\n  by auto\n\n(* 2\u00aa demostraci\u00f3n *)\nlemma\n  assumes \"c1 \u27f7 dp \u2227 ts\"\n    \"c2 \u27f7 (dp \u2227 ts) \u2228 (ds \u2227 tp)\"\n    \"(c1 \u2227 \u00ac c2) \u2228 (c2 \u2227 \u00ac c1)\"\n  shows \"ds\"\nproof -\n  note \u2039(c1 \u2227 \u00ac c2) \u2228 (c2 \u2227 \u00ac c1)\u203a\n  then show \"ds\"\n  proof\n    assume \"c1 \u2227 \u00ac c2\"\n    then have \"c1\" ..\n    with \u2039c1 \u27f7 dp \u2227 ts\u203a have \"dp \u2227 ts\" ..\n    then have \"(dp \u2227 ts) \u2228 (ds \u2227 tp)\" ..\n    with assms(2) have \"c2\" ..\n    have \"\u00ac c2\" using \u2039c1 \u2227 \u00ac c2\u203a ..\n    then show \"ds\" using \u2039c2\u203a ..\n  next\n    assume \"c2 \u2227 \u00ac c1\"\n    then have \"c2\" ..\n    with assms(2) have \"(dp \u2227 ts) \u2228 (ds \u2227 tp)\" ..\n    then show \"ds\"\n    proof\n      assume \"dp \u2227 ts\"\n      with assms(1) have c1 ..\n      have \"\u00ac c1\" using \u2039c2 \u2227 \u00ac c1\u203a ..\n      then show ds using \u2039c1\u203a ..\n    next\n      assume \"ds \u2227 tp\"\n      then show ds ..\n    qed\n  qed\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\nlemma\n  assumes \"c1 \u27f7 dp \u2227 ts\"\n    \"c2 \u27f7 (dp \u2227 ts) \u2228 (ds \u2227 tp)\"\n    \"(c1 \u2227 \u00ac c2) \u2228 (c2 \u2227 \u00ac c1)\"\n  shows \"ds\"\nproof -\n  note \u2039(c1 \u2227 \u00ac c2) \u2228 (c2 \u2227 \u00ac c1)\u203a\n  then show \"ds\"\n  proof (rule disjE)\n    assume \"c1 \u2227 \u00ac c2\"\n    then have \"c1\" by (rule conjunct1)\n    with \u2039c1 \u27f7 dp \u2227 ts\u203a have \"dp \u2227 ts\" by (rule iffD1)\n    then have \"(dp \u2227 ts) \u2228 (ds \u2227 tp)\" by (rule disjI1)\n    with assms(2) have \"c2\" by (rule iffD2)\n    have \"\u00ac c2\" using \u2039c1 \u2227 \u00ac c2\u203a by (rule conjunct2)\n    then show \"ds\" using \u2039c2\u203a by (rule notE)\n  next\n    assume \"c2 \u2227 \u00ac c1\"\n    then have \"c2\" by (rule conjunct1)\n    with assms(2) have \"(dp \u2227 ts) \u2228 (ds \u2227 tp)\" by (rule iffD1)\n    then show \"ds\"\n    proof (rule disjE)\n      assume \"dp \u2227 ts\"\n      with assms(1) have c1 by (rule iffD2)\n      have \"\u00ac c1\" using \u2039c2 \u2227 \u00ac c1\u203a by (rule conjunct2)\n      then show ds using \u2039c1\u203a by (rule notE)\n    next\n      assume \"ds \u2227 tp\"\n      then show ds by (rule conjunct1)\n    qed\n  qed\nqed\n\nend\n<\/pre>\n<h4>Otras soluciones<\/h4>\n<ul>\n<li>Se pueden escribir otras soluciones en los comentarios.\n<li>El c\u00f3digo se debe escribir entre una l\u00ednea con &#60;pre lang=&quot;isar&quot;&#62; y otra con &#60;\/pre&#62;\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>En el libro de Raymond Smullyan \u00bfLa dama o el tigre? (en ingl\u00e9s, 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, de las que el prisionero debe elegir una, y entrar la habitaci\u00f3n 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 \u00aben esta habitaci\u00f3n hay una dama y en la otra un tigre\u00bb y el de la puerta&#8230;<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"default","_kad_post_title":"default","_kad_post_layout":"default","_kad_post_sidebar_id":"","_kad_post_content_style":"default","_kad_post_vertical_padding":"default","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[104],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/217"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/comments?post=217"}],"version-history":[{"count":16,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/217\/revisions"}],"predecessor-version":[{"id":2534,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/217\/revisions\/2534"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=217"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=217"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=217"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}