{"id":7159,"date":"2020-04-23T14:14:56","date_gmt":"2020-04-23T12:14:56","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7159"},"modified":"2020-04-29T14:17:37","modified_gmt":"2020-04-29T12:17:37","slug":"lmf2019-razonamiento-sobre-programas-con-isabelle-hol-2o-parte","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2019-razonamiento-sobre-programas-con-isabelle-hol-2o-parte\/","title":{"rendered":"LMF2019: Razonamiento sobre programas con Isabelle\/HOL (2\u00ba parte)"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"https:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-19\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se ha concluido el estudio, iniciado en la clase anterior, de c\u00f3mo se pueden demostrar manualmente propiedades de programas Haskell y c\u00f3mo traducir dichas demostraciones a Isabelle\/HOL.<\/p>\n<p>Para ello, se han usado las <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-19\/temas\/tema-8.pdf\">transparencias del tema 8<\/a> del curso de <a href=\"https:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-19\/\">Inform\u00e1tica<\/a> (de 1\u00ba del Grado en Matem\u00e1tica). Como lectura complementaria se recomienda el cap\u00edtulo 13 del libro de G. Hutton <a href=\"http:\/\/bit.ly\/1gMqK0X\">Programming in Haskell<\/a>.<\/p>\n<p>De cada propiedad se han presentados distintas demostracciones:<\/p>\n<ul>\n<li>autom\u00e1tica,<\/li>\n<li>aplicativa estructurada (usando <code>simp<\/code>)<\/li>\n<li>aplicativa detallada (usando <code>simp only<\/code>)<\/li>\n<li>declarativa estructurada (usando <code>simp<\/code>)<\/li>\n<li>declarativa detallada (usando <code>simp only<\/code>)<\/li>\n<\/ul>\n<p>La clase se ha dado mediante videoconferencia y los v\u00eddeos correspondientes son:<\/p>\n<ul>\n<li>Primera parte:<\/li>\n<\/ul>\n<p><iframe loading=\"lazy\" width=\"560\" height=\"315\" src=\"https:\/\/www.youtube.com\/embed\/lk-UsIOtClk\" frameborder=\"0\" allow=\"accelerometer; autoplay; encrypted-media; gyroscope; picture-in-picture\" allowfullscreen><\/iframe><\/p>\n<ul>\n<li>Segunda parte:<\/li>\n<\/ul>\n<p><iframe loading=\"lazy\" width=\"560\" height=\"315\" src=\"https:\/\/www.youtube.com\/embed\/R6_MV8r4KFw\" frameborder=\"0\" allow=\"accelerometer; autoplay; encrypted-media; gyroscope; picture-in-picture\" allowfullscreen><\/iframe><\/p>\n<ul>\n<li>Tercera parte:<\/li>\n<\/ul>\n<p><iframe loading=\"lazy\" width=\"560\" height=\"315\" src=\"https:\/\/www.youtube.com\/embed\/Ai8RC6nbCKo\" frameborder=\"0\" allow=\"accelerometer; autoplay; encrypted-media; gyroscope; picture-in-picture\" allowfullscreen><\/iframe><\/p>\n<p>Las transparencia utilizadas son las del tema \n<!-- iframe plugin v.5.0 wordpress.org\/plugins\/iframe\/ -->\n<iframe loading=\"lazy\" src=\"https:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\/temas\/tema-8.pdf\" width=\"100%\" frameborder=\"1\" height=\"500\" scrolling=\"yes\" class=\"iframe-class\"><\/iframe>\n a partir de la p\u00e1gina 29.<\/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\/R10\">relaci\u00f3n 10<\/a> y de la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/LMF2020\/index.php\/R11\">relaci\u00f3n 11<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de L\u00f3gica matem\u00e1tica y fundamentos se ha concluido el estudio, iniciado en la clase anterior, de c\u00f3mo se pueden demostrar manualmente propiedades de programas Haskell y c\u00f3mo traducir dichas demostraciones a Isabelle\/HOL. Para ello, se han usado las transparencias del tema 8 del curso de Inform\u00e1tica (de 1\u00ba&#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\/7159"}],"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=7159"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7159\/revisions"}],"predecessor-version":[{"id":7162,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7159\/revisions\/7162"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7159"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7159"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7159"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}