{"id":7166,"date":"2020-05-07T17:24:03","date_gmt":"2020-05-07T15:24:03","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7166"},"modified":"2020-05-07T17:24:03","modified_gmt":"2020-05-07T15:24:03","slug":"lmf2019-razonamiento-por-casos-y-por-induccion-en-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2019-razonamiento-por-casos-y-por-induccion-en-isabelle-hol\/","title":{"rendered":"LMF2019: Razonamiento por casos y por inducci\u00f3n en Isabelle\/HOL"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-19\">Razonamiento autom\u00e1tico<\/a> hemos profundizado en el estudio de las demostraciones por casos y por inducci\u00f3n. En concreto, se ha estudiado<\/p>\n<ul>\n<li>el razonamiento por casos booleanos,<\/li>\n<li>el razonamiento por casos booleanos sobre una variable,<\/li>\n<li>el razonamiento por casos sobre listas,<\/li>\n<li>el razonamiento por inducci\u00f3n sobre n\u00fameros naturales con patrones,<\/li>\n<li>el razonamiento sobre definiciones con existenciales,<\/li>\n<li>el uso de librer\u00edas auxiliares (como Parity) y<\/li>\n<li>el uso de otros m\u00e9todos de demostraci\u00f3n (como presburg).<\/li>\n<\/ul>\n<p>La clase se ha dado mediante videoconferencia y el v\u00eddeo correspondiente es:<\/p>\n<p><iframe loading=\"lazy\" width=\"560\" height=\"315\" src=\"https:\/\/www.youtube.com\/embed\/si_DTm4ImEM\" frameborder=\"0\" allow=\"accelerometer; autoplay; encrypted-media; gyroscope; picture-in-picture\" allowfullscreen><\/iframe><\/p>\n<p>La teor\u00eda con los ejemplos presentados en la clase es la siguiente:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter \u2039Tema 6: Razonamiento sobre programas\u203a\n\ntheory T6_Razonamiento_sobre_programas\nimports Main \nbegin\nchapter \u2039Tema 6: Razonamiento sobre programas\u203a\n\ntheory T6_Razonamiento_sobre_programas\nimports Main \nbegin\n\ntext \u2039--------------------------------------------------------------- \n  Ejemplo 13. (p. 30) Demostrar que \n     longitud (conc xs ys) = longitud xs + longitud ys\n  ------------------------------------------------------------------- \u203a\n\n(* La demostraci\u00f3n aplicativa es *)\nlemma \"longitud (conc xs ys) = longitud xs + longitud ys\"\n  apply (induct xs) (* 1. longitud (conc [] ys) =\n                          longitud [] + longitud ys\n                       2. \u22c0a xs.\n                             longitud (conc xs ys) =\n                             longitud xs + longitud ys \u27f9\n                             longitud (conc (a # xs) ys) =\n                             longitud (a # xs) + longitud ys *) \n   apply simp_all   (* No subgoals! *)\n  done  \n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"longitud (conc xs ys) = longitud xs + longitud ys\"\n  by (induct xs) simp_all\n\n(* La demostraci\u00f3n declarativa es *)\nlemma \"longitud (conc xs ys) = longitud xs + longitud ys\"\nproof (induct xs)\n  show \"longitud (conc [] ys) = longitud [] + longitud ys\" \n    by simp\nnext\n  fix x xs\n  assume HI: \"longitud (conc xs ys) = longitud xs + longitud ys\"\n  have \"longitud (conc (x # xs) ys) = longitud (x # (conc xs ys))\" \n    by simp\n  also have \"\u2026 = 1 + longitud (conc xs ys)\" \n    by simp\n  also have \"\u2026 = 1 + longitud xs + longitud ys\" \n    using HI by simp\n  also have \"\u2026 = longitud (x # xs) + longitud ys\" \n    by simp\n  finally show \"longitud (conc (x # xs) ys) = \n                longitud (x # xs) + longitud ys\" \n    by simp\nqed\n\n(* La demostraci\u00f3n declarativa detallada es *)\nlemma \"longitud (conc xs ys) = longitud xs + longitud ys\"\nproof (induct xs)\n  show \"longitud (conc [] ys) = longitud [] + longitud ys\" \n    by (simp only: conc.simps(1)\n                   longitud.simps(1))\nnext\n  fix x xs\n  assume HI: \"longitud (conc xs ys) = longitud xs + longitud ys\"\n  have \"longitud (conc (x # xs) ys) = longitud (x # (conc xs ys))\" \n    by (simp only: conc.simps(2))\n  also have \"\u2026 = 1 + longitud (conc xs ys)\" \n    by (simp only: longitud.simps(2))\n  also have \"\u2026 = 1 + longitud xs + longitud ys\" \n    using HI by (simp only:)\n  also have \"\u2026 = longitud (x # xs) + longitud ys\" \n    by (simp only: longitud.simps(2))\n  finally show \"longitud (conc (x # xs) ys) = \n                longitud (x # xs) + longitud ys\" \n    by this\nqed\n\nsection \u2039Inducci\u00f3n correspondiente a la definici\u00f3n recursiva \u203a\n\ntext \u2039--------------------------------------------------------------- \n  Ejemplo 14. Definir la funci\u00f3n\n     coge :: nat \u21d2 'a list \u21d2 'a list\n  tal que (coge n xs) es la lista de los n primeros elementos de xs. Por \n  ejemplo, \n     coge 2 [a,c,d,b,e] = [a,c]\n  ------------------------------------------------------------------ \u203a\n\nfun coge :: \"nat \u21d2 'a list \u21d2 'a list\" where\n  \"coge n []           = []\"\n| \"coge 0 xs           = []\"\n| \"coge (Suc n) (x#xs) = x # (coge n xs)\"\n\nvalue \"coge 2 [a,c,d,b,e] = [a,c]\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejemplo 15. Definir la funci\u00f3n\n     elimina :: nat \u21d2 'a list \u21d2 'a list\n  tal que (elimina n xs) es la lista obtenida eliminando los n primeros\n  elementos de xs. Por ejemplo, \n     elimina 2 [a,c,d,b,e] = [d,b,e]\n  ------------------------------------------------------------------ \u203a\n\nfun elimina :: \"nat \u21d2 'a list \u21d2 'a list\" where\n  \"elimina n []           = []\"\n| \"elimina 0 xs           = xs\"\n| \"elimina (Suc n) (x#xs) = elimina n xs\"\n\nvalue \"elimina 2 [a,c,d,b,e] = [d,b,e]\"\n\ntext \u2039La definici\u00f3n coge genera el esquema de inducci\u00f3n coge.induct:\n     \u27e6\u22c0n. P n []; \n      \u22c0x xs. P 0 (x#xs); \n      \u22c0n x xs. P n xs \u27f9 P (Suc n) (x#xs)\u27e7\n     \u27f9 P n xs\n\n  Puede verse usando \"thm coge.induct\". \u203a\n\nthm elimina.induct\nthm coge.induct\n\ntext \u2039--------------------------------------------------------------- \n  Ejemplo 16. (p. 35) Demostrar que \n     conc (coge n xs) (elimina n xs) = xs\n  ------------------------------------------------------------------- \u203a\n\n(* La demostraci\u00f3n aplicativa es *)\nlemma \"conc (coge n xs) (elimina n xs) = xs\"\n  apply (induct rule: coge.induct) \n      (*  1. \u22c0n. conc (coge n []) (elimina n []) = []\n          2. \u22c0v va. conc (coge 0 (v # va)) (elimina 0 (v # va)) =\n                     v # va\n          3. \u22c0n x xs. conc (coge n xs) (elimina n xs) = xs \u27f9\n                       conc (coge (Suc n) (x # xs)) \n                            (elimina (Suc n) (x # xs)) =\n                       x # xs *)\n    apply simp_all\n      (* No subgoals! *)\n  done\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"conc (coge n xs) (elimina n xs) = xs\"\n  by (induct rule: coge.induct) simp_all\n\n(* La demostraci\u00f3n declarativa es *)\nlemma \"conc (coge n xs) (elimina n xs) = xs\"\nproof (induct rule: coge.induct)\n  fix n\n  show \"conc (coge n []) (elimina n []) = []\" \n    by simp\nnext\n  fix x :: \"'a\" and xs :: \"'a list\"\n  show \"conc (coge 0 (x#xs)) (elimina 0 (x#xs)) = x#xs\" \n    by simp\nnext\n  fix n and x :: \"'a\" and xs :: \"'a list\"\n  assume HI: \"conc (coge n xs) (elimina n xs) = xs\"\n  have \"conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = \n        conc (x#(coge n xs)) (elimina n xs)\" \n    by simp\n  also have \"\u2026 = x#(conc (coge n xs) (elimina n xs))\" \n    by simp\n  also have \"\u2026 = x#xs\" \n    using HI by simp  \n  finally show \"conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = \n                x#xs\"\n    by simp\nqed\n\ntext \u2039Comentario sobre la demostraci\u00f3n anterior:\n  \u00b7 (induct rule: coge.induct) indica que el m\u00e9todo de demostraci\u00f3n es\n    por el esquema de inducci\u00f3n correspondiente a la definici\u00f3n de la\n    funci\u00f3n coge.\n  \u00b7 Se generan 3 subobjetivos:\n    \u00b7 1. \u22c0n. conc (coge n []) (elimina n []) = []\n    \u00b7 2. \u22c0x xs. conc (coge 0 (x#xs)) (elimina 0 (x#xs)) = x#xs\n    \u00b7 3. \u22c0n x xs. \n            conc (coge n xs) (elimina n xs) = xs \u27f9\n            conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = x#xs\n\u203a\n\n(* La demostraci\u00f3n declarativa detallada es *)\nlemma \"conc (coge n xs) (elimina n xs) = xs\"\nproof (induct rule: coge.induct)\n  fix n\n  show \"conc (coge n []) (elimina n []) = []\" \n    by (simp only: coge.simps(1)\n                   elimina.simps(1)\n                   conc.simps(1))\nnext\n  fix x :: \"'a\" and xs :: \"'a list\"\n  show \"conc (coge 0 (x#xs)) (elimina 0 (x#xs)) = x#xs\" \n    by (simp only: coge.simps(2)\n                   elimina.simps(2)\n                   conc.simps(1))\nnext\n  fix n and x :: \"'a\" and xs :: \"'a list\"\n  assume HI: \"conc (coge n xs) (elimina n xs) = xs\"\n  have \"conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = \n        conc (x#(coge n xs)) (elimina n xs)\" \n    by (simp only: coge.simps(3)\n                   elimina.simps(3))\n  also have \"\u2026 = x#(conc (coge n xs) (elimina n xs))\" \n    by (simp only: conc.simps(2))\n  also have \"\u2026 = x#xs\" \n    using HI by (simp only:) \n  finally show \"conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = \n                x#xs\"\n    by this\nqed\n\nsection \u2039Razonamiento por casos \u203a\n\ntext \u2039 --------------------------------------------------------------- \n  Ejemplo 17. Definir la funci\u00f3n\n     esVacia :: 'a list \u21d2 bool\n  tal que (esVacia xs) se verifica si xs es la lista vac\u00eda. Por ejemplo,\n     esVacia []  = True\n     esVacia [1] = False\n  ------------------------------------------------------------------ \u203a\n\nfun esVacia :: \"'a list \u21d2 bool\" where\n  \"esVacia []     = True\"\n| \"esVacia (x#xs) = False\"\n\nvalue \"esVacia []  = True\"\nvalue \"esVacia [a] = False\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejemplo 18 (p. 39) . Demostrar que \n     esVacia xs = esVacia (conc xs xs)\n  ------------------------------------------------------------------- \u203a\n\n(* La demostraci\u00f3n aplicativa es *)\nlemma \"esVacia xs = esVacia (conc xs xs)\"\n  apply (cases xs) \n     (* 1. xs = [] \u27f9 esVacia xs = esVacia (conc xs xs)\n        2. \u22c0a list. xs = a # list \u27f9\n                    esVacia xs = esVacia (conc xs xs) *)\n   apply simp_all\n     (* No subgoals! *)\n  done\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"esVacia xs = esVacia (conc xs xs)\"\n  by (cases xs) simp_all\n\n(* La demostraci\u00f3n declarativa es *)\nlemma \"esVacia xs = esVacia (conc xs xs)\"\nproof (cases xs)\n  assume \"xs = []\"\n  then show \"esVacia xs = esVacia (conc xs xs)\" \n    by simp\nnext\n  fix y ys\n  assume \"xs = y#ys\"\n  then show \"esVacia xs = esVacia (conc xs xs)\" \n    by simp\nqed\n\ntext \u2039Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 \"(cases xs)\" es el m\u00e9todo de demostraci\u00f3n por casos seg\u00fan xs.\n  \u00b7 Se generan dos subobjetivos  correspondientes a los dos\n    constructores de listas:\n    \u00b7 1. xs = [] \u27f9 esVacia xs = esVacia (conc xs xs)\n    \u00b7 2. \u22c0y ys. xs = y#ys \u27f9 esVacia xs = esVacia (conc xs xs)\n  \u00b7 \"then\" indica \"usando la propiedad anterior\"\n\u203a\n\n(* La demostraci\u00f3n declarativa detallada es *)\nlemma \"esVacia xs = esVacia (conc xs xs)\"\nproof (cases xs)\n  assume \"xs = []\"\n  then show \"esVacia xs = esVacia (conc xs xs)\" \n    by (simp only: conc.simps(1))\nnext\n  fix y ys\n  assume \"xs = y#ys\"\n  then show \"esVacia xs = esVacia (conc xs xs)\" \n    by (simp only: esVacia.simps(2)\n                   conc.simps(2))\nqed\n\n(* La demostraci\u00f3n declarativa simplificada es *)\nlemma \"esVacia xs = esVacia (conc xs xs)\"\nproof (cases xs)\n  case Nil\n  then show \"esVacia xs = esVacia (conc xs xs)\" \n    by simp\nnext\n  case Cons\n  then show \"esVacia xs = esVacia (conc xs xs)\" \n    by simp\nqed\n\ntext \u2039Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 \"case Nil\" es una abreviatura de \"assume xs = []\"\n  \u00b7 \"case Cons\" es una abreviatura de \"fix y ys assume xs = y#ys\"\u203a\n\nlemma \"esVacia xs = esVacia (conc xs xs)\"\nproof (cases xs)\n  case Nil\n  then show ?thesis \n    by simp\nnext\n  case (Cons a list)\n  then show ?thesis \n    by simp\nqed\n\n\n(* La demostraci\u00f3n con el patr\u00f3n sugerido es *)\nlemma \"esVacia xs = esVacia (conc xs xs)\"\nproof (cases xs)\n  case Nil\n  then show ?thesis by simp\nnext\n  case (Cons x xs)\n  then show ?thesis by simp\nqed\n\nsection \u2039Heur\u00edstica de generalizaci\u00f3n\u203a\n\ntext \u2039--------------------------------------------------------------- \n  Ejemplo 19. Definir la funci\u00f3n\n     inversaAc :: 'a list \u21d2 'a list\n  tal que (inversaAc xs) es a inversa de xs calculada usando\n  acumuladores. Por ejemplo, \n     inversaAc [a,c,b,e] = [e,b,c,a]\n  ------------------------------------------------------------------ \u203a\n\nfun inversaAcAux :: \"'a list \u21d2 'a list \u21d2 'a list\" where\n  \"inversaAcAux [] ys     = ys\"\n| \"inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)\"\n\ndefinition inversaAc :: \"'a list \u21d2 'a list\" where\n  \"inversaAc xs = inversaAcAux xs []\"\n\nvalue \"inversaAc [a,c,b,e] = [e,b,c,a]\"\n\ntext \u2039Lema. [Ejemplo de equivalencia entre las definiciones]\n  La inversa de [a,b,c] es lo mismo calculada con la primera definici\u00f3n\n  que con la segunda.\u203a\n\nlemma \"inversaAc [a,b,c] = inversa [a,b,c]\"\n  by (simp add: inversaAc_def)\n\ntext \u2039Nota. [Ejemplo fallido de demostraci\u00f3n por inducci\u00f3n]\n  El siguiente intento de demostrar que para cualquier lista xs, se\n  tiene que  \"inversaAc xs = inversa xs\" falla.\u203a\n\nlemma \"inversaAc xs = inversa xs\"\nproof (induct xs)\n  show \"inversaAc [] = inversa []\" \n    by (simp add: inversaAc_def)\nnext\n  fix a :: \"'b\" and xs :: \"'b list\" \n  assume HI: \"inversaAc xs = inversa xs\"\n  have \"inversaAc (a#xs) = inversaAcAux (a#xs) []\" \n    by (simp add: inversaAc_def)\n  also have \"\u2026 = inversaAcAux xs [a]\" \n    by simp\n  also have \"\u2026 = inversa (a#xs)\"\n  (* Problema: la hip\u00f3tesis de inducci\u00f3n no es aplicable. *)\noops\n\ntext \u2039Nota. [Heur\u00edstica de generalizaci\u00f3n]\n  Cuando se use demostraci\u00f3n estructural, cuantificar universalmente las \n  variables libres (o, equivalentemente, considerar las variables libres\n  como variables arbitrarias).\n\n  Lema. [Lema con generalizaci\u00f3n]\n  Para toda lista ys se tiene \n     inversaAcAux xs ys = (inversa xs) @ ys\n\u203a\n\ntext \u2039--------------------------------------------------------------- \n  Ejemplo 20. (p. 44) Demostrar que \n     inversaAcAux xs ys = (inversa xs) @ ys\n  ------------------------------------------------------------------- \u203a\n\n(* La demostraci\u00f3n aplicativa es *)\nlemma \"inversaAcAux xs ys = (inversa xs) @ ys\"\n  apply (induct xs arbitrary: ys) \n     (* 1. \u22c0ys. inversaAcAux [] ys = inversa [] @ ys\n        2. \u22c0a xs ys.\n              (\u22c0ys. inversaAcAux xs ys = inversa xs @ ys) \u27f9\n              inversaAcAux (a # xs) ys = inversa (a # xs) @ ys *)\n   apply simp_all\n     (* No subgoals! *)\n  done\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"inversaAcAux xs ys = (inversa xs) @ ys\"\n  by (induct xs arbitrary: ys) simp_all\n\n(* La demostraci\u00f3n declarativa es *)\nlemma\n  \"inversaAcAux xs ys = (inversa xs) @ ys\"\nproof (induct xs arbitrary: ys)\n  show \"\u22c0ys. inversaAcAux [] ys = (inversa []) @ ys\" \n    by simp\nnext\n  fix a :: \"'b\" and xs :: \"'b list\" \n  assume HI: \"\u22c0ys. inversaAcAux xs ys = inversa xs @ ys\"\n  show \"\u22c0ys. inversaAcAux (a#xs) ys = inversa (a#xs) @ ys\"\n  proof -\n    fix ys\n    have \"inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)\" \n      by simp\n    also have \"\u2026 = inversa xs @ (a#ys)\" \n      using HI by simp\n    also have \"\u2026 = inversa (a#xs) @ ys\" \n      (* using [[simp_trace]] *)\n      by simp \n    finally show \"inversaAcAux (a#xs) ys = inversa (a#xs) @ ys\" \n      by simp\n  qed\nqed\n\ntext \u2039Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 \"(induct xs arbitrary: ys)\" es el m\u00e9todo de demostraci\u00f3n por\n    inducci\u00f3n sobre xs usando ys como variable arbitraria.\n  \u00b7 Se generan dos subobjetivos:\n    \u00b7 1. \u22c0ys. inversaAcAux [] ys = inversa [] @ ys\n    \u00b7 2. \u22c0a xs ys. (\u22c0ys. inversaAcAux xs ys = inversa xs @ ys) \u27f9\n                    inversaAcAux (a # xs) ys = inversa (a # xs) @ ys\n  \u00b7 Dentro de una demostraci\u00f3n se pueden incluir otras demostraciones.\n  \u00b7 Para demostrar la propiedad universal \"\u22c0ys. P(ys)\" se elige una\n    lista arbitraria (con \"fix ys\") y se demuestra \"P(ys)\". \u203a\n\ntext \u2039Nota. En el paso \"inversa xs@(a#ys) = inversa (a#xs)@ys\" se usan\n  lemas de la teor\u00eda List. Se puede observar, insertano \n     using [[simp_trace]]\n  entre la igualdad y by simp, que los lemas usados son \n  \u00b7 append_simps_1: []@ys = ys\n  \u00b7 append_simps_2: (x#xs)@ys = x#(xs@ys)\n  \u00b7 append_assoc:   (xs @ ys) @ zs = xs @ (ys @ zs)\n  Las dos primeras son las ecuaciones de la definici\u00f3n de append.\n\n  En la siguiente demostraci\u00f3n se detallan los lemas utilizados.\u203a\n\n\u2015 \u2039Demostraci\u00f3n aplicativa detallada\u203a\nlemma \"(inversa xs) @ (a#ys) = (inversa (a#xs)) @ ys\"\n  apply (simp only: inversa.simps(2))\n    (* inversa xs @ (a # ys) = (inversa xs @ [a]) @ ys*)\n  apply (simp only: append_assoc)\n    (* inversa xs @ (a # ys) = inversa xs @ ([a] @ ys) *)\n  apply (simp only: append.simps(2))\n    (* inversa xs @ (a # ys) = inversa xs @ (a # ([] @ ys)) *)\n  apply (simp only: append.simps(1))\n    (* *)\n  done\n\n\u2015 \u2039Demostraci\u00f3n declarativa detallada del lema auxiliar\u203a\nlemma auxiliar: \"(inversa xs) @ (a#ys) = (inversa (a#xs)) @ ys\"\nproof -\n  have \"(inversa xs) @ (a#ys) = (inversa xs) @ (a # ([] @ ys))\" \n    by (simp only: append.simps(1))\n  also have \"\u2026 = (inversa xs) @ ([a] @ ys)\" \n    by (simp only: append.simps(2))\n  also have \"\u2026 = ((inversa xs) @ [a]) @ ys\" \n    by (simp only: append_assoc)\n  also have \"\u2026 = (inversa (a#xs)) @ ys\" \n    by (simp only: inversa.simps(2))\n  finally show ?thesis \n    by this\nqed\n\n(* La demostraci\u00f3n declarativa detallada es *)\nlemma inversaAcAux_es_inversa:\n  \"inversaAcAux xs ys = (inversa xs) @ ys\"\nproof (induct xs arbitrary: ys)\n  fix ys :: \"'b list\"\n  show \"inversaAcAux [] ys = (inversa []) @ ys\" \n    by (simp only: inversaAcAux.simps(1)\n                   inversa.simps(1)\n                   append.simps(1))\nnext\n  fix a :: \"'b\" and xs :: \"'b list\"\n  assume HI: \"\u22c0ys. inversaAcAux xs ys = inversa xs @ ys\"\n  show \"\u22c0ys. inversaAcAux (a#xs) ys = inversa (a#xs) @ ys\"\n  proof -\n    fix ys\n    have \"inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)\" \n      by (simp only: inversaAcAux.simps(2))\n    also have \"\u2026 = inversa xs @ (a#ys)\" \n      using HI by (simp only:)\n    also have \"\u2026 = inversa (a#xs) @ ys\" \n      by (rule auxiliar) \n    finally show \"inversaAcAux (a#xs) ys = inversa (a#xs) @ ys\" \n      by this\n  qed\nqed\n\ntext \u2039--------------------------------------------------------------- \n  Ejemplo 21. (p. 43) Demostrar que \n     inversaAc xs = inversa xs\n  ------------------------------------------------------------------- \u203a\n\n(* La demostraci\u00f3n aplicativa es *)\ncorollary \"inversaAc xs = inversa xs\"\n  apply (simp add: inversaAcAux_es_inversa inversaAc_def)\n  done \n\n(* La demostraci\u00f3n autom\u00e1tica es *)\ncorollary \"inversaAc xs = inversa xs\"\n  by (simp add: inversaAcAux_es_inversa inversaAc_def)\n\ntext \u2039Comentario de la demostraci\u00f3n anterior:\n  \u00b7 \"(simp add: inversaAcAux_es_inversa inversaAc_def)\" es el m\u00e9todo de \n    demostraci\u00f3n por simplificaci\u00f3n usando como regla de simplificaci\u00f3n \n    las propiedades inversaAcAux_es_inversa e inversaAc_def. \u203a\n \nsection \u2039Demostraci\u00f3n por inducci\u00f3n para funciones de orden superior \u203a\n\ntext \u2039 --------------------------------------------------------------- \n  Ejemplo 22. Definir la funci\u00f3n\n     sum :: nat list \u21d2 nat\n  tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,\n     sum [3,2,5] = 10\n  ------------------------------------------------------------------ \u203a\n\nfun sum :: \"nat list \u21d2 nat\" where\n  \"sum []     = 0\"\n| \"sum (x#xs) = x + sum xs\"\n\nvalue \"sum [3,2,5] = 10\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejemplo 23. Definir la funci\u00f3n\n     map :: ('a \u21d2 'b) \u21d2 'a list \u21d2 'b list\n  tal que (map f xs) es la lista obtenida aplicando la funci\u00f3n f a los\n  elementos de xs. Por ejemplo,\n     map (\u03bbx. 2*x) [3::nat,2,5] = [6,4,10]\n     map ((*) 2)   [3::nat,2,5] = [6,4,10]\n     map ((+) 2)   [3::nat,2,5] = [5,4,7]\n  ------------------------------------------------------------------ \u203a\n\nfun map :: \"('a \u21d2 'b) \u21d2 'a list \u21d2 'b list\" where\n  \"map f []     = []\"\n| \"map f (x#xs) = (f x) # map f xs\"\n\nvalue \"map (\u03bbx. 2*x) [3::nat,2,5] = [6,4,10]\"\nvalue \"map ((*) 2)   [3::nat,2,5] = [6,4,10]\"\nvalue \"map ((+) 2)   [3::nat,2,5] = [5,4,7]\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejemplo 24. (p. 45) Demostrar que \n     sum (map ((*) 2) xs) = 2 * (sum xs)\n  ------------------------------------------------------------------- \u203a\n\ndeclare [[names_short]]\n\n(* La demostraci\u00f3n aplicativa es *)\nlemma \"sum (map ((*) 2) xs) = 2 * (sum xs)\"\n  apply (induct xs) \n     (* 1. sum (map (( * ) 2) []) = 2 * sum []\n        2. \u22c0a xs. sum (map (( * ) 2) xs) = 2 * sum xs \u27f9\n                  sum (map (( * ) 2) (a # xs)) = 2 * sum (a # xs) *)\n   apply simp_all\n     (* No subgoals! *)\n  done\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"sum (map ((*) 2) xs) = 2 * (sum xs)\"\n  by (induct xs) simp_all\n\n(* La demostraci\u00f3n declarativa es *)\nlemma \"sum (map ((*) 2) xs) = 2 * (sum xs)\"\nproof (induct xs)\n  show \"sum (map ((*) 2) []) = 2 * (sum [])\" by simp\nnext\n  fix a xs\n  assume HI: \"sum (map ((*) 2) xs) = 2 * (sum xs)\"\n  have \"sum (map ((*) 2) (a#xs)) = sum ((2*a) # (map ((*) 2) xs))\" \n    by simp\n  also have \"\u2026 = 2*a + sum (map ((*) 2) xs)\" \n    by simp\n  also have \"\u2026 = 2*a + 2*(sum xs)\" \n    using HI by simp\n  also have \"\u2026 = 2*(a + sum xs)\" \n    by simp\n  also have \"\u2026 = 2*(sum (a#xs))\" \n    by simp\n  finally show \"sum (map ((*) 2) (a#xs)) = 2*(sum (a#xs))\" \n    by simp\nqed\n\n(* La demostraci\u00f3n declarativa detallada es *)\nlemma \"sum (map ((*) 2) xs) = 2 * (sum xs)\"\nproof (induct xs)\n  show \"sum (map ((*) 2) []) = 2 * (sum [])\" \n    by (simp only: map.simps(1)\n                   sum.simps(1))\nnext\n  fix a xs\n  assume HI: \"sum (map ((*) 2) xs) = 2 * (sum xs)\"\n  have \"sum (map ((*) 2) (a#xs)) = sum ((2*a)#(map ((*) 2) xs))\" \n    by (simp only: map.simps(2))\n  also have \"\u2026 = 2*a + sum (map ((*) 2) xs)\" \n    by (simp only: sum.simps(2))\n  also have \"\u2026 = 2*a + 2*(sum xs)\" \n    using HI by (simp only:)\n  also have \"\u2026 = 2*(a + sum xs)\" \n    (* find_theorems \"_ * (_ + _)\" *)\n    by (simp only: add_mult_distrib2)\n  also have \"\u2026 = 2*(sum (a#xs))\" \n    by (simp only: sum.simps(2))\n  finally show \"sum (map ((*) 2) (a#xs)) = 2*(sum (a#xs))\" \n    by this\nqed\n\ntext \u2039 --------------------------------------------------------------- \n  Ejemplo 25. (p. 48) Demostrar que \n     longitud (map f xs) = longitud xs\n  ------------------------------------------------------------------- \u203a\n\n(* La demostraci\u00f3n aplicativa es *)\nlemma \"longitud (map f xs) = longitud xs\"\n  apply (induct xs) \n     (* 1. longitud (map f []) = longitud []\n        2. \u22c0a xs. longitud (map f xs) = longitud xs \u27f9\n                   longitud (map f (a # xs)) = longitud (a # xs) *)\n   apply simp_all\n     (* No subgoals! *)\n  done\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"longitud (map f xs) = longitud xs\"\n  by (induct xs) simp_all\n\n(* La demostraci\u00f3n declarativa es *)\nlemma \"longitud (map f xs) = longitud xs\"\nproof (induct xs)\n  show \"longitud (map f []) = longitud []\" \n    by simp\nnext\n  fix a xs\n  assume HI: \"longitud (map f xs) = longitud xs\"\n  have \"longitud (map f (a#xs)) = longitud (f a # (map f xs))\" \n    by simp\n  also have \"\u2026 = 1 + longitud (map f xs)\" \n    by simp\n  also have \"\u2026 = 1 + longitud xs\" \n    using HI by simp\n  also have \"\u2026 = longitud (a#xs)\" \n    by simp\n  finally show \"longitud (map f (a#xs)) = longitud (a#xs)\" \n    by simp\nqed\n\n(* La demostraci\u00f3n declarativa detallada es *)\nlemma \"longitud (map f xs) = longitud xs\"\nproof (induct xs)\n  show \"longitud (map f []) = longitud []\" \n    by (simp only: map.simps(1)\n                   longitud.simps(1))\nnext\n  fix a xs\n  assume HI: \"longitud (map f xs) = longitud xs\"\n  have \"longitud (map f (a#xs)) = longitud (f a # (map f xs))\" \n    by (simp only: map.simps(2))\n  also have \"\u2026 = 1 + longitud (map f xs)\" \n    by (simp only: longitud.simps(2))\n  also have \"\u2026 = 1 + longitud xs\" \n    using HI by (simp only:)\n  also have \"\u2026 = longitud (a#xs)\" \n    by (simp only: longitud.simps(2))\n  finally show \"longitud (map f (a#xs)) = longitud (a#xs)\" \n    by this\nqed\n\nsection \u2039Referencias\u203a\n\ntext \u2039\n  \u00b7 J.A. Alonso. \"Razonamiento sobre programas\" http:\/\/goo.gl\/R06O3\n  \u00b7 G. Hutton. \"Programming in Haskell\". Cap. 13 \"Reasoning about\n    programms\". \n  \u00b7 S. Thompson. \"Haskell: the Craft of Functional Programming, 3rd\n    Edition. Cap. 8 \"Reasoning about programms\". \n  \u00b7 L. Paulson. \"ML for the Working Programmer, 2nd Edition\". Cap. 6. \n    \"Reasoning about functional programs\". \n\u203a\n\nend \n<\/pre>\n<p>Como tarea se ha propuesto la resoluci\u00f3n de los ejercicios de la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/LMF2020\/index.php\/R12\">relaci\u00f3n 12<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de Razonamiento autom\u00e1tico hemos profundizado en el estudio de las demostraciones por casos y por inducci\u00f3n. En concreto, se ha estudiado el razonamiento por casos booleanos, el razonamiento por casos booleanos sobre una variable, el razonamiento por casos sobre listas, el razonamiento por inducci\u00f3n sobre n\u00fameros naturales con&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","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,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[334],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7166"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=7166"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7166\/revisions"}],"predecessor-version":[{"id":7167,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7166\/revisions\/7167"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7166"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7166"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7166"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}