{"id":746,"date":"2021-09-08T05:00:55","date_gmt":"2021-09-08T03:00:55","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=746"},"modified":"2021-09-08T12:04:01","modified_gmt":"2021-09-08T10:04:01","slug":"asociatividad-de-la-concatenacion-de-listas","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/asociatividad-de-la-concatenacion-de-listas\/","title":{"rendered":"Asociatividad de la concatenaci\u00f3n de listas"},"content":{"rendered":"

En Lean la operaci\u00f3n de concatenaci\u00f3n de listas se representa por (++) y est\u00e1 caracterizada por los siguientes lemas<\/p>\n

\n   nil_append  : [] ++ ys = ys\n   cons_append : (x :: xs) ++ y = x :: (xs ++ ys)\n<\/pre>\n
Demostrar que la concatenaci\u00f3n es asociativa; es decir,<\/p>\n
\n   xs ++ (ys ++ zs) = (xs ++ ys) ++ zs\n<\/pre>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport data.list.basic\nimport tactic\nopen list\n\nvariable  {\u03b1 : Type}\nvariable  (x : \u03b1)\nvariables (xs ys zs : list \u03b1)\n\nexample :\n  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=\nsorry\n<\/pre>\n
[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n
\r\nimport data.list.basic\r\nimport tactic\r\nopen list\r\n\r\nvariable  {\u03b1 : Type}\r\nvariable  (x : \u03b1)\r\nvariables (xs ys zs : list \u03b1)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample :\r\n  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=\r\nbegin\r\n  induction xs with a as HI,\r\n  { calc [] ++ (ys ++ zs)\r\n         = ys ++ zs                : append.equations._eqn_1 (ys ++ zs)\r\n     ... = ([] ++ ys) ++ zs        : congr_arg2 (++) (append.equations._eqn_1 ys) rfl, },\r\n  { calc (a :: as) ++ (ys ++ zs)\r\n         = a :: (as ++ (ys ++ zs)) : append.equations._eqn_2 a as (ys ++ zs)\r\n     ... = a :: ((as ++ ys) ++ zs) : congr_arg2 (::) rfl HI\r\n     ... = (a :: (as ++ ys)) ++ zs : (append.equations._eqn_2 a (as ++ ys) zs).symm\r\n     ... = ((a :: as) ++ ys) ++ zs : congr_arg2 (++) (append.equations._eqn_2 a as ys).symm rfl, },\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample :\r\n  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=\r\nbegin\r\n  induction xs with a as HI,\r\n  { calc [] ++ (ys ++ zs)\r\n         = ys ++ zs                : nil_append (ys ++ zs)\r\n     ... = ([] ++ ys) ++ zs        : congr_arg2 (++) (nil_append ys) rfl, },\r\n  { calc (a :: as) ++ (ys ++ zs)\r\n         = a :: (as ++ (ys ++ zs)) : cons_append a as (ys ++ zs)\r\n     ... = a :: ((as ++ ys) ++ zs) : congr_arg2 (::) rfl HI\r\n     ... = (a :: (as ++ ys)) ++ zs : (cons_append a (as ++ ys) zs).symm\r\n     ... = ((a :: as) ++ ys) ++ zs : congr_arg2 (++) (cons_append a as ys).symm rfl, },\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample :\r\n  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=\r\nbegin\r\n  induction xs with a as HI,\r\n  { calc [] ++ (ys ++ zs)\r\n         = ys ++ zs                : by rw nil_append\r\n     ... = ([] ++ ys) ++ zs        : by rw nil_append, },\r\n  { calc (a :: as) ++ (ys ++ zs)\r\n         = a :: (as ++ (ys ++ zs)) : by rw cons_append\r\n     ... = a :: ((as ++ ys) ++ zs) : by rw HI\r\n     ... = (a :: (as ++ ys)) ++ zs : by rw cons_append\r\n     ... = ((a :: as) ++ ys) ++ zs : by rw \u2190 cons_append, },\r\nend\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample :\r\n  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=\r\nbegin\r\n  induction xs with a as HI,\r\n  { calc [] ++ (ys ++ zs)\r\n         = ys ++ zs                : rfl\r\n     ... = ([] ++ ys) ++ zs        : rfl, },\r\n  { calc (a :: as) ++ (ys ++ zs)\r\n         = a :: (as ++ (ys ++ zs)) : rfl\r\n     ... = a :: ((as ++ ys) ++ zs) : by rw HI\r\n     ... = (a :: (as ++ ys)) ++ zs : rfl\r\n     ... = ((a :: as) ++ ys) ++ zs : rfl, },\r\nend\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample :\r\n  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=\r\nbegin\r\n  induction xs with a as HI,\r\n  { calc [] ++ (ys ++ zs)\r\n         = ys ++ zs                : by simp\r\n     ... = ([] ++ ys) ++ zs        : by simp, },\r\n  { calc (a :: as) ++ (ys ++ zs)\r\n         = a :: (as ++ (ys ++ zs)) : by simp\r\n     ... = a :: ((as ++ ys) ++ zs) : congr_arg (cons a) HI\r\n     ... = (a :: (as ++ ys)) ++ zs : by simp\r\n     ... = ((a :: as) ++ ys) ++ zs : by simp, },\r\nend\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nexample :\r\n  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=\r\nbegin\r\n  induction xs with a as HI,\r\n  { by simp, },\r\n  { by exact (cons_inj a).mpr HI, },\r\nend\r\n\r\n-- 7\u00aa demostraci\u00f3n\r\nexample :\r\n  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=\r\nbegin\r\n  induction xs with a as HI,\r\n  { rw nil_append,\r\n    rw nil_append, },\r\n  { rw cons_append,\r\n    rw HI,\r\n    rw cons_append,\r\n    rw cons_append, },\r\nend\r\n\r\n-- 8\u00aa demostraci\u00f3n\r\nexample :\r\n  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=\r\nlist.rec_on xs\r\n  ( show [] ++ (ys ++ zs) = ([] ++ ys) ++ zs,\r\n      from calc\r\n        [] ++ (ys ++ zs)\r\n            = ys ++ zs         : by rw nil_append\r\n        ... = ([] ++ ys) ++ zs : by rw nil_append )\r\n  ( assume a as,\r\n    assume HI : as ++ (ys ++ zs) = (as ++ ys) ++ zs,\r\n    show (a :: as) ++ (ys  ++ zs) = ((a :: as) ++ ys) ++ zs,\r\n      from calc\r\n        (a :: as) ++ (ys ++ zs)\r\n            = a :: (as ++ (ys ++ zs)) : by rw cons_append\r\n        ... = a :: ((as ++ ys) ++ zs) : by rw HI\r\n        ... = (a :: (as ++ ys)) ++ zs : by rw cons_append\r\n        ... = ((a :: as) ++ ys) ++ zs : by rw \u2190 cons_append)\r\n\r\n-- 9\u00aa demostraci\u00f3n\r\nexample :\r\n  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=\r\nlist.rec_on xs\r\n  (by simp)\r\n  (by simp [*])\r\n\r\n-- 10\u00aa demostraci\u00f3n\r\nlemma conc_asoc_1 :\r\n  \u2200 xs, xs ++ (ys ++ zs) = (xs ++ ys) ++ zs\r\n| [] := by calc\r\n    [] ++ (ys ++ zs)\r\n        = ys ++ zs         : by rw nil_append\r\n    ... = ([] ++ ys) ++ zs : by rw nil_append\r\n| (a :: as) := by calc\r\n    (a :: as) ++ (ys ++ zs)\r\n        = a :: (as ++ (ys ++ zs)) : by rw cons_append\r\n    ... = a :: ((as ++ ys) ++ zs) : by rw conc_asoc_1\r\n    ... = (a :: (as ++ ys)) ++ zs : by rw cons_append\r\n    ... = ((a :: as) ++ ys) ++ zs : by rw \u2190 cons_append\r\n\r\n-- 11\u00aa demostraci\u00f3n\r\nexample :\r\n  (xs ++ ys) ++ zs = xs ++ (ys ++ zs) :=\r\n-- by library_search\r\nappend_assoc xs ys zs\r\n\r\n-- 12\u00aa demostraci\u00f3n\r\nexample :\r\n  (xs ++ ys) ++ zs = xs ++ (ys ++ zs) :=\r\nby induction xs ; simp [*]\r\n\r\n-- 13\u00aa demostraci\u00f3n\r\nexample :\r\n  (xs ++ ys) ++ zs = xs ++ (ys ++ zs) :=\r\nby simp\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 Asociatividad_de_la_concatenacion_de_listas\r\nimports Main\r\nbegin\r\n\r\n(* 1\u00aa demostraci\u00f3n *)\r\nlemma \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\r\nproof (induct xs)\r\n  have \"[] @ (ys @ zs) = ys @ zs\"\r\n    by (simp only: append_Nil)\r\n  also have \"\u2026 = ([] @ ys) @ zs\"\r\n    by (simp only: append_Nil)\r\n  finally show \"[] @ (ys @ zs) = ([] @ ys) @ zs\"\r\n    by this\r\nnext\r\n  fix x xs\r\n  assume HI : \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\r\n  have \"(x # xs) @ (ys @ zs) = x # (xs @ (ys @ zs))\"\r\n    by (simp only: append_Cons)\r\n  also have \"\u2026 = x # ((xs @ ys) @ zs)\"\r\n    by (simp only: HI)\r\n  also have \"\u2026 = (x # (xs @ ys)) @ zs\"\r\n    by (simp only: append_Cons)\r\n  also have \"\u2026 = ((x # xs) @ ys) @ zs\"\r\n    by (simp only: append_Cons)\r\n  finally show \"(x # xs) @ (ys @ zs) = ((x # xs) @ ys) @ zs\"\r\n    by this\r\nqed\r\n\r\n(* 2\u00aa demostraci\u00f3n *)\r\nlemma \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\r\nproof (induct xs)\r\n  have \"[] @ (ys @ zs) = ys @ zs\" by simp\r\n  also have \"\u2026 = ([] @ ys) @ zs\" by simp\r\n  finally show \"[] @ (ys @ zs) = ([] @ ys) @ zs\" .\r\nnext\r\n  fix x xs\r\n  assume HI : \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\r\n  have \"(x # xs) @ (ys @ zs) = x # (xs @ (ys @ zs))\" by simp\r\n  also have \"\u2026 = x # ((xs @ ys) @ zs)\" by simp\r\n  also have \"\u2026 = (x # (xs @ ys)) @ zs\" by simp\r\n  also have \"\u2026 = ((x # xs) @ ys) @ zs\" by simp\r\n  finally show \"(x # xs) @ (ys @ zs) = ((x # xs) @ ys) @ zs\" .\r\nqed\r\n\r\n(* 3\u00aa demostraci\u00f3n *)\r\nlemma \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\r\nproof (induct xs)\r\n  show \"[] @ (ys @ zs) = ([] @ ys) @ zs\" by simp\r\nnext\r\n  fix x xs\r\n  assume \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\r\n  then show \"(x # xs) @ (ys @ zs) = ((x # xs) @ ys) @ zs\" by simp\r\nqed\r\n\r\n(* 4\u00aa demostraci\u00f3n *)\r\nlemma \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\r\nproof (induct xs)\r\n  case Nil\r\n  then show ?case by simp\r\nnext\r\n  case (Cons a xs)\r\n  then show ?case by simp\r\nqed\r\n\r\n(* 5\u00aa demostraci\u00f3n *)\r\nlemma \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\r\n  by (rule append_assoc [symmetric])\r\n\r\n(* 6\u00aa demostraci\u00f3n *)\r\nlemma \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\r\n  by (induct xs) simp_all\r\n\r\n(* 7\u00aa demostraci\u00f3n *)\r\nlemma \"xs @ (ys @ zs) = (xs @ ys) @ zs\"\r\n  by simp\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":"
En Lean la operaci\u00f3n de concatenaci\u00f3n de listas se representa por (++) y est\u00e1 caracterizada por los siguientes lemas nil_append : [] ++ ys = ys cons_append : (x :: xs) ++ y = x :: (xs ++ ys) Demostrar que la concatenaci\u00f3n es asociativa; es decir, xs ++ (ys ++ zs) = (xs ++ ys) ++ zs Para ello, completar la siguiente teor\u00eda de Lean: import data.list.basic import tactic open list variable {\u03b1 : Type} variable (x : \u03b1) variables (xs ys zs : list \u03b1) example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := sorry [expand title=\u00bbSoluciones con Lean\u00bb] import data.list.basic import tactic open list variable {\u03b1 : Type} variable (x : \u03b1) variables (xs ys zs :…<\/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":[105,227],"tags":[245,244,243,177,100,62,242,276,277,238,84,237,239,49,169,241,240,236,147,111,99,72],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/746"}],"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=746"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/746\/revisions"}],"predecessor-version":[{"id":755,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/746\/revisions\/755"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=746"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=746"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=746"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}