{"id":750,"date":"2021-09-10T05:00:43","date_gmt":"2021-09-10T03:00:43","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=750"},"modified":"2021-09-06T18:25:07","modified_gmt":"2021-09-06T16:25:07","slug":"pruebas-de-take-n-xs-drop-n-xs-xs","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/pruebas-de-take-n-xs-drop-n-xs-xs\/","title":{"rendered":"Pruebas de take n xs ++ drop n xs = xs"},"content":{"rendered":"<p>En Lean est\u00e1n definidas las funciones<\/p>\n<pre lang=\"text\">\n   take : nat \u2192 list \u03b1 \u2192 nat\n   drop : nat \u2192 list \u03b1 \u2192 nat\n   (++) : list \u03b1 \u2192 list \u03b1 \u2192 list \u03b1\n<\/pre>\n<p>tales que<\/p>\n<ul>\n<li>(take n xs) es la lista formada por los n primeros elementos de xs. Por ejemplo,<\/li>\n<\/ul>\n<pre lang=\"text\">\n     take 2 [3,5,1,9,7] = [3,5]\n<\/pre>\n<ul>\n<li>(drop n xs) es la lista formada eliminando los n primeros elementos de xs. Por ejemplo,<\/li>\n<\/ul>\n<pre lang=\"text\">\n     drop 2 [3,5,1,9,7] = [1,9,7]\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     [3,5] ++ [1,9,7] = [3,5,1,9,7]\n<\/pre>\n<p>Dichas funciones est\u00e1n caracterizadas por los siguientes lemas:<\/p>\n<pre lang=\"text\">\n   take_zero   : take 0 xs = []\n   take_nil    : take n [] = []\n   take_cons   : take (succ n) (x :: xs) = x :: take n xs\n   drop_zero   : drop 0 xs = xs\n   drop_nil    : drop n [] = []\n   drop_cons   : drop (succ n) (x :: xs) = drop n xs := rfl\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   take n xs ++ drop n xs = xs\n<\/pre>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport data.list.basic\nimport tactic\nopen list nat\n\nvariable {\u03b1 : Type}\nvariable (x : \u03b1)\nvariable (xs : list \u03b1)\nvariable (n : \u2115)\n\nlemma drop_zero : drop 0 xs = xs := rfl\nlemma drop_cons : drop (succ n) (x :: xs) = drop n xs := rfl\n\nexample :\n  take n xs ++ drop n xs = xs :=\nsorry\n<\/pre>\n<p>[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n<pre lang=\"lean\">\r\nimport data.list.basic\r\nimport tactic\r\nopen list\r\nopen nat\r\n\r\nvariable {\u03b1 : Type}\r\nvariable (n : \u2115)\r\nvariable (x : \u03b1)\r\nvariable (xs : list \u03b1)\r\n\r\nlemma drop_zero : drop 0 xs = xs := rfl\r\nlemma drop_cons : drop (succ n) (x :: xs) = drop n xs := rfl\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample :\r\n  take n xs ++ drop n xs = xs :=\r\nbegin\r\n  induction n with m HI1 generalizing xs,\r\n  { rw take_zero,\r\n    rw drop_zero,\r\n    rw nil_append, },\r\n  { induction xs with a as HI2,\r\n    { rw take_nil,\r\n      rw drop_nil,\r\n      rw nil_append, },\r\n    { rw take_cons,\r\n      rw drop_cons,\r\n      rw cons_append,\r\n      rw (HI1 as), }, },\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample :\r\n  take n xs ++ drop n xs = xs :=\r\nbegin\r\n  induction n with m HI1 generalizing xs,\r\n  { calc take 0 xs ++ drop 0 xs\r\n         = [] ++ drop 0 xs        : by rw take_zero\r\n     ... = [] ++ xs               : by rw drop_zero\r\n     ... = xs                     : by rw nil_append, },\r\n  { induction xs with a as HI2,\r\n    { calc take (succ m) [] ++ drop (succ m) []\r\n           = ([] : list \u03b1) ++ drop (succ m) [] : by rw take_nil\r\n       ... = [] ++ []                          : by rw drop_nil\r\n       ... = []                                : by rw nil_append, },\r\n    { calc take (succ m) (a :: as) ++ drop (succ m) (a :: as)\r\n           = (a :: take m as) ++ drop (succ m) (a :: as) : by rw take_cons\r\n       ... = (a :: take m as) ++ drop m as               : by rw drop_cons\r\n       ... = a :: (take m as ++ drop m as)               : by rw cons_append\r\n       ... = a :: as                                     : by rw (HI1 as), }, },\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample :\r\n  take n xs ++ drop n xs = xs :=\r\nbegin\r\n  induction n with m HI1 generalizing xs,\r\n  { simp, },\r\n  { induction xs with a as HI2,\r\n    { simp, },\r\n    { simp [HI1 as], }, },\r\nend\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nlemma conc_take_drop_1 :\r\n  \u2200 (n : \u2115) (xs : list \u03b1), take n xs ++ drop n xs = xs\r\n| 0 xs := by calc\r\n    take 0 xs ++ drop 0 xs\r\n        = [] ++ drop 0 xs   : by rw take_zero\r\n    ... = [] ++ xs          : by rw drop_zero\r\n    ... = xs                : by rw nil_append\r\n| (succ m) [] := by calc\r\n    take (succ m) [] ++ drop (succ m) []\r\n        = ([] : list \u03b1) ++ drop (succ m) [] : by rw take_nil\r\n    ... = [] ++ []                          : by rw drop_nil\r\n    ... = []                                : by rw nil_append\r\n| (succ m) (a :: as) := by calc\r\n    take (succ m) (a :: as) ++ drop (succ m) (a :: as)\r\n        = (a :: take m as) ++ drop (succ m) (a :: as)    : by rw take_cons\r\n    ... = (a :: take m as) ++ drop m as                  : by rw drop_cons\r\n    ... = a :: (take m as ++ drop m as)                  : by rw cons_append\r\n    ... = a :: as                                        : by rw conc_take_drop_1\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nlemma conc_take_drop_2 :\r\n  \u2200 (n : \u2115) (xs : list \u03b1), take n xs ++ drop n xs = xs\r\n| 0        xs        := by simp\r\n| (succ m) []        := by simp\r\n| (succ m) (a :: as) := by simp [conc_take_drop_2]\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nlemma conc_take_drop_3 :\r\n  \u2200 (n : \u2115) (xs : list \u03b1), take n xs ++ drop n xs = xs\r\n| 0        xs        := rfl\r\n| (succ m) []        := rfl\r\n| (succ m) (a :: as) := congr_arg (cons a) (conc_take_drop_3 m as)\r\n\r\n-- 7\u00aa demostraci\u00f3n\r\nexample : take n xs ++ drop n xs = xs :=\r\n-- by library_search\r\ntake_append_drop n xs\r\n\r\n-- 8\u00aa demostraci\u00f3n\r\nexample : take n xs ++ drop n xs = xs :=\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_take_n_xs_++_drop_n_xs_Ig_xs.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_take_n_xs_++_drop_n_xs_Ig_xs\"\r\nimports Main\r\nbegin\r\n\r\nfun take' :: \"nat \u21d2 'a list \u21d2 'a list\" where\r\n  \"take' n []           = []\"\r\n| \"take' 0 xs           = []\"\r\n| \"take' (Suc n) (x#xs) = x # (take' n xs)\"\r\n\r\nfun drop' :: \"nat \u21d2 'a list \u21d2 'a list\" where\r\n  \"drop' n []           = []\"\r\n| \"drop' 0 xs           = xs\"\r\n| \"drop' (Suc n) (x#xs) = drop' n xs\"\r\n\r\n(* 1\u00aa demostraci\u00f3n *)\r\nlemma \"take' n xs @ drop' n xs = xs\"\r\nproof (induct rule: take'.induct)\r\n  fix n\r\n  have \"take' n [] @ drop' n [] = [] @ drop' n []\"\r\n    by (simp only: take'.simps(1))\r\n  also have \"\u2026 = drop' n []\"\r\n    by (simp only: append.simps(1))\r\n  also have \"\u2026 = []\"\r\n    by (simp only: drop'.simps(1))\r\n  finally show \"take' n [] @ drop' n [] = []\"\r\n    by this\r\nnext\r\n  fix x :: 'a and xs :: \"'a list\"\r\n  have \"take' 0 (x#xs) @ drop' 0 (x#xs) =\r\n        [] @ drop' 0 (x#xs)\"\r\n    by (simp only: take'.simps(2))\r\n  also have \"\u2026 = drop' 0 (x#xs)\"\r\n    by  (simp only: append.simps(1))\r\n  also have \"\u2026 = x # xs\"\r\n    by  (simp only: drop'.simps(2))\r\n  finally show \"take' 0 (x#xs) @ drop' 0 (x#xs) = x#xs\"\r\n    by this\r\nnext\r\n  fix n :: nat and x :: 'a and xs :: \"'a list\"\r\n  assume HI: \"take' n xs @ drop' n xs = xs\"\r\n  have \"take' (Suc n) (x # xs) @ drop' (Suc n) (x # xs) =\r\n        (x # (take' n xs)) @ drop' n xs\"\r\n    by (simp only: take'.simps(3)\r\n                   drop'.simps(3))\r\n  also have \"\u2026 = x # (take' n xs @ drop' n xs)\"\r\n    by (simp only: append.simps(2))\r\n  also have \"\u2026 = x#xs\"\r\n    by (simp only: HI)\r\n  finally show \"take' (Suc n) (x#xs) @ drop' (Suc n) (x#xs) =\r\n                x#xs\"\r\n    by this\r\nqed\r\n\r\n(* 2\u00aa demostraci\u00f3n *)\r\nlemma \"take' n xs @ drop' n xs = xs\"\r\nproof (induct rule: take'.induct)\r\ncase (1 n)\r\n  then show ?case by simp\r\nnext\r\n  case (2 x xs)\r\n  then show ?case by simp\r\nnext\r\n  case (3 n x xs)\r\n  then show ?case by simp\r\nqed\r\n\r\n(* 3\u00aa demostraci\u00f3n *)\r\nlemma \"take' n xs @ drop' n xs = xs\"\r\nby (induct rule: take'.induct) 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>En Lean est\u00e1n definidas las funciones take : nat \u2192 list \u03b1 \u2192 nat drop : nat \u2192 list \u03b1 \u2192 nat (++) : list \u03b1 \u2192 list \u03b1 \u2192 list \u03b1 tales que (take n xs) es la lista formada por los n primeros elementos de xs. Por ejemplo, take 2 [3,5,1,9,7] = [3,5] (drop n xs) es la lista formada eliminando los n primeros elementos de xs. Por ejemplo, drop 2 [3,5,1,9,7] = [1,9,7] (xs ++ ys) es la lista obtenida concatenando xs e ys. Por ejemplo. [3,5] ++ [1,9,7] = [3,5,1,9,7] Dichas funciones est\u00e1n caracterizadas por los siguientes lemas: take_zero : take 0 xs = [] take_nil : take n [] = [] take_cons : take (succ n) (x :: xs) =&#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":[264,177,100,254,98,198,238,237,262,260,258,169,236,111,99,263,261,259,257],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/750"}],"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=750"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/750\/revisions"}],"predecessor-version":[{"id":751,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/750\/revisions\/751"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=750"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=750"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=750"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}