{"id":748,"date":"2021-09-09T05:00:33","date_gmt":"2021-09-09T03:00:33","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=748"},"modified":"2021-09-05T19:26:35","modified_gmt":"2021-09-05T17:26:35","slug":"pruebas-de-length-xs-ys-length-xs-length-ys","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/pruebas-de-length-xs-ys-length-xs-length-ys\/","title":{"rendered":"Pruebas de length (xs ++ ys) = length xs + length ys"},"content":{"rendered":"<p>En Lean est\u00e1n definidas las funciones<\/p>\n<pre lang=\"text\">\n   length : list \u03b1 \u2192 nat\n   (++)   : list \u03b1 \u2192 list \u03b1 \u2192 list \u03b1\n<\/pre>\n<p>tales que<\/p>\n<ul>\n<li>(length xs) es la longitud de xs. Por ejemplo,<\/li>\n<\/ul>\n<pre lang=\"text\">\n     length [2,3,5,3] = 4\n<\/pre>\n<ul>\n<li>(xs ++ ys) es la lista obtenida concatenando xs e ys. Por ejemplo.<\/li>\n<\/ul>\n<pre lang=\"text\">\n     [1,2] ++ [2,3,5,3] = [1,2,2,3,5,3]\n<\/pre>\n<p>Dichas funciones est\u00e1n caracterizadas por los siguientes lemas:<\/p>\n<pre lang=\"text\">\n   length_nil  : length [] = 0\n   length_cons : length (x :: xs) = length xs + 1\n   nil_append  : [] ++ ys = ys\n   cons_append : (x :: xs) ++ y = x :: (xs ++ ys)\n<\/pre>\n<p>Demostrar que<\/p>\n<pre lang=\"text\">\n   length (xs ++ ys) = length xs + length ys\n<\/pre>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport tactic\nopen list\n\nvariable  {\u03b1 : Type}\nvariable  (x : \u03b1)\nvariables (xs ys zs : list \u03b1)\n\nlemma length_nil  : length ([] : list \u03b1) = 0 := rfl\n\nexample :\n  length (xs ++ ys) = length xs + length ys :=\nsorry\n<\/pre>\n<p>[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n<pre lang=\"lean\">\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\nlemma length_nil  : length ([] : list \u03b1) = 0 := rfl\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample :\r\n  length (xs ++ ys) = length xs + length ys :=\r\nbegin\r\n  induction xs with a as HI,\r\n  { rw nil_append,\r\n    rw length_nil,\r\n    rw zero_add, },\r\n  { rw cons_append,\r\n    rw length_cons,\r\n    rw HI,\r\n    rw length_cons,\r\n    rw add_assoc,\r\n    rw add_comm (length ys),\r\n    rw add_assoc, },\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample :\r\n  length (xs ++ ys) = length xs + length ys :=\r\nbegin\r\n  induction xs with a as HI,\r\n  { rw nil_append,\r\n    rw length_nil,\r\n    rw zero_add, },\r\n  { rw cons_append,\r\n    rw length_cons,\r\n    rw HI,\r\n    rw length_cons,\r\n    -- library_search,\r\n    exact add_right_comm (length as) (length ys) 1 },\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample :\r\n  length (xs ++ ys) = length xs + length ys :=\r\nbegin\r\n  induction xs with a as HI,\r\n  { rw nil_append,\r\n    rw length_nil,\r\n    rw zero_add, },\r\n  { rw cons_append,\r\n    rw length_cons,\r\n    rw HI,\r\n    rw length_cons,\r\n    -- by hint,\r\n    linarith, },\r\nend\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample :\r\n  length (xs ++ ys) = length xs + length ys :=\r\nbegin\r\n  induction xs with a as HI,\r\n  { simp, },\r\n  { simp [HI],\r\n    linarith, },\r\nend\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample :\r\n  length (xs ++ ys) = length xs + length ys :=\r\nbegin\r\n  induction xs with a as HI,\r\n  { simp, },\r\n  { finish [HI],},\r\nend\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nexample :\r\n  length (xs ++ ys) = length xs + length ys :=\r\nby induction xs ; finish [*]\r\n\r\n-- 7\u00aa demostraci\u00f3n\r\nexample :\r\n  length (xs ++ ys) = length xs + length ys :=\r\nbegin\r\n  induction xs with a as HI,\r\n  { calc length ([] ++ ys)\r\n         = length ys                    : congr_arg length (nil_append ys)\r\n     ... = 0 + length ys                : (zero_add (length ys)).symm\r\n     ... = length [] + length ys        : congr_arg2 (+) length_nil.symm rfl, },\r\n  { calc length ((a :: as) ++ ys)\r\n         = length (a :: (as ++ ys))     : congr_arg length (cons_append a as ys)\r\n     ... = length (as ++ ys) + 1        : length_cons a (as ++ ys)\r\n     ... = (length as + length ys) + 1  : congr_arg2 (+) HI rfl\r\n     ... = (length as + 1) + length ys  : add_right_comm (length as) (length ys) 1\r\n     ... = length (a :: as) + length ys : congr_arg2 (+) (length_cons a as).symm rfl, },\r\nend\r\n\r\n-- 8\u00aa demostraci\u00f3n\r\nexample :\r\n  length (xs ++ ys) = length xs + length ys :=\r\nbegin\r\n  induction xs with a as HI,\r\n  { calc length ([] ++ ys)\r\n         = length ys                    : by rw nil_append\r\n     ... = 0 + length ys                : (zero_add (length ys)).symm\r\n     ... = length [] + length ys        : by rw length_nil },\r\n  { calc length ((a :: as) ++ ys)\r\n         = length (a :: (as ++ ys))     : by rw cons_append\r\n     ... = length (as ++ ys) + 1        : by rw length_cons\r\n     ... = (length as + length ys) + 1  : by rw HI\r\n     ... = (length as + 1) + length ys  : add_right_comm (length as) (length ys) 1\r\n     ... = length (a :: as) + length ys : by rw length_cons, },\r\nend\r\n\r\n-- 9\u00aa demostraci\u00f3n\r\nexample :\r\n  length (xs ++ ys) = length xs + length ys :=\r\nlist.rec_on xs\r\n  ( show length ([] ++ ys) = length [] + length ys, from\r\n      calc length ([] ++ ys)\r\n           = length ys                    : by rw nil_append\r\n       ... = 0 + length ys                : by exact (zero_add (length ys)).symm\r\n       ... = length [] + length ys        : by rw length_nil )\r\n  ( assume a as,\r\n    assume HI : length (as ++ ys) = length as + length ys,\r\n    show length ((a :: as) ++ ys) = length (a :: as) + length ys, from\r\n      calc length ((a :: as) ++ ys)\r\n           = length (a :: (as ++ ys))     : by rw cons_append\r\n       ... = length (as ++ ys) + 1        : by rw length_cons\r\n       ... = (length as + length ys) + 1  : by rw HI\r\n       ... = (length as + 1) + length ys  : by exact add_right_comm (length as) (length ys) 1\r\n       ... = length (a :: as) + length ys : by rw length_cons)\r\n\r\n-- 10\u00aa demostraci\u00f3n\r\nexample :\r\n  length (xs ++ ys) = length xs + length ys :=\r\nlist.rec_on xs\r\n  ( by simp)\r\n  ( \u03bb a as HI, by simp [HI, add_right_comm])\r\n\r\n-- 11\u00aa demostraci\u00f3n\r\nlemma longitud_conc_1 :\r\n  \u2200 xs, length (xs ++ ys) = length xs + length ys\r\n| [] := by calc\r\n    length ([] ++ ys)\r\n        = length ys                    : by rw nil_append\r\n    ... = 0 + length ys                : by rw zero_add\r\n    ... = length [] + length ys        : by rw length_nil\r\n| (a :: as) := by calc\r\n    length ((a :: as) ++ ys)\r\n        = length (a :: (as ++ ys))     : by rw cons_append\r\n    ... = length (as ++ ys) + 1        : by rw length_cons\r\n    ... = (length as + length ys) + 1  : by rw longitud_conc_1\r\n    ... = (length as + 1) + length ys  : by exact add_right_comm (length as) (length ys) 1\r\n    ... = length (a :: as) + length ys : by rw length_cons\r\n\r\n-- 12\u00aa demostraci\u00f3n\r\nlemma longitud_conc_2 :\r\n  \u2200 xs, length (xs ++ ys) = length xs + length ys\r\n| []        := by simp\r\n| (a :: as) := by simp [longitud_conc_2 as, add_right_comm]\r\n\r\n-- 13\u00aa demostraci\u00f3n\r\nexample :\r\n  length (xs ++ ys) = length xs + length ys :=\r\n-- by library_search\r\nlength_append xs ys\r\n\r\n-- 14\u00aa demostraci\u00f3n\r\nexample :\r\n  length (xs ++ ys) = length xs + length ys :=\r\nby simp\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_length(xs_++_ys)_Ig_length_xs+length_ys.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_length(xs_++_ys)_Ig_length_xs+length_ys\"\r\nimports Main\r\nbegin\r\n\r\n(* 1\u00aa demostraci\u00f3n *)\r\nlemma \"length (xs @ ys) = length xs + length ys\"\r\nproof (induct xs)\r\n  have \"length ([] @ ys) = length ys\"\r\n    by (simp only: append_Nil)\r\n  also have \"\u2026 = 0 + length ys\"\r\n    by (rule add_0 [symmetric])\r\n  also have \"\u2026 = length [] + length ys\"\r\n    by (simp only: list.size(3))\r\n  finally show \"length ([] @ ys) = length [] + length ys\"\r\n    by this\r\nnext\r\n  fix x xs\r\n  assume HI : \"length (xs @ ys) = length xs + length ys\"\r\n  have \"length ((x # xs) @ ys) =\r\n        length (x # (xs @ ys))\"\r\n    by (simp only: append_Cons)\r\n  also have \"\u2026 = length (xs @ ys) + 1\"\r\n    by (simp only: list.size(4))\r\n  also have \"\u2026 = (length xs + length ys) + 1\"\r\n    by (simp only: HI)\r\n  also have \"\u2026 = (length xs + 1) + length ys\"\r\n    by (simp only: add.assoc add.commute)\r\n  also have \"\u2026 = length (x # xs) + length ys\"\r\n    by (simp only: list.size(4))\r\n  then show \"length ((x # xs) @ ys) = length (x # xs) + length ys\"\r\n    by simp\r\nqed\r\n\r\n(* 2\u00aa demostraci\u00f3n *)\r\nlemma \"length (xs @ ys) = length xs + length ys\"\r\nproof (induct xs)\r\n  show \"length ([] @ ys) = length [] + length ys\"\r\n    by simp\r\nnext\r\n  fix x xs\r\n  assume \"length (xs @ ys) = length xs + length ys\"\r\n  then show \"length ((x # xs) @ ys) = length (x # xs) + length ys\"\r\n    by simp\r\nqed\r\n\r\n(* 3\u00aa demostraci\u00f3n *)\r\nlemma \"length (xs @ ys) = length xs + length ys\"\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(* 4\u00aa demostraci\u00f3n *)\r\nlemma \"length (xs @ ys) = length xs + length ys\"\r\nby (induct xs) simp_all\r\n\r\n(* 5\u00aa demostraci\u00f3n *)\r\nlemma \"length (xs @ ys) = length xs + length ys\"\r\nby (fact length_append)\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>En Lean est\u00e1n definidas las funciones length : list \u03b1 \u2192 nat (++) : list \u03b1 \u2192 list \u03b1 \u2192 list \u03b1 tales que (length xs) es la longitud de xs. Por ejemplo, length [2,3,5,3] = 4 (xs ++ ys) es la lista obtenida concatenando xs e ys. Por ejemplo. [1,2] ++ [2,3,5,3] = [1,2,2,3,5,3] Dichas funciones est\u00e1n caracterizadas por los siguientes lemas: length_nil : length [] = 0 length_cons : length (x :: xs) = length xs + 1 nil_append : [] ++ ys = ys cons_append : (x :: xs) ++ y = x :: (xs ++ ys) Demostrar que length (xs ++ ys) = length xs + length ys Para ello, completar la siguiente teor\u00eda de Lean: import tactic open list variable&#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":[105,227],"tags":[252,253,214,244,243,255,177,256,233,100,254,62,98,248,249,250,198,238,84,237,125,169,228,251,247,89,241,236,147,111,99,72,246],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/748"}],"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=748"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/748\/revisions"}],"predecessor-version":[{"id":749,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/748\/revisions\/749"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=748"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=748"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=748"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}