{"id":756,"date":"2021-09-12T05:00:46","date_gmt":"2021-09-12T03:00:46","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=756"},"modified":"2021-09-08T13:14:09","modified_gmt":"2021-09-08T11:14:09","slug":"pruebas-de-que-la-funcion-espejo-de-los-arboles-binarios-es-involutiva","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/pruebas-de-que-la-funcion-espejo-de-los-arboles-binarios-es-involutiva\/","title":{"rendered":"Pruebas de que la funci\u00f3n espejo de los \u00e1rboles binarios es involutiva"},"content":{"rendered":"<p>El \u00e1rbol correspondiente a<\/p>\n<pre lang=\"text\">\n       3\n      \/ \\\n     2   4\n    \/ \\\n   1   5\n<\/pre>\n<p>se puede representar por el t\u00e9rmino<\/p>\n<pre lang=\"text\">\n   nodo 3 (nodo 2 (hoja 1) (hoja 5)) (hoja 4)\n<\/pre>\n<p>usado el tipo de dato arbol definido por<\/p>\n<pre lang=\"text\">\n   inductive arbol (\u03b1 : Type) : Type\n   | hoja : \u03b1 \u2192 arbol\n   | nodo : \u03b1 \u2192 arbol \u2192 arbol \u2192 arbol\n<\/pre>\n<p>La imagen especular del \u00e1rbol anterior es<\/p>\n<pre lang=\"text\">\n     3\n    \/ \\\n   4   2\n      \/ \\\n     5   1\n<\/pre>\n<p>cuyo t\u00e9rmino es<\/p>\n<pre lang=\"text\">\n   nodo 3 (hoja 4) (nodo 2 (hoja 5) (hoja 1))\n<\/pre>\n<p>La definici\u00f3n de la funci\u00f3n que calcula la imagen especular es<\/p>\n<pre lang=\"text\">\n   def espejo : arbol \u03b1 \u2192 arbol \u03b1\n   | (hoja x)     := hoja x\n   | (nodo x i d) := nodo x (espejo d) (espejo i)\n<\/pre>\n<p>Demostrar que la funci\u00f3n espejo es involutiva; es decir,<\/p>\n<pre lang=\"text\">\n   espejo (espejo a) = a\n<\/pre>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport tactic\n\nvariable  {\u03b1 : Type}\n\ninductive arbol (\u03b1 : Type) : Type\n| hoja : \u03b1 \u2192 arbol\n| nodo : \u03b1 \u2192 arbol \u2192 arbol \u2192 arbol\n\nnamespace arbol\n\nvariables (a i d : arbol \u03b1)\nvariable  (x : \u03b1)\n\ndef espejo : arbol \u03b1 \u2192 arbol \u03b1\n| (hoja x)     := hoja x\n| (nodo x i d) := nodo x (espejo d) (espejo i)\n\nexample :\n  espejo (espejo a) = a :=\nsorry\n\nend arbol\n<\/pre>\n<p>[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n<pre lang=\"lean\">\r\nimport tactic\r\n\r\nvariable  {\u03b1 : Type}\r\n\r\ninductive arbol (\u03b1 : Type) : Type\r\n| hoja : \u03b1 \u2192 arbol\r\n| nodo : \u03b1 \u2192 arbol \u2192 arbol \u2192 arbol\r\n\r\nnamespace arbol\r\n\r\nvariables (a i d : arbol \u03b1)\r\nvariable  (x : \u03b1)\r\n\r\ndef espejo : arbol \u03b1 \u2192 arbol \u03b1\r\n| (hoja x)     := hoja x\r\n| (nodo x i d) := nodo x (espejo d) (espejo i)\r\n\r\n@[simp]\r\nlemma espejo_1 :\r\n  espejo (hoja x) = hoja x :=\r\nespejo.equations._eqn_1 x\r\n\r\n@[simp]\r\nlemma espejo_2 :\r\n  espejo (nodo x i d) = nodo x (espejo d) (espejo i) :=\r\nespejo.equations._eqn_2 x i d\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample :\r\n  espejo (espejo a) = a :=\r\nbegin\r\n  induction a with x x i d Hi Hd,\r\n  { rw espejo_1,\r\n    rw espejo_1, },\r\n  { rw espejo_2,\r\n    rw espejo_2,\r\n    rw Hi,\r\n    rw Hd, },\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample :\r\n  espejo (espejo a) = a :=\r\nbegin\r\n  induction a with x x i d Hi Hd,\r\n  { calc espejo (espejo (hoja x))\r\n         = espejo (hoja x)\r\n             : congr_arg espejo (espejo_1 x)\r\n     ... = hoja x\r\n             : espejo_1 x, },\r\n  { calc espejo (espejo (nodo x i d))\r\n         = espejo (nodo x (espejo d) (espejo i))\r\n             : congr_arg espejo (espejo_2 i d x)\r\n     ... = nodo x (espejo (espejo i)) (espejo (espejo d))\r\n             : espejo_2 (espejo d) (espejo i) x\r\n     ... = nodo x i (espejo (espejo d))\r\n             : congr_arg2 (nodo x) Hi rfl\r\n     ... = nodo x i d\r\n             : congr_arg2 (nodo x) rfl Hd, },\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample :\r\n  espejo (espejo a) = a :=\r\nbegin\r\n  induction a with x x i d Hi Hd,\r\n  { calc espejo (espejo (hoja x))\r\n         = espejo (hoja x)\r\n             : congr_arg espejo (espejo_1 x)\r\n     ... = hoja x\r\n             : by rw espejo_1, },\r\n  { calc espejo (espejo (nodo x i d))\r\n         = espejo (nodo x (espejo d) (espejo i))\r\n             : congr_arg espejo (espejo_2 i d x)\r\n     ... = nodo x (espejo (espejo i)) (espejo (espejo d))\r\n             : by rw espejo_2\r\n     ... = nodo x i (espejo (espejo d))\r\n             : by rw Hi\r\n     ... = nodo x i d\r\n             : by rw Hd, },\r\nend\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample :\r\n  espejo (espejo a) = a :=\r\nbegin\r\n  induction a with x x i d Hi Hd,\r\n  { calc espejo (espejo (hoja x))\r\n         = espejo (hoja x)\r\n             : by simp\r\n     ... = hoja x\r\n             : by simp },\r\n  { calc espejo (espejo (nodo x i d))\r\n         = espejo (nodo x (espejo d) (espejo i))\r\n             : by simp\r\n     ... = nodo x (espejo (espejo i)) (espejo (espejo d))\r\n             : by simp\r\n     ... = nodo x i (espejo (espejo d))\r\n             : by simp [Hi]\r\n     ... = nodo x i d\r\n             : by simp [Hd], },\r\nend\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample :\r\n  espejo (espejo a) = a :=\r\nbegin\r\n  induction a with _ x i d Hi Hd,\r\n  { simp, },\r\n  { simp [Hi, Hd], },\r\nend\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nexample :\r\n  espejo (espejo a) = a :=\r\nby induction a ; simp [*]\r\n\r\n-- 7\u00aa demostraci\u00f3n\r\nexample :\r\n  espejo (espejo a) = a :=\r\narbol.rec_on a\r\n  ( assume x,\r\n    calc espejo (espejo (hoja x))\r\n         = espejo (hoja x)\r\n             : congr_arg espejo (espejo_1 x)\r\n     ... = hoja x\r\n             : espejo_1 x)\r\n  ( assume x i d,\r\n    assume Hi : espejo (espejo i) = i,\r\n    assume Hd : espejo (espejo d) = d,\r\n    calc espejo (espejo (nodo x i d))\r\n         = espejo (nodo x (espejo d) (espejo i))\r\n             : congr_arg espejo (espejo_2 i d x)\r\n     ... = nodo x (espejo (espejo i)) (espejo (espejo d))\r\n             : by rw espejo_2\r\n     ... = nodo x i (espejo (espejo d))\r\n             : by rw Hi\r\n     ... = nodo x i d\r\n             : by rw Hd )\r\n\r\n-- 8\u00aa demostraci\u00f3n\r\nexample :\r\n  espejo (espejo a) = a :=\r\narbol.rec_on a\r\n  (\u03bb x, by simp )\r\n  (\u03bb x i d Hi Hd, by simp [Hi,Hd])\r\n\r\n-- 9\u00aa demostraci\u00f3n\r\nlemma espejo_espejo :\r\n  \u2200 a : arbol \u03b1, espejo (espejo a) = a\r\n| (hoja x)     := by simp\r\n| (nodo x i d) := by simp [espejo_espejo i, espejo_espejo d]\r\n\r\nend arbol\r\n<\/pre>\n<p>Se puede interactuar con la prueba anterior en <a href=\"https:\/\/leanprover-community.github.io\/lean-web-editor\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus\/main\/src\/Pruebas_de_que_la_funcion_espejo_de_los_arboles_binarios_es_involutiva.lean\" rel=\"noopener noreferrer\" target=\"_blank\">esta sesi\u00f3n con Lean<\/a>.<\/p>\n<p>En los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con &#60;pre lang=&quot;lean&quot;&#62; y otra con &#60;\/pre&#62;<br \/>\n[\/expand]<\/p>\n<p>[expand title=\u00bbSoluciones con Isabelle\/HOL\u00bb]<\/p>\n<pre lang=\"isar\">\r\ntheory Pruebas_de_que_la_funcion_espejo_de_los_arboles_binarios_es_involutiva\r\nimports Main\r\nbegin\r\n\r\ndatatype 'a arbol = hoja \"'a\"\r\n                  | nodo \"'a\" \"'a arbol\" \"'a arbol\"\r\n\r\nfun espejo :: \"'a arbol \u21d2 'a arbol\" where\r\n  \"espejo (hoja x)     = (hoja x)\"\r\n| \"espejo (nodo x i d) = (nodo x (espejo d) (espejo i))\"\r\n\r\n(* 1\u00aa demostraci\u00f3n *)\r\nlemma\r\n  fixes a :: \"'b arbol\"\r\n  shows \"espejo (espejo a) = a\" (is \"?P a\")\r\nproof (induct a)\r\n  fix x\r\n  show \"?P (hoja x)\"\r\n    by (simp only: espejo.simps(1))\r\nnext\r\n  fix x\r\n  fix i assume h1: \"?P i\"\r\n  fix d assume h2: \"?P d\"\r\n  show \"?P (nodo x i d)\"\r\n  proof -\r\n    have \"espejo (espejo (nodo x i d)) =\r\n          espejo (nodo x (espejo d) (espejo i))\"\r\n      by (simp only: espejo.simps(2))\r\n    also have \"\u2026 = nodo x (espejo (espejo i)) (espejo (espejo d))\"\r\n      by (simp only: espejo.simps(2))\r\n    also have \"\u2026 = nodo x i d\"\r\n      by (simp only: h1 h2)\r\n    finally show ?thesis\r\n      by this\r\n qed\r\nqed\r\n\r\n(* 2\u00aa demostraci\u00f3n *)\r\nlemma\r\n  fixes a :: \"'b arbol\"\r\n  shows \"espejo (espejo a) = a\" (is \"?P a\")\r\nproof (induct a)\r\n  fix x\r\n  show \"?P (hoja x)\"  by simp\r\nnext\r\n  fix x\r\n  fix i assume h1: \"?P i\"\r\n  fix d assume h2: \"?P d\"\r\n  show \"?P (nodo x i d)\"\r\n  proof -\r\n    have \"espejo (espejo (nodo x i d)) =\r\n          espejo (nodo x (espejo d) (espejo i))\" by simp\r\n    also have \"\u2026 = nodo x (espejo (espejo i)) (espejo (espejo d))\"\r\n      by simp\r\n    also have \"\u2026 = nodo x i d\" using h1 h2 by simp\r\n    finally show ?thesis .\r\n qed\r\nqed\r\n\r\n(* 3\u00aa demostraci\u00f3n *)\r\nlemma\r\n  \"espejo (espejo a ) = a\"\r\nby (induct a) simp_all\r\n\r\nend\r\n<\/pre>\n<p>En los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con &#60;pre lang=&quot;isar&quot;&#62; y otra con &#60;\/pre&#62;<br \/>\n[\/expand]<\/p>\n","protected":false},"excerpt":{"rendered":"<p>El \u00e1rbol correspondiente a 3 \/ \\ 2 4 \/ \\ 1 5 se puede representar por el t\u00e9rmino nodo 3 (nodo 2 (hoja 1) (hoja 5)) (hoja 4) usado el tipo de dato arbol definido por inductive arbol (\u03b1 : Type) : Type | hoja : \u03b1 \u2192 arbol | nodo : \u03b1 \u2192 arbol \u2192 arbol \u2192 arbol La imagen especular del \u00e1rbol anterior es 3 \/ \\ 4 2 \/ \\ 5 1 cuyo t\u00e9rmino es nodo 3 (hoja 4) (nodo 2 (hoja 5) (hoja 1)) La definici\u00f3n de la funci\u00f3n que calcula la imagen especular es def espejo : arbol \u03b1 \u2192 arbol \u03b1 | (hoja x) := hoja x | (nodo x i d) := nodo x (espejo d) (espejo&#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":[278,105],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/756"}],"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=756"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/756\/revisions"}],"predecessor-version":[{"id":757,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/756\/revisions\/757"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=756"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=756"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=756"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}