{"id":758,"date":"2021-09-13T05:00:02","date_gmt":"2021-09-13T03:00:02","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=758"},"modified":"2021-09-08T16:37:41","modified_gmt":"2021-09-08T14:37:41","slug":"razonamiento-sobre-arboles-binarios-aplanamiento-e-imagen-especular","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/razonamiento-sobre-arboles-binarios-aplanamiento-e-imagen-especular\/","title":{"rendered":"Razonamiento sobre \u00e1rboles binarios: Aplanamiento e imagen especular"},"content":{"rendered":"

El \u00e1rbol correspondiente a<\/p>\n

\n       3\n      \/ \\\n     2   4\n    \/ \\\n   1   5\n<\/pre>\n
se puede representar por el t\u00e9rmino<\/p>\n
\n   nodo 3 (nodo 2 (hoja 1) (hoja 5)) (hoja 4)\n<\/pre>\n
usando el tipo de dato arbol definido por<\/p>\n
\n   inductive arbol (\u03b1 : Type) : Type\n   | hoja : \u03b1 \u2192 arbol\n   | nodo : \u03b1 \u2192 arbol \u2192 arbol \u2192 arbol\n<\/pre>\n
La imagen especular del \u00e1rbol anterior es<\/p>\n
\n     3\n    \/ \\\n   4   2\n      \/ \\\n     5   1\n<\/pre>\n
y la lista obtenida aplan\u00e1ndolo (recorri\u00e9ndolo en orden infijo) es<\/p>\n
\n   [4, 3, 5, 2, 1]\n<\/pre>\n
La definici\u00f3n de la funci\u00f3n que calcula la imagen especular es<\/p>\n
\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
y la que aplana el \u00e1rbol es<\/p>\n
\n   def aplana : arbol \u03b1 \u2192 list \u03b1\n   | (hoja x)     := [x]\n   | (nodo x i d) := (aplana i) ++ [x] ++ (aplana d)\n<\/pre>\n
Demostrar que<\/p>\n
\n   aplana (espejo a) = rev (aplana a)\n<\/pre>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport tactic\nopen list\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\ndef aplana : arbol \u03b1 \u2192 list \u03b1\n| (hoja x)     := [x]\n| (nodo x i d) := (aplana i) ++ [x] ++ (aplana d)\n\nexample :\n  aplana (espejo a) = reverse (aplana a) :=\nsorry\n\nend arbol\n<\/pre>\n
[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n
\r\nimport tactic\r\nopen list\r\n\r\nvariable {\u03b1 : Type}\r\n\r\n-- Para que no use la notaci\u00f3n con puntos\r\nset_option pp.structure_projections false\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\nrfl\r\n\r\n@[simp]\r\nlemma espejo_2 :\r\n  espejo (nodo x i d) = nodo x (espejo d) (espejo i) :=\r\nrfl\r\n\r\ndef aplana : arbol \u03b1 \u2192 list \u03b1\r\n| (hoja x)     := [x]\r\n| (nodo x i d) := (aplana i) ++ [x] ++ (aplana d)\r\n\r\n@[simp]\r\nlemma aplana_1 :\r\n  aplana (hoja x) = [x] :=\r\nrfl\r\n\r\n@[simp]\r\nlemma aplana_2 :\r\n  aplana (nodo x i d) = (aplana i) ++ [x] ++ (aplana d) :=\r\nrfl\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample :\r\n  aplana (espejo a) = reverse (aplana a) :=\r\nbegin\r\n  induction a with x x i d Hi Hd,\r\n  { rw espejo_1,\r\n    rw aplana_1,\r\n    rw reverse_singleton, },\r\n  { rw espejo_2,\r\n    rw aplana_2,\r\n    rw [Hi, Hd],\r\n    rw aplana_2,\r\n    rw reverse_append,\r\n    rw reverse_append,\r\n    rw reverse_singleton,\r\n    rw append_assoc, },\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample :\r\n  aplana (espejo a) = reverse (aplana a) :=\r\nbegin\r\n  induction a with x x i d Hi Hd,\r\n  { calc aplana (espejo (hoja x))\r\n         = aplana (hoja x)\r\n             : congr_arg aplana (espejo_1 x)\r\n     ... = [x]\r\n             : aplana_1 x\r\n     ... = reverse [x]\r\n             : reverse_singleton x\r\n     ... = reverse (aplana (hoja x))\r\n             : congr_arg reverse (aplana_1 x).symm, },\r\n  { calc aplana (espejo (nodo x i d))\r\n         = aplana (nodo x (espejo d) (espejo i))\r\n             : congr_arg aplana (espejo_2 i d x)\r\n     ... = (aplana (espejo d) ++ [x]) ++ aplana (espejo i)\r\n             : aplana_2 (espejo d) (espejo i) x\r\n     ... = (reverse (aplana d) ++ [x]) ++ aplana (espejo i)\r\n             : congr_arg2 (++) (congr_arg2 (++) Hd rfl) rfl\r\n     ... = (reverse (aplana d) ++ [x]) ++ reverse (aplana i)\r\n             : congr_arg2 (++) rfl Hi\r\n     ... = (reverse (aplana d) ++ reverse [x]) ++ reverse (aplana i)\r\n             : congr_arg2 (++) (congr_arg2 (++) rfl (reverse_singleton x).symm) rfl\r\n     ... = reverse ([x] ++ aplana d) ++ reverse (aplana i)\r\n             : congr_arg2 (++) (reverse_append [x] (aplana d)).symm rfl\r\n     ... = reverse (aplana i ++ ([x] ++ aplana d))\r\n             : (reverse_append (aplana i) ([x] ++ aplana d)).symm\r\n     ... = reverse ((aplana i ++ [x]) ++ aplana d)\r\n             : congr_arg reverse (append_assoc (aplana i) [x] (aplana d)).symm\r\n     ... = reverse (aplana (nodo x i d))\r\n             : congr_arg reverse (aplana_2 i d x), },\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample :\r\n  aplana (espejo a) = reverse (aplana a) :=\r\nbegin\r\n  induction a with x x i d Hi Hd,\r\n  { calc aplana (espejo (hoja x))\r\n         = aplana (hoja x)\r\n             : by simp only [espejo_1]\r\n     ... = [x]\r\n             : by rw aplana_1\r\n     ... = reverse [x]\r\n             : by rw reverse_singleton\r\n     ... = reverse (aplana (hoja x))\r\n             : by simp only [aplana_1], },\r\n  { calc aplana (espejo (nodo x i d))\r\n         = aplana (nodo x (espejo d) (espejo i))\r\n             : by simp only [espejo_2]\r\n     ... = aplana (espejo d) ++ [x] ++ aplana (espejo i)\r\n             : by rw aplana_2\r\n     ... = reverse (aplana d) ++ [x] ++ reverse (aplana i)\r\n             : by rw [Hi, Hd]\r\n     ... = reverse (aplana d) ++ reverse [x] ++ reverse (aplana i)\r\n             : by simp only [reverse_singleton]\r\n     ... = reverse ([x] ++ aplana d) ++ reverse (aplana i)\r\n             : by simp only [reverse_append]\r\n     ... = reverse (aplana i ++ ([x] ++ aplana d))\r\n             : by simp only [reverse_append]\r\n     ... = reverse (aplana i ++ [x] ++ aplana d)\r\n             : by simp only [append_assoc]\r\n     ... = reverse (aplana (nodo x i d))\r\n             : by simp only [aplana_2], },\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample :\r\n  aplana (espejo a) = reverse (aplana a) :=\r\nbegin\r\n  induction a with x x i d Hi Hd,\r\n  { calc aplana (espejo (hoja x))\r\n         = aplana (hoja x)           : by simp\r\n     ... = [x]                       : by simp\r\n     ... = reverse [x]               : by simp\r\n     ... = reverse (aplana (hoja x)) : by simp, },\r\n  { calc aplana (espejo (nodo x i d))\r\n         = aplana (nodo x (espejo d) (espejo i))\r\n             : by simp\r\n     ... = aplana (espejo d) ++ [x] ++ aplana (espejo i)\r\n             : by simp\r\n     ... = reverse (aplana d) ++ [x] ++ reverse (aplana i)\r\n             : by simp [Hi, Hd]\r\n     ... = reverse (aplana d) ++ reverse [x] ++ reverse (aplana i)\r\n             : by simp\r\n     ... = reverse ([x] ++ aplana d) ++ reverse (aplana i)\r\n             : by simp\r\n     ... = reverse (aplana i ++ ([x] ++ aplana d))\r\n             : by simp\r\n     ... = reverse (aplana i ++ [x] ++ aplana d)\r\n             : by simp\r\n     ... = reverse (aplana (nodo x i d))\r\n             : by simp },\r\nend\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample :\r\n  aplana (espejo a) = reverse (aplana a) :=\r\nbegin\r\n  induction a with x x i d Hi Hd,\r\n  { simp, },\r\n  { calc aplana (espejo (nodo x i d))\r\n         = reverse (aplana d) ++ [x] ++ reverse (aplana i)\r\n             : by simp [Hi, Hd]\r\n     ... = reverse (aplana (nodo x i d))\r\n             : by simp },\r\nend\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nexample :\r\n  aplana (espejo a) = reverse (aplana a) :=\r\nbegin\r\n  induction a with x x i d Hi Hd,\r\n  { simp, },\r\n  { simp [Hi, Hd], },\r\nend\r\n\r\n-- 7\u00aa demostraci\u00f3n\r\nexample :\r\n  aplana (espejo a) = reverse (aplana a) :=\r\nby induction a ; simp [*]\r\n\r\n-- 8\u00aa demostraci\u00f3n\r\nexample :\r\n  aplana (espejo a) = reverse (aplana a) :=\r\narbol.rec_on a\r\n  ( assume x,\r\n    calc aplana (espejo (hoja x))\r\n         = aplana (hoja x)\r\n             : by simp only [espejo_1]\r\n     ... = [x]\r\n             : by rw aplana_1\r\n     ... = reverse [x]\r\n             : by rw reverse_singleton\r\n     ... = reverse (aplana (hoja x))\r\n             : by simp only [aplana_1])\r\n  ( assume x i d,\r\n    assume Hi : aplana (espejo i) = reverse (aplana i),\r\n    assume Hd : aplana (espejo d) = reverse (aplana d),\r\n    calc aplana (espejo (nodo x i d))\r\n         = aplana (nodo x (espejo d) (espejo i))\r\n             : by simp only [espejo_2]\r\n     ... = aplana (espejo d) ++ [x] ++ aplana (espejo i)\r\n             : by rw aplana_2\r\n     ... = reverse (aplana d) ++ [x] ++ reverse (aplana i)\r\n             : by rw [Hi, Hd]\r\n     ... = reverse (aplana d) ++ reverse [x] ++ reverse (aplana i)\r\n             : by simp only [reverse_singleton]\r\n     ... = reverse ([x] ++ aplana d) ++ reverse (aplana i)\r\n             : by simp only [reverse_append]\r\n     ... = reverse (aplana i ++ ([x] ++ aplana d))\r\n             : by simp only [reverse_append]\r\n     ... = reverse (aplana i ++ [x] ++ aplana d)\r\n             : by simp only [append_assoc]\r\n     ... = reverse (aplana (nodo x i d))\r\n             : by simp only [aplana_2])\r\n\r\n-- 9\u00aa demostraci\u00f3n\r\nexample :\r\n  aplana (espejo a) = reverse (aplana 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-- 10\u00aa demostraci\u00f3n\r\nlemma aplana_espejo :\r\n  \u2200 a : arbol \u03b1, aplana (espejo a) = reverse (aplana a)\r\n| (hoja x)     := by simp\r\n| (nodo x i d) := by simp [aplana_espejo i,\r\n                           aplana_espejo d]\r\n\r\nend arbol\r\n<\/pre>\n
Se puede interactuar con la prueba anterior en esta sesi\u00f3n con Lean<\/a>.<\/p>\n
En los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con <pre lang="lean"> y otra con <\/pre>
\n[\/expand]<\/p>\n
[expand title=\u00bbSoluciones con Isabelle\/HOL\u00bb]<\/p>\n
\r\ntheory Razonamiento_sobre_arboles_binarios_Aplanamiento_e_imagen_especular\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\nfun aplana :: \"'a arbol \u21d2 'a list\" where\r\n  \"aplana (hoja x)     = [x]\"\r\n| \"aplana (nodo x i d) = (aplana i) @ [x] @ (aplana d)\"\r\n\r\n(* Lema auxiliar *)\r\n(* ============= *)\r\n\r\n(* 1\u00aa demostraci\u00f3n del lema auxiliar *)\r\nlemma \"rev [x] = [x]\"\r\nproof -\r\n  have \"rev [x] = rev [] @ [x]\"\r\n    by (simp only: rev.simps(2))\r\n  also have \"\u2026 = [] @ [x]\"\r\n    by (simp only: rev.simps(1))\r\n  also have \"\u2026 = [x]\"\r\n    by (simp only: append.simps(1))\r\n  finally show ?thesis\r\n    by this\r\nqed\r\n\r\n(* 2\u00aa demostraci\u00f3n del lema auxiliar *)\r\nlemma rev_unit: \"rev [x] = [x]\"\r\nby simp\r\n\r\n(* Lema principal *)\r\n(* ============== *)\r\n\r\n(* ?\u00aa demostraci\u00f3n *)\r\nlemma\r\n  fixes a :: \"'b arbol\"\r\n  shows \"aplana (espejo a) = rev (aplana a)\" (is \"?P a\")\r\nproof (induct a)\r\n  fix x :: 'b\r\n  have \"aplana (espejo (hoja x)) = aplana (hoja x)\"\r\n    by (simp only: espejo.simps(1))\r\n  also have \"\u2026 = [x]\"\r\n    by (simp only: aplana.simps(1))\r\n  also have \"\u2026 = rev [x]\"\r\n    by (rule rev_unit [symmetric])\r\n  also have \"\u2026 = rev (aplana (hoja x))\"\r\n    by (simp only: aplana.simps(1))\r\n  finally show \"?P (hoja x)\"\r\n    by this\r\nnext\r\n  fix x :: 'b\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 \"aplana (espejo (nodo x i d)) =\r\n          aplana (nodo x (espejo d) (espejo i))\"\r\n      by (simp only: espejo.simps(2))\r\n    also have \"\u2026 = (aplana (espejo d)) @ [x] @ (aplana (espejo i))\"\r\n      by (simp only: aplana.simps(2))\r\n    also have \"\u2026 = (rev (aplana d)) @ [x] @ (rev (aplana i))\"\r\n      by (simp only: h1 h2)\r\n    also have \"\u2026 = rev ((aplana i) @ [x] @ (aplana d))\"\r\n      by (simp only: rev_append rev_unit append_assoc)\r\n    also have \"\u2026 = rev (aplana (nodo x i d))\"\r\n      by (simp only: aplana.simps(2))\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 \"aplana (espejo a) = rev (aplana 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 \"aplana (espejo (nodo x i d)) =\r\n          aplana (nodo x (espejo d) (espejo i))\" by simp\r\n    also have \"\u2026 = (aplana (espejo d)) @ [x] @ (aplana (espejo i))\"\r\n      by simp\r\n    also have \"\u2026 = (rev (aplana d)) @ [x] @ (rev (aplana i))\"\r\n      using h1 h2 by simp\r\n    also have \"\u2026 = rev ((aplana i) @ [x] @ (aplana d))\" by simp\r\n    also have \"\u2026 = rev (aplana (nodo x i d))\" by simp\r\n    finally show ?thesis .\r\n qed\r\nqed\r\n\r\n(* 3\u00aa demostraci\u00f3n *)\r\nlemma \"aplana (espejo a) = rev (aplana a)\"\r\nproof (induct a)\r\ncase (hoja x)\r\nthen show ?case by simp\r\nnext\r\n  case (nodo x i d)\r\n  then show ?case by simp\r\nqed\r\n\r\n(* 4\u00aa demostraci\u00f3n *)\r\nlemma \"aplana (espejo a) = rev (aplana a)\"\r\n  by (induct a) simp_all\r\n\r\nend\r\n<\/pre>\n
En los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con <pre lang="isar"> y otra con <\/pre>
\n[\/expand]<\/p>\n","protected":false},"excerpt":{"rendered":"
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) usando 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 y la lista obtenida aplan\u00e1ndolo (recorri\u00e9ndolo en orden infijo) es [4, 3, 5, 2, 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…<\/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\/758"}],"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=758"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/758\/revisions"}],"predecessor-version":[{"id":759,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/758\/revisions\/759"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=758"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=758"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=758"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}