{"id":227,"date":"2020-03-19T18:10:06","date_gmt":"2020-03-19T16:10:06","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=227"},"modified":"2025-03-15T15:09:33","modified_gmt":"2025-03-15T13:09:33","slug":"el-problema-de-los-infectados","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/el-problema-de-los-infectados\/","title":{"rendered":"El problema de los infectados"},"content":{"rendered":"<p>Decidir si es cierto que<\/p>\n<blockquote><p>\nExiste una persona tal que si dicha persona se infecta, entonces todas las personas se infectan.\n<\/p><\/blockquote>\n<p>En la formalizaci\u00f3n se usar\u00e1 I(x) para representar que la persona x est\u00e1 infectada. El problema consiste en completar la siguiente teor\u00eda de Isabelle\/HOL:<\/p>\n<pre lang=\"isar\">\ntheory Infectados\nimports Main\nbegin\n\nlemma \"\u2203x. (I x \u27f6 (\u2200y. I y))\"\n  by simp\n\nend\n<\/pre>\n<h4>Soluciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Infectados\nimports Main\n\nbegin\n\n(* 1\u00aa soluci\u00f3n (autom\u00e1tica) *)\nlemma \"\u2203x. (I x \u27f6 (\u2200y. I y))\"\n  by simp\n\n(* 2\u00aa soluci\u00f3n (estructurada) *)\nlemma \"\u2203x. (I x \u27f6 (\u2200y. I y))\"\nproof -\n  have \"\u00ac (\u2200y. I y) \u2228 (\u2200y. I y)\" ..\n  then show \"\u2203x. (I x \u27f6 (\u2200y. I y))\"\n  proof \n    assume \"\u00ac (\u2200y. I y)\"\n    then have \"\u2203y. \u00ac(I y)\" by simp\n    then obtain a where \"\u00ac I a\" ..\n    then have \"I a \u27f6 (\u2200y. I y)\" by simp\n    then show \"\u2203x. (I x \u27f6 (\u2200y. I y))\" ..\n  next\n    assume \"\u2200y. I y\"\n    then show \"\u2203x. (I x \u27f6 (\u2200y. I y))\" by simp\n  qed\nqed\n\n(* 3\u00aa soluci\u00f3n (detallada con lemas auxiliares) *)\n\nlemma aux1:\n  assumes \"\u00ac (\u2200y. I y)\"\n  shows \"\u2203y. \u00ac(I y)\"\nproof (rule ccontr)\n  assume \"\u2204y. \u00ac I y\"\n  have \"\u2200y. I y\"\n  proof \n    fix a\n    show \"I a\"\n    proof (rule ccontr)\n      assume \"\u00ac I a\"\n      then have \"\u2203y. \u00ac I y\" by (rule exI)\n      with \u2039\u2204y. \u00ac I y\u203a show False by (rule notE)\n    qed \n  qed\n  with assms show False by (rule notE)\nqed\n\nlemma aux2:\n  assumes \"\u00acP\"\n  shows   \"P \u27f6 Q\"\nproof\n  assume \"P\"\n  with assms show \"Q\" by (rule notE)\nqed\n\nlemma aux3:\n  assumes \"\u2204x. P x\"\n  shows   \"\u2200x. \u00ac P x\"\nproof\n  fix a\n  show \"\u00ac P a\"\n  proof \n    assume \"P a\"\n    then have \"\u2203x. P x\" by (rule exI)\n    with assms show False by (rule notE)\n  qed \nqed\n\nlemma aux4:\n  assumes \"Q\"\n  shows   \"\u2203x. (P x \u27f6 Q)\"\nproof (rule ccontr)\n  assume \"\u2204x. (P x \u27f6 Q)\"\n  then have \"\u2200x. \u00ac (P x \u27f6 Q)\" by (rule aux3)\n  then have \"\u00ac (P a \u27f6 Q)\" by (rule allE)\n  moreover\n  have \"P a \u27f6 Q\"\n  proof\n    assume \"P a\"\n    show \"Q\" using assms by this\n  qed\n  ultimately show False by (rule notE)\nqed\n\nlemma \"\u2203x. (I x \u27f6 (\u2200y. I y))\"\nproof -\n  have \"\u00ac (\u2200y. I y) \u2228 (\u2200y. I y)\" ..\n  then show \"\u2203x. (I x \u27f6 (\u2200y. I y))\"\n  proof \n    assume \"\u00ac (\u2200y. I y)\"\n    then have \"\u2203y. \u00ac(I y)\" by (rule aux1)\n    then obtain a where \"\u00ac I a\" by (rule exE)\n    then have \"I a \u27f6 (\u2200y. I y)\" by (rule aux2)\n    then show \"\u2203x. (I x \u27f6 (\u2200y. I y))\" by (rule exI)\n  next\n    assume \"\u2200y. I y\"\n    then show \"\u2203x. (I x \u27f6 (\u2200y. I y))\" by (rule aux4)\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>Decidir si es cierto que Existe una persona tal que si dicha persona se infecta, entonces todas las personas se infectan. En la formalizaci\u00f3n se usar\u00e1 I(x) para representar que la persona x est\u00e1 infectada. El problema consiste en completar la siguiente teor\u00eda de Isabelle\/HOL: theory Infectados imports Main begin lemma \u00ab\u2203x. (I x \u27f6 (\u2200y. I y))\u00bb by simp end Soluciones con Isabelle\/HOL theory Infectados imports Main begin (* 1\u00aa soluci\u00f3n (autom\u00e1tica) *) lemma \u00ab\u2203x. (I x \u27f6 (\u2200y. I y))\u00bb by simp (* 2\u00aa soluci\u00f3n (estructurada) *) lemma \u00ab\u2203x. (I x \u27f6 (\u2200y. I y))\u00bb proof &#8211; have \u00ab\u00ac (\u2200y. I y) \u2228 (\u2200y. I y)\u00bb .. then show \u00ab\u2203x. (I x \u27f6 (\u2200y. I y))\u00bb proof assume \u00ab\u00ac (\u2200y. I y)\u00bb then&#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":[103],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/227"}],"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=227"}],"version-history":[{"count":8,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/227\/revisions"}],"predecessor-version":[{"id":2541,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/227\/revisions\/2541"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=227"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=227"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=227"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}