{"id":752,"date":"2021-09-11T05:00:06","date_gmt":"2021-09-11T03:00:06","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=752"},"modified":"2021-09-07T18:14:53","modified_gmt":"2021-09-07T16:14:53","slug":"pruebas-de-equivalencia-de-definiciones-de-inversa","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/pruebas-de-equivalencia-de-definiciones-de-inversa\/","title":{"rendered":"Pruebas de equivalencia de definiciones de inversa"},"content":{"rendered":"

En Lean, est\u00e1 definida la funci\u00f3n<\/p>\n

\n   reverse : list \u03b1 \u2192 list \u03b1\n<\/pre>\n
tal que (reverse xs) es la lista obtenida invirtiendo el orden de los elementos de xs. Por ejemplo,<\/p>\n
\n   reverse  [3,2,5,1] = [1,5,2,3]\n<\/pre>\n
Su definici\u00f3n es<\/p>\n
\n   def reverse_core : list \u03b1 \u2192 list \u03b1 \u2192 list \u03b1\n   | []     r := r\n   | (a::l) r := reverse_core l (a::r)\n\n   def reverse : list \u03b1 \u2192 list \u03b1 :=\n   \u03bb l, reverse_core l []\n<\/pre>\n
Una definici\u00f3n alternativa es<\/p>\n
\n   def inversa : list \u03b1 \u2192 list \u03b1\n   | []        := []\n   | (x :: xs) := inversa xs ++ [x]\n<\/pre>\n
Demostrar que las dos definiciones son equivalentes; es decir,<\/p>\n
\n   reverse xs = inversa xs\n<\/pre>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport data.list.basic\nopen list\n\nvariable  {\u03b1 : Type*}\nvariable  (x : \u03b1)\nvariables (xs ys : list \u03b1)\n\ndef inversa : list \u03b1 \u2192 list \u03b1\n| []        := []\n| (x :: xs) := inversa xs ++ [x]\n\nexample : reverse xs = inversa xs :=\nsorry\n<\/pre>\n
[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n
\r\nimport data.list.basic\r\nopen list\r\n\r\nvariable  {\u03b1 : Type*}\r\nvariable  (x : \u03b1)\r\nvariables (xs ys : list \u03b1)\r\n\r\n-- Definici\u00f3n y reglas de simplificaci\u00f3n de inversa\r\n-- ================================================\r\n\r\ndef inversa : list \u03b1 \u2192 list \u03b1\r\n| []        := []\r\n| (x :: xs) := inversa xs ++ [x]\r\n\r\n@[simp]\r\nlemma inversa_nil :\r\n  inversa ([] : list \u03b1) = [] :=\r\nrfl\r\n\r\n@[simp]\r\nlemma inversa_cons :\r\n  inversa (x :: xs) = inversa xs ++ [x] :=\r\nrfl\r\n\r\n-- Reglas de simplificaci\u00f3n de reverse_core\r\n-- ========================================\r\n\r\n@[simp]\r\nlemma reverse_core_nil :\r\n  reverse_core [] ys = ys :=\r\nrfl\r\n\r\n@[simp]\r\nlemma reverse_core_cons :\r\n  reverse_core (x :: xs) ys = reverse_core xs (x :: ys) :=\r\nrfl\r\n\r\n-- Lema auxiliar: reverse_core xs ys = (inversa xs) ++ ys\r\n-- ======================================================\r\n\r\n-- 1\u00aa demostraci\u00f3n del lema auxiliar\r\nexample :\r\n  reverse_core xs ys = (inversa xs) ++ ys :=\r\nbegin\r\n  induction xs with a as HI generalizing ys,\r\n  { calc reverse_core [] ys\r\n         = ys                        : reverse_core_nil ys\r\n     ... = [] ++ ys                  : (nil_append ys).symm\r\n     ... = inversa [] ++ ys          : congr_arg2 (++) inversa_nil.symm rfl, },\r\n  { calc reverse_core (a :: as) ys\r\n         = reverse_core as (a :: ys) : reverse_core_cons a as ys\r\n     ... = inversa as ++ (a :: ys)   : (HI (a :: ys))\r\n     ... = inversa as ++ ([a] ++ ys) : congr_arg2 (++) rfl singleton_append\r\n     ... = (inversa as ++ [a]) ++ ys : (append_assoc (inversa as) [a] ys).symm\r\n     ... = inversa (a :: as) ++ ys   : congr_arg2 (++) (inversa_cons a as).symm rfl},\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n del lema auxiliar\r\nexample :\r\n  reverse_core xs ys = (inversa xs) ++ ys :=\r\nbegin\r\n  induction xs with a as HI generalizing ys,\r\n  { calc reverse_core [] ys\r\n         = ys                        : by rw reverse_core_nil\r\n     ... = [] ++ ys                  : by rw nil_append\r\n     ... = inversa [] ++ ys          : by rw inversa_nil },\r\n  { calc reverse_core (a :: as) ys\r\n         = reverse_core as (a :: ys) : by rw reverse_core_cons\r\n     ... = inversa as ++ (a :: ys)   : by rw (HI (a :: ys))\r\n     ... = inversa as ++ ([a] ++ ys) : by rw singleton_append\r\n     ... = (inversa as ++ [a]) ++ ys : by rw append_assoc\r\n     ... = inversa (a :: as) ++ ys   : by rw inversa_cons },\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n del lema auxiliar\r\nexample :\r\n  reverse_core xs ys = (inversa xs) ++ ys :=\r\nbegin\r\n  induction xs with a as HI generalizing ys,\r\n  { calc reverse_core [] ys\r\n         = ys                        : rfl\r\n     ... = [] ++ ys                  : rfl\r\n     ... = inversa [] ++ ys          : rfl },\r\n  { calc reverse_core (a :: as) ys\r\n         = reverse_core as (a :: ys) : rfl\r\n     ... = inversa as ++ (a :: ys)   : (HI (a :: ys))\r\n     ... = inversa as ++ ([a] ++ ys) : rfl\r\n     ... = (inversa as ++ [a]) ++ ys : by rw append_assoc\r\n     ... = inversa (a :: as) ++ ys   : rfl },\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n del lema auxiliar\r\nexample :\r\n  reverse_core xs ys = (inversa xs) ++ ys :=\r\nbegin\r\n  induction xs with a as HI generalizing ys,\r\n  { calc reverse_core [] ys\r\n         = ys                        : by simp\r\n     ... = [] ++ ys                  : by simp\r\n     ... = inversa [] ++ ys          : by simp },\r\n  { calc reverse_core (a :: as) ys\r\n         = reverse_core as (a :: ys) : by simp\r\n     ... = inversa as ++ (a :: ys)   : (HI (a :: ys))\r\n     ... = inversa as ++ ([a] ++ ys) : by simp\r\n     ... = (inversa as ++ [a]) ++ ys : by simp\r\n     ... = inversa (a :: as) ++ ys   : by simp },\r\nend\r\n\r\n-- 4\u00aa demostraci\u00f3n del lema auxiliar\r\nexample :\r\n  reverse_core xs ys = (inversa xs) ++ ys :=\r\nbegin\r\n  induction xs with a as HI generalizing ys,\r\n  { by simp, },\r\n  { calc reverse_core (a :: as) ys\r\n         = reverse_core as (a :: ys) : by simp\r\n     ... = inversa as ++ (a :: ys)   : (HI (a :: ys))\r\n     ... = inversa (a :: as) ++ ys   : by simp },\r\nend\r\n\r\n-- 5\u00aa demostraci\u00f3n del lema auxiliar\r\nexample :\r\n  reverse_core xs ys = (inversa xs) ++ ys :=\r\nbegin\r\n  induction xs with a as HI generalizing ys,\r\n  { simp, },\r\n  { simp [HI (a :: ys)], },\r\nend\r\n\r\n-- 6\u00aa demostraci\u00f3n del lema auxiliar\r\nexample :\r\n  reverse_core xs ys = (inversa xs) ++ ys :=\r\nby induction xs generalizing ys ; simp [*]\r\n\r\n-- 7\u00aa demostraci\u00f3n del lema auxiliar\r\nexample :\r\n  reverse_core xs ys = (inversa xs) ++ ys :=\r\nbegin\r\n  induction xs with a as HI generalizing ys,\r\n  { rw reverse_core_nil,\r\n    rw inversa_nil,\r\n    rw nil_append, },\r\n  { rw reverse_core_cons,\r\n    rw (HI (a :: ys)),\r\n    rw inversa_cons,\r\n    rw append_assoc,\r\n    rw singleton_append, },\r\nend\r\n\r\n-- 8\u00aa demostraci\u00f3n  del lema auxiliar\r\n@[simp]\r\nlemma inversa_equiv :\r\n  \u2200 xs : list \u03b1, \u2200 ys, reverse_core xs ys = (inversa xs) ++ ys\r\n| []         := by simp\r\n| (a :: as)  := by simp [inversa_equiv as]\r\n\r\n-- Demostraciones del lema principal\r\n-- =================================\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample : reverse xs = inversa xs :=\r\ncalc reverse xs\r\n     = reverse_core xs [] : rfl\r\n ... = inversa xs ++ []   : by rw inversa_equiv\r\n ... = inversa xs         : by rw append_nil\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample : reverse xs = inversa xs :=\r\nby simp [inversa_equiv, reverse]\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample : reverse xs = inversa xs :=\r\nby simp [reverse]\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 Pruebas_de_equivalencia_de_definiciones_de_inversa\r\nimports Main\r\nbegin\r\n\r\n(* Definici\u00f3n alternativa *)\r\n(* ====================== *)\r\n\r\nfun inversa_aux :: \"'a list \u21d2 'a list \u21d2 'a list\" where\r\n  \"inversa_aux [] ys     = ys\"\r\n| \"inversa_aux (x#xs) ys = inversa_aux xs (x#ys)\"\r\n\r\nfun inversa :: \"'a list \u21d2 'a list\" where\r\n  \"inversa xs = inversa_aux xs []\"\r\n\r\n(* Lema auxiliar: inversa_aux xs ys = (rev xs) @ ys *)\r\n(* ================================================ *)\r\n\r\n(* 1\u00aa demostraci\u00f3n del lema auxiliar *)\r\nlemma\r\n  \"inversa_aux xs ys = (rev xs) @ ys\"\r\nproof (induct xs arbitrary: ys)\r\n  fix ys :: \"'a list\"\r\n  have \"inversa_aux [] ys = ys\"\r\n    by (simp only: inversa_aux.simps(1))\r\n  also have \"\u2026 = [] @ ys\"\r\n    by (simp only: append.simps(1))\r\n  also have \"\u2026 = rev [] @ ys\"\r\n    by (simp only: rev.simps(1))\r\n  finally show \"inversa_aux [] ys = rev [] @ ys\"\r\n    by this\r\nnext\r\n  fix a ::'a and xs :: \"'a list\"\r\n  assume HI: \"\u22c0ys. inversa_aux xs ys = rev xs@ys\"\r\n  show \"\u22c0ys. inversa_aux (a#xs) ys = rev (a#xs)@ys\"\r\n  proof -\r\n    fix ys\r\n    have \"inversa_aux (a#xs) ys = inversa_aux xs (a#ys)\"\r\n      by (simp only: inversa_aux.simps(2))\r\n    also have \"\u2026 = rev xs@(a#ys)\"\r\n      by (simp only: HI)\r\n    also have \"\u2026 = rev xs @ ([a] @ ys)\"\r\n      by (simp only: append.simps)\r\n    also have \"\u2026 = (rev xs @ [a]) @ ys\"\r\n      by (simp only: append_assoc)\r\n    also have \"\u2026 = rev (a # xs) @ ys\"\r\n      by (simp only: rev.simps(2))\r\n    finally show \"inversa_aux (a#xs) ys = rev (a#xs)@ys\"\r\n      by this\r\n  qed\r\nqed\r\n\r\n(* 2\u00aa demostraci\u00f3n del lema auxiliar *)\r\nlemma\r\n  \"inversa_aux xs ys = (rev xs) @ ys\"\r\nproof (induct xs arbitrary: ys)\r\n  fix ys :: \"'a list\"\r\n  have \"inversa_aux [] ys = ys\" by simp\r\n  also have \"\u2026 = [] @ ys\" by simp\r\n  also have \"\u2026 = rev [] @ ys\" by simp\r\n  finally show \"inversa_aux [] ys = rev [] @ ys\" .\r\nnext\r\n  fix a ::'a and xs :: \"'a list\"\r\n  assume HI: \"\u22c0ys. inversa_aux xs ys = rev xs@ys\"\r\n  show \"\u22c0ys. inversa_aux (a#xs) ys = rev (a#xs)@ys\"\r\n  proof -\r\n    fix ys\r\n    have \"inversa_aux (a#xs) ys = inversa_aux xs (a#ys)\" by simp\r\n    also have \"\u2026 = rev xs@(a#ys)\" using HI by simp\r\n    also have \"\u2026 = rev xs @ ([a] @ ys)\" by simp\r\n    also have \"\u2026 = (rev xs @ [a]) @ ys\" by simp\r\n    also have \"\u2026 = rev (a # xs) @ ys\" by simp\r\n    finally show \"inversa_aux (a#xs) ys = rev (a#xs)@ys\" .\r\n  qed\r\nqed\r\n\r\n(* 3\u00aa demostraci\u00f3n del lema auxiliar *)\r\nlemma\r\n  \"inversa_aux xs ys = (rev xs) @ ys\"\r\nproof (induct xs arbitrary: ys)\r\n  fix ys :: \"'a list\"\r\n  show \"inversa_aux [] ys = rev [] @ ys\" by simp\r\nnext\r\n  fix a ::'a and xs :: \"'a list\"\r\n  assume HI: \"\u22c0ys. inversa_aux xs ys = rev xs@ys\"\r\n  show \"\u22c0ys. inversa_aux (a#xs) ys = rev (a#xs)@ys\"\r\n  proof -\r\n    fix ys\r\n    have \"inversa_aux (a#xs) ys = rev xs@(a#ys)\" using HI by simp\r\n    also have \"\u2026 = rev (a # xs) @ ys\" by simp\r\n    finally show \"inversa_aux (a#xs) ys = rev (a#xs)@ys\" .\r\n  qed\r\nqed\r\n\r\n(* 4\u00aa demostraci\u00f3n del lema auxiliar *)\r\nlemma\r\n  \"inversa_aux xs ys = (rev xs) @ ys\"\r\nproof (induct xs arbitrary: ys)\r\n  show \"\u22c0ys. inversa_aux [] ys = rev [] @ ys\" by simp\r\nnext\r\n  fix a ::'a and xs :: \"'a list\"\r\n  assume \"\u22c0ys. inversa_aux xs ys = rev xs@ys\"\r\n  then show \"\u22c0ys. inversa_aux (a#xs) ys = rev (a#xs)@ys\" by simp\r\nqed\r\n\r\n(* 5\u00aa demostraci\u00f3n del lema auxiliar *)\r\nlemma\r\n  \"inversa_aux xs ys = (rev xs) @ ys\"\r\nproof (induct xs arbitrary: ys)\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(* 6\u00aa demostraci\u00f3n del lema auxiliar *)\r\nlemma inversa_equiv:\r\n  \"inversa_aux xs ys = (rev xs) @ ys\"\r\nby (induct xs arbitrary: ys) simp_all\r\n\r\n(* Demostraciones del lema principal *)\r\n(* ================================= *)\r\n\r\n(* 1\u00aa demostraci\u00f3n *)\r\nlemma \"inversa xs = rev xs\"\r\nproof -\r\n  have \"inversa xs = inversa_aux xs []\"\r\n    by (rule inversa.simps)\r\n  also have \"\u2026 = (rev xs) @ []\"\r\n    by (rule inversa_equiv)\r\n  also have \"\u2026 = rev xs\"\r\n    by (rule append.right_neutral)\r\n  finally show \"inversa xs = rev xs\"\r\n    by this\r\nqed\r\n\r\n(* 2\u00aa demostraci\u00f3n *)\r\nlemma \"inversa xs = rev xs\"\r\nproof -\r\n  have \"inversa xs = inversa_aux xs []\"  by simp\r\n  also have \"\u2026 = (rev xs) @ []\" by (rule inversa_equiv)\r\n  also have \"\u2026 = rev xs\" by simp\r\n  finally show \"inversa xs = rev xs\" .\r\nqed\r\n\r\n(* 3\u00aa demostraci\u00f3n *)\r\nlemma \"inversa xs = rev xs\"\r\nby (simp add: inversa_equiv)\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, est\u00e1 definida la funci\u00f3n reverse : list \u03b1 \u2192 list \u03b1 tal que (reverse xs) es la lista obtenida invirtiendo el orden de los elementos de xs. Por ejemplo, reverse [3,2,5,1] = [1,5,2,3] Su definici\u00f3n es def reverse_core : list \u03b1 \u2192 list \u03b1 \u2192 list \u03b1 | [] r := r | (a::l) r := reverse_core l (a::r) def reverse : list \u03b1 \u2192 list \u03b1 := \u03bb l, reverse_core l [] Una definici\u00f3n alternativa es def inversa : list \u03b1 \u2192 list \u03b1 | [] := [] | (x :: xs) := inversa xs ++ [x] Demostrar que las dos definiciones son equivalentes; es decir, reverse xs = inversa xs Para ello, completar la siguiente teor\u00eda de Lean: import data.list.basic open…<\/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,271,264,177,269,100,254,242,267,198,84,169,236,268,265,147,99,266,72],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/752"}],"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=752"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/752\/revisions"}],"predecessor-version":[{"id":753,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/752\/revisions\/753"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=752"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=752"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=752"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}