{"id":238,"date":"2020-04-08T18:35:16","date_gmt":"2020-04-08T16:35:16","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=238"},"modified":"2021-08-21T13:19:56","modified_gmt":"2021-08-21T11:19:56","slug":"las-reflexivas-circulares-son-simetricas","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/las-reflexivas-circulares-son-simetricas\/","title":{"rendered":"Las reflexivas circulares son sim\u00e9tricas"},"content":{"rendered":"<p>Se dice que la relaci\u00f3n binaria R es<\/p>\n<ul>\n<li>reflexiva si \u2200x. R(x, x)<\/li>\n<li>circular si \u2200x y z. R(x, y) \u2227 R(y, z) \u27f6 R(z, x)<\/li>\n<li>sim\u00e9trica si \u2200x y. R(x, y) \u27f6 R(y, x)<\/li>\n<\/ul>\n<p>Demostrar que las relaciones reflexivas y circulares son sim\u00e9tricas. Para ello, completar la siguiente teor\u00eda de Isabelle\/HOL:<\/p>\n<pre lang=\"isar\">\ntheory Las_reflexivas_circulares_son_simetricas\nimports Main\nbegin\n\nlemma\n  assumes \"\u2200x. R(x, x)\"\n          \"\u2200x y z. R(x, y) \u2227 R(y, z) \u27f6 R(z, x)\"\n  shows   \"\u2200x y. R(x, y) \u27f6 R(y, x)\"\n  oops\n\nend\n<\/pre>\n<h4>Soluciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Las_reflexivas_circulares_son_simetricas\nimports Main\nbegin\n\n(* 1\u00aa demostraci\u00f3n: autom\u00e1tica *)\nlemma\n  assumes \"\u2200x. R(x, x)\"\n          \"\u2200x y z. R(x, y) \u2227 R(y, z) \u27f6 R(z, x)\"\n  shows   \"\u2200x y. R(x, y) \u27f6 R(y, x)\"\n  using assms\n  by blast\n\n(* 2\u00aa demostraci\u00f3n: estructurada *)\nlemma\n  assumes \"\u2200x. R(x, x)\"\n          \"\u2200x y z. R(x, y) \u2227 R(y, z) \u27f6 R(z, x)\"\n  shows   \"\u2200x y. R(x, y) \u27f6 R(y, x)\"\nproof (rule allI)+\n  fix a b\n  show \"R (a, b) \u27f6 R (b, a)\"\n  proof (rule impI)\n    assume \"R(a, b)\"\n    have \"R(b, b)\"\n      using assms(1) by (rule allE)\n    with `R(a, b)` have \"R(a, b) \u2227 R(b, b)\"\n      by (rule conjI)\n    have  \"\u2200y z. R(a, y) \u2227 R(y, z) \u27f6 R(z, a)\"\n      using assms(2) by (rule allE)\n    then have \"\u2200z. R(a, b) \u2227 R(b, z) \u27f6R(z, a)\"\n      by (rule allE)\n    then have \"R(a, b) \u2227 R(b, b) \u27f6R(b, a)\"\n      by (rule allE)\n    then show \"R(b, a)\" using `R(a, b) \u2227 R(b, b)`\n      by (rule mp)\n  qed\nqed\n\n(* 3\u00ba demostraci\u00f3n: detallada *)\nlemma\n  assumes \"\u2200x. R(x, x)\"\n          \"\u2200x y z. R(x, y) \u2227 R(y, z) \u27f6 R(z, x)\"\n  shows   \"\u2200x y. R(x, y) \u27f6 R(y, x)\"\nproof (rule allI)+\n  fix a b\n  show \"R (a, b) \u27f6 R (b, a)\"\n  proof (rule impI)\n    assume \"R(a , b)\"\n    have \"R(b, b)\" using assms(1) ..\n    with `R(a, b)` have \"R(a, b) \u2227 R(b, b)\" ..\n    have  \"\u2200y z. R(a, y) \u2227 R(y, z) \u27f6 R(z, a)\" using assms(2) ..\n    then have \"\u2200z. R(a, b) \u2227 R(b, z) \u27f6R(z, a)\" ..\n    then have \"R(a, b) \u2227 R(b, b) \u27f6R(b, a)\" ..\n    then show \"R(b, a)\" using `R(a, b) \u2227 R(b, b)` ..\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>Se dice que la relaci\u00f3n binaria R es reflexiva si \u2200x. R(x, x) circular si \u2200x y z. R(x, y) \u2227 R(y, z) \u27f6 R(z, x) sim\u00e9trica si \u2200x y. R(x, y) \u27f6 R(y, x) Demostrar que las relaciones reflexivas y circulares son sim\u00e9tricas. Para ello, completar la siguiente teor\u00eda de Isabelle\/HOL: theory Las_reflexivas_circulares_son_simetricas imports Main begin lemma assumes \u00ab\u2200x. R(x, x)\u00bb \u00ab\u2200x y z. R(x, y) \u2227 R(y, z) \u27f6 R(z, x)\u00bb shows \u00ab\u2200x y. R(x, y) \u27f6 R(y, x)\u00bb oops end Soluciones con Isabelle\/HOL theory Las_reflexivas_circulares_son_simetricas imports Main begin (* 1\u00aa demostraci\u00f3n: autom\u00e1tica *) lemma assumes \u00ab\u2200x. R(x, x)\u00bb \u00ab\u2200x y z. R(x, y) \u2227 R(y, z) \u27f6 R(z, x)\u00bb shows \u00ab\u2200x y. R(x, y) \u27f6 R(y, x)\u00bb using assms by blast (*&#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":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_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":[29],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/238"}],"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=238"}],"version-history":[{"count":7,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/238\/revisions"}],"predecessor-version":[{"id":266,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/238\/revisions\/266"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=238"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=238"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=238"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}