{"id":4317,"date":"2014-05-14T18:47:02","date_gmt":"2014-05-14T16:47:02","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4317"},"modified":"2014-05-16T08:52:38","modified_gmt":"2014-05-16T06:52:38","slug":"lmf2014-razonamiento-sobre-programas-con-isabellhol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2014-razonamiento-sobre-programas-con-isabellhol\/","title":{"rendered":"LMF2014: Razonamiento sobre programas con Isabelle\/HOL"},"content":{"rendered":"<p>En la  clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-13\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se ha estudiado c\u00f3m escribir programas funcionales y c\u00f3mo demostrar sus propiedades con Isabelle\/HOL.<\/p>\n<p>En la presentaci\u00f3n se han usado los ejemplos del <a href=\"http:\/\/goo.gl\/Imvyt\">tema 8<\/a> del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\">Inform\u00e1tica<\/a> (de 1\u00ba del Grado en Matem\u00e1ticas).<\/p>\n<p>La teor\u00eda correspondiente es<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nheader {* Tema 13: Razonamiento sobre programas en Isabelle *}\n\ntheory T13\nimports Main\nbegin\n\ntext {* \n  En este tema se demuestra con Isabelle las propiedades de los\n  programas funcionales como se expone en el tema 8 del curso\n  \"Inform\u00e1tica\" que puede leerse en\n  <p><a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\/temas\/tema-8t.pdf\" target=\"_blank\" rel=\"noopener noreferrer nofollow\">Click to access tema-8t.pdf<\/a><\/p>\n*}\n\nsection {* Razonamiento ecuacional *}\n\ntext {* ----------------------------------------------------------------\n  Ejercicio 1. Definir, por recursi\u00f3n, la funci\u00f3n\n     longitud :: \"'a list \u21d2 nat\" where\n  tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,\n     longitud [4,2,5] = 3\n  ------------------------------------------------------------------- *}\n\nfun longitud :: \"'a list \u21d2 nat\" where\n  \"longitud []     = 0\"\n| \"longitud (x#xs) = 1 + longitud xs\"\n   \nvalue \"longitud [4,2,5]\" -- \"= 3\"\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 2. Demostrar que \n     longitud [4,2,5] = 3\n  ------------------------------------------------------------------- *}\n\nlemma \"longitud [4,2,5] = 3\"\nby simp\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 3. Definir la funci\u00f3n\n     fun intercambia :: \"'a \u00d7 'b \u21d2 'b \u00d7 'a\"\n  tal que (intercambia p) es el par obtenido intercambiando las\n  componentes del par p. Por ejemplo,\n     \"intercambia (2,3) = (3,2)\n  ------------------------------------------------------------------ *}\n\nfun intercambia :: \"'a \u00d7 'b \u21d2 'b \u00d7 'a\" where\n  \"intercambia (x,y) = (y,x)\"\n\nvalue \"intercambia (2,3)\" -- \"= (3,2)\"\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 4. Demostrar que \n     intercambia (intercambia (x,y)) = (x,y)\n  ------------------------------------------------------------------- *}\n\nlemma \"intercambia (intercambia (x,y)) = (x,y)\"\nby simp\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 5. Definir, por recursi\u00f3n, la funci\u00f3n\n     inversa :: \"'a list \u21d2 'a list\"\n  tal que (inversa xs) es la lista obtenida invirtiendo el orden de los\n  elementos de xs. Por ejemplo,\n     inversa [3,2,5] = [5,2,3]\n  ------------------------------------------------------------------ *}\n\nfun inversa :: \"'a list \u21d2 'a list\" where\n  \"inversa []     = []\"\n| \"inversa (x#xs) = inversa xs @ [x]\"\n\nvalue \"inversa [3,2,5]\" -- \"= [5,2,3]\"\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 6. Demostrar que \n     inversa [x] = [x]\n  ------------------------------------------------------------------- *}\n\nlemma \"inversa [x] = [x]\"\nby simp\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 7. Definir la funci\u00f3n\n     repite :: \"nat \u21d2 'a \u21d2 'a list\" where\n  tal que (repite n x) es la lista obtenida repitiendo n veces el \n  elemento x. Por ejemplo,\n     repite 3 5 = [5,5,5]\n  ------------------------------------------------------------------ *}\n\nfun repite :: \"nat \u21d2 'a \u21d2 'a list\" where\n  \"repite 0 x       = []\"\n| \"repite (Suc n) x = x # (repite n x)\"\n\nvalue \"repite 3 5\" -- \"= [5,5,5]\"\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 8. Demostrar que \n     longitud (repite n x) = n\n  ------------------------------------------------------------------- *}\n\nlemma \"longitud (repite n x) = n\"\nby (induct n) auto\n\nlemma longitud_repite:\n  \"longitud (repite n x) = n\"\nproof (induct n)\n  show \"longitud (repite 0 x) = 0\" by simp\nnext\n  fix n\n  assume hi: \"longitud (repite n x) = n\"\n  show \"longitud (repite (Suc n) x) = Suc n\"\n  proof -\n    have \"longitud (repite (Suc n) x) = longitud (x # (repite n x))\" by simp\n    also have \"... = 1 +  longitud (repite n x)\" by simp\n    also have \"... = 1 + n\" using hi by simp\n    also have \"... = Suc n\" by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 9. Definir la funci\u00f3n\n     fun conc :: \"'a list \u21d2 'a list \u21d2 'a list\"\n  tal que (conc xs ys) es la concatenaci\u00f3n de las listas xs e ys. Por \n  ejemplo,\n     conc [2,3] [4,3,5] = [2,3,4,3,5]\n  ------------------------------------------------------------------ *}\n\nfun conc :: \"'a list \u21d2 'a list \u21d2 'a list\" where\n  \"conc []     ys = ys\"\n| \"conc (x#xs) ys = x # (conc xs ys)\"\n\nvalue \"conc [2,3] [4,3,5]\" -- \"= [2,3,4,3,5]\"\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 10. Demostrar que \n     conc xs (conc ys zs) = (conc xs ys) zs\n  ------------------------------------------------------------------- *}\n\nlemma \"conc xs (conc ys zs) = conc (conc xs ys) zs\"\nby (induct xs) auto\n\nlemma conc_asociativa:\n  \"conc xs (conc ys zs) = conc (conc xs ys) zs\"\nproof (induct xs)\n  show \"conc [] (conc ys zs) = conc (conc [] ys) zs\" by simp\nnext\n  fix x xs\n  assume hi: \"conc xs (conc ys zs) = conc (conc xs ys) zs\"\n  show \"conc (x # xs) (conc ys zs) = conc (conc (x # xs) ys) zs\"\n  proof -\n    have \"conc (x # xs) (conc ys zs) = x # (conc xs (conc ys zs))\" by simp\n    also have \"... = x # (conc (conc xs ys) zs)\" using hi by simp\n    also have \"... = conc (x#(conc xs ys)) zs\" by simp\n    also have \"... = conc (conc (x # xs) ys) zs\" by simp\n    finally show ?thesis .\n  qed\nqed\n\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 11. Refutar que \n     conc xs ys = conc ys xs\n  ------------------------------------------------------------------- *}\n\nlemma \"conc xs ys = conc ys xs\"\nquickcheck\noops\n\ntext {* Encuentra el contraejemplo, \n  xs = [a2]\n  ys = [a1] *}\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 12. Demostrar que \n     conc xs [] = xs\n  ------------------------------------------------------------------- *}\n\nlemma \"conc xs [] = xs\"\nby (induct xs) auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 13. Demostrar que \n     longitud (conc xs ys) = longitud xs + longitud ys\n  ------------------------------------------------------------------- *}\n\nlemma \"longitud (conc xs ys) = longitud xs + longitud ys\"\nby (induct xs) auto\n\nlemma long_conc:\n  \"longitud (conc xs ys) = longitud xs + longitud ys\"\nproof (induct xs)\n  show \"longitud (conc [] ys) = longitud [] + longitud ys\" by simp\nnext\n  fix x xs\n  assume hi: \"longitud (conc xs ys) = longitud xs + longitud ys\"\n  show \"longitud (conc (x # xs) ys) = longitud (x # xs) + longitud ys\"\n  proof -\n    have \"longitud (conc (x # xs) ys) = longitud (x # (conc xs ys))\" by simp\n    also have \"... = 1 + longitud (conc xs ys)\" by simp\n    also have \"... = 1 + (longitud xs + longitud ys)\" using hi by simp\n    also have \"... = (1+ longitud xs) + longitud ys\" by simp\n    also have \"... = longitud (x # xs) + longitud ys\" by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 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 [3,7,5,4] = [3,7]\n  ------------------------------------------------------------------ *}\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 [3,7,5,4]\" -- \"= [3,7]\"\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 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 [3,7,5,4] = [5,4]\n  ------------------------------------------------------------------ *}\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 [3,7,5,4]\" -- \"= [5,4]\"\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 16. Demostrar que \n     conc (coge n xs) (elimina n xs) = xs\n  ------------------------------------------------------------------- *}\n\nlemma \"conc (coge n xs) (elimina n xs) = xs\"\nby (induct rule: coge.induct) auto\n\ntext {* coge.induct es el esquema de inducci\u00f3n asociado a la definici\u00f3n\n  de la funci\u00f3n coge. Puede verse como sigue: *}\n\nthm coge.induct\n\nlemma \"conc (coge n xs) (elimina n xs) = xs\"\nby (induct rule: elimina.induct) auto\n\nlemma conc_coge_elimina:\n  \"conc (coge n xs) (elimina n xs) = xs\"\nproof (induct rule: coge.induct) \n  show \"\u22c0n. conc (coge n []) (elimina n []) = []\" by simp\nnext\n  show \"\u22c0v va. conc (coge 0 (v # va)) (elimina 0 (v # va)) = v # va\" by simp\nnext\n  fix x xs n \n  assume hi: \"conc (coge n xs) (elimina n xs) = xs\"\n  show \"conc (coge (Suc n) (x # xs)) (elimina (Suc n) (x # xs)) = x # xs\"\n  proof -\n    have \"conc (coge (Suc n) (x # xs)) (elimina (Suc n) (x # xs)) = conc (coge (Suc n) (x # xs)) (elimina n xs)\" by simp\n    also have \"... = conc (x# (coge n xs)) (elimina n xs)\" by simp\n    also have \"... = x#(conc (coge n xs) (elimina n xs))\" by simp\n    also have \"... = (x#xs)\" using hi by simp\n    finally show ?thesis .\n  qed\nqed\n\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 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  ------------------------------------------------------------------ *}\n\nfun esVacia :: \"'a list \u21d2 bool\" where\n  \"esVacia []     = True\"\n| \"esVacia (x#xs) = False\"\n\nvalue \"esVacia []\"  -- \"= True\"\nvalue \"esVacia [1]\" -- \"= False\"\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 18. Demostrar que \n     esVacia xs = esVacia (conc xs xs)\n  ------------------------------------------------------------------- *}\n\nlemma \"esVacia xs = esVacia (conc xs xs)\"\nby (induct xs) auto\n\nlemma vacia_conc:\n  \"esVacia xs = esVacia (conc xs xs)\"\nproof (induct xs)\n  show \"esVacia [] = esVacia (conc [] [])\" by simp\n  next\n    fix x xs\n    assume hi: \"esVacia xs = esVacia (conc xs xs)\"\n    show \"esVacia (x # xs) = esVacia (conc (x # xs) (x # xs))\"\n    proof -\n      have \"esVacia (conc (x # xs) (x # xs)) = esVacia (x# (conc xs (x#xs)))\" by simp\n      also have \"... = esVacia (x # xs)\" by simp\n      finally show ?thesis by simp\n    qed\nqed\n\nlemma vacia_conc':\n  \"esVacia xs = esVacia (conc xs xs)\"\nproof (cases xs)\n  case Nil thus ?thesis by simp\nnext\n  case Cons thus ?thesis by simp\nqed\n\n\nlemma vacia_conc'':\n  \"esVacia xs = esVacia (conc xs xs)\"\nby (cases xs) simp_all\n\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 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 [3,2,5] = [5,2,3]\n  ------------------------------------------------------------------ *}\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\nfun inversaAc :: \"'a list \u21d2 'a list\" where\n  \"inversaAc xs = inversaAcAux xs []\"\n\nvalue \"inversaAc [3,2,5]\" -- \"= [5,2,3]\"\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 20. Demostrar que \n     inversaAcAux xs ys = (inversa xs)@ys\n  ------------------------------------------------------------------- *}\n\nlemma inversaAcAux_es_inversa:\n  \"inversaAcAux xs ys = (inversa xs)@ys\"\nby (induct xs arbitrary: ys) auto\n\nlemma inversaAcAux_es_inversa_b:\n  \"inversaAcAux xs ys = (inversa xs)@ys\"\nproof (induct xs arbitrary: ys) \n  show \"\u22c0ys. inversaAcAux [] ys = inversa [] @ ys\" by simp\nnext\n  fix x xs zs\n  assume hi: \"\u22c0ys. inversaAcAux xs ys = inversa xs @ ys\"\n  show \"inversaAcAux (x#xs) zs = inversa (x#xs) @ zs\"\n  proof -\n    have \"inversaAcAux (x#xs) zs = inversaAcAux xs (x#zs)\" by simp\n    also have \"... = inversa xs @ (x#zs)\" using hi by simp\n    also have \"... = inversa xs @ [x] @ zs\" by simp\n    also have \"... = inversa (x#xs) @ zs\" by simp\n    finally show ?thesis .\n  qed\nqed\n\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 21. Demostrar que \n     inversaAc xs = inversa xs\n  ------------------------------------------------------------------- *}\n\ncorollary \"inversaAc xs = inversa xs\"\nby (simp add: inversaAcAux_es_inversa)\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 22. Definir la funci\u00f3n\n     sum :: \"int list \u21d2 int\" \n  tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,\n     sum [3,2,5] = 10\n  ------------------------------------------------------------------ *}\n\nfun sum :: \"int list \u21d2 int\" where\n  \"sum []     = 0\"\n| \"sum (x#xs) = x + sum xs\"\n\nvalue \"sum [3,2,5]\" -- \"= 10\"\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 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,2,5] = [6,4,10]\n  ------------------------------------------------------------------ *}\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::int,2,5]\" -- \"= [6,4,10]\"\n\nvalue \"map (\u03bbx. 6*x) [3::int,2,5]\" -- \"= [18,12,30]\"\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 24. Demostrar que \n     sum (map (\u03bbx. 2*x) xs) = 2 * (sum xs)\n  ------------------------------------------------------------------- *}\n\nlemma \"sum (map (\u03bbx. 2*x) xs) = 2 * (sum xs)\"\nby (induct xs) auto\n\nlemma sum_map:\n  \"sum (map (\u03bbx. 2*x) xs) = 2 * (sum xs)\"\nproof (induct xs)\n  show \"sum (map (\u03bbx. 2*x) []) = 2 * (sum [])\" by simp\nnext\n  fix a xs\n  assume hi: \"sum (map (\u03bbx. 2*x) xs) = 2 * (sum xs)\"\n  show \"sum (map (\u03bbx. 2*x) (a#xs)) = 2 * (sum (a#xs))\"\n  proof -\n    have \"sum (map (\u03bbx. 2*x) (a#xs)) = sum ((2*a)#(map (\u03bbx. 2*x) xs))\" by simp\n    also have \"... = 2*a + sum (map (\u03bbx. 2*x) xs)\" by simp\n    also have \"... = 2*a + 2 * (sum xs)\" using hi by simp\n    also have \"... = 2*(a + sum xs)\" by simp\n    also have \"... = 2 * (sum (a#xs))\"by simp\n    finally show ?thesis .\n  qed\nqed\n\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 25. Demostrar que \n     longitud (map f xs) = longitud xs\n  ------------------------------------------------------------------- *}\n\nlemma \"longitud (map f xs) = longitud xs\"\nby (induct xs) auto\n\nlemma long_map:\n  \"longitud (map f xs) = longitud xs\"\nproof (induct xs) \n  show \"longitud (map f []) = longitud []\" by simp\nnext\n  fix x xs\n  assume hi: \"longitud (map f xs) = longitud xs\"\n  show \"longitud (map f (x#xs)) = longitud (x#xs)\"\n  proof -\n    have \"longitud (map f (x#xs)) = longitud ((f x)#(map f xs))\" by simp\n    also have \"... = 1 + longitud (map f xs)\" by simp\n    also have \"... = 1 + longitud xs\" using hi by simp\n    also have \"... = longitud (x#xs)\" by simp\n    finally show ?thesis .\n  qed\nqed\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos se ha estudiado c\u00f3m escribir programas funcionales y c\u00f3mo demostrar sus propiedades con Isabelle\/HOL. En la presentaci\u00f3n se han usado los ejemplos del tema 8 del curso de Inform\u00e1tica (de 1\u00ba del Grado en Matem\u00e1ticas). La teor\u00eda correspondiente es<\/p>\n","protected":false},"author":2,"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,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[234],"tags":[144,303],"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\/4317"}],"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=4317"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4317\/revisions"}],"predecessor-version":[{"id":4319,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4317\/revisions\/4319"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4317"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4317"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4317"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}