{"id":3860,"date":"2013-11-28T19:28:29","date_gmt":"2013-11-28T18:28:29","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3860"},"modified":"2016-03-29T17:22:16","modified_gmt":"2016-03-29T15:22:16","slug":"ra2013-razonamiento-estructurado-sobre-programas-con-isabellehol-2","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2013-razonamiento-estructurado-sobre-programas-con-isabellehol-2\/","title":{"rendered":"RA2013: Razonamiento estructurado sobre programas con Isabelle\/HOL (2)"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-13\">Razonamiento autom\u00e1tico<\/a> hemos continuado la presentaci\u00f3n de c\u00f3mo se puede demostrar detalladamente propiedades de programas funcionales con Isabelle\/HOL.<\/p>\n<p>Para ello, se visto c\u00f3mo representar en Isabelle\/HOL las demostraciones de propiedades de programas estudiadas en el  <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-15\/temas\/tema-8.pdf\">tema 2a<\/a> (que se corresponden con el cap\u00edtulo 13 del libro de G. Hutton <a href=\"http:\/\/bit.ly\/1gMqK0X\">Programming in Haskell<\/a>).<\/p>\n<p>Las demostraciones estudiadas son las correspondientes a las p\u00e1ginas 38 a 50 del <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-15\/temas\/tema-8.pdf\">tema 2a<\/a>. Los m\u00e9todos de demostraci\u00f3n utilizados son razonamiento ecuacional, inducci\u00f3n sobre los n\u00fameros naturales, inducci\u00f3n sobre listas e inducci\u00f3n sobre esquemas correspondientes a definiciones recursivas.<\/p>\n<p>La teor\u00eda con los ejemplos presentados en la clase es la siguiente:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nheader {* Tema 3: Razonamiento estructurado sobre programas *}\n\ntheory T3\nimports Main \nbegin\n\nsection {* Razonamiento por casos *}\n\ntext {* --------------------------------------------------------------- \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  ------------------------------------------------------------------ *}\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  Ejemplo 18 (p. 39) . Demostrar que \n     esVacia xs = esVacia (conc xs xs)\n  ------------------------------------------------------------------- *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma \"esVacia xs = esVacia (conc xs xs)\"\nproof (cases xs)\n  assume \"xs = []\"\n  then show \"esVacia xs = esVacia (conc xs xs)\" by simp\nnext\n  fix y ys\n  assume \"xs = y#ys\"\n  then show \"esVacia xs = esVacia (conc xs xs)\" by simp\nqed\n\ntext {*\n  Comentarios 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*}\n\n-- \"La demostraci\u00f3n estructurada simplificada es\"\nlemma \"esVacia xs = esVacia (conc xs xs)\"\nproof (cases xs)\n  case Nil\n  then show \"esVacia xs = esVacia (conc xs xs)\" by simp\nnext\n  case Cons\n  then show \"esVacia xs = esVacia (conc xs xs)\" by simp\nqed\n\ntext {*\n  Comentarios 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\"\n  \u00b7 \"thus\" es una abreviatura de \"then show\".\n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"esVacia xs = esVacia (conc xs xs)\"\nby (cases xs) auto\n\nsection {* Heur\u00edstica de generalizaci\u00f3n *}\n\ntext {* \n  Heur\u00edstica de generalizaci\u00f3n: Cuando se use demostraci\u00f3n estructural,\n  cuantificar universalmente las variables libres (o, equivalentemente,\n  considerar las variables libres como variables arbitrarias). *}\n\ntext {* --------------------------------------------------------------- \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  ------------------------------------------------------------------ *}\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 [a,c,b,e]\" -- \"= [e,b,c,a]\"\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 20. (p. 44) Demostrar que \n     inversaAcAux xs ys = (inversa xs) @ ys\n  ------------------------------------------------------------------- *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma inversaAcAux_es_inversa:\n  \"inversaAcAux xs ys = (inversa xs) @ ys\"\nproof (induct xs arbitrary: ys)\n  show \"\u22c0ys. inversaAcAux [] ys = inversa [] @ ys\" by simp\nnext\n  fix a xs \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)\" by simp\n    also have \"\u2026 = inversa xs@(a#ys)\" using HI by simp\n    also have \"\u2026 = inversa (a#xs)@ys\" by simp \n    finally show \"inversaAcAux (a#xs) ys = inversa (a#xs)@ys\" by simp\n  qed\nqed\n\ntext {*\n  Comentarios 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)\". \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"inversaAcAux xs ys = (inversa xs)@ys\"\nby (induct xs arbitrary: ys) auto\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 21. (p. 43) Demostrar que \n     inversaAc xs = inversa xs\n  ------------------------------------------------------------------- *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\ncorollary \"inversaAc xs = inversa xs\"\nby (simp add: inversaAcAux_es_inversa)\n\ntext {*\n  Comentario de la demostraci\u00f3n anterior:\n  \u00b7 \"(simp add: inversaAcAux_es_inversa)\" es el m\u00e9todo de demostraci\u00f3n\n    por simplificaci\u00f3n usando como regla de simplificaci\u00f3n la propiedad\n    inversaAcAux_es_inversa. \n*}\n\nsection {* Demostraci\u00f3n por inducci\u00f3n para funciones de orden superior *}\n\ntext {* --------------------------------------------------------------- \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  ------------------------------------------------------------------ *}\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 {* --------------------------------------------------------------- \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,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::nat,2,5]\" -- \"= [6,4,10]\"\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 24. (p. 45) Demostrar que \n     sum (map (\u03bbx. 2*x) xs) = 2 * (sum xs)\n  ------------------------------------------------------------------- *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma \"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  have \"sum (map (\u03bbx. 2*x) (a#xs)) = sum ((2*a)#(map (\u03bbx. 2*x) xs))\" \n    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 \"sum (map (\u03bbx. 2*x) (a#xs)) = 2*(sum (a#xs))\" by simp\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"sum (map (\u03bbx. 2*x) xs) = 2 * (sum xs)\"\nby (induct xs) auto\n\ntext {* --------------------------------------------------------------- \n  Ejemplo 25. (p. 48) Demostrar que \n     longitud (map f xs) = longitud xs\n  ------------------------------------------------------------------- *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma \"longitud (map f xs) = longitud xs\"\nproof (induct xs)\n  show \"longitud (map f []) = longitud []\" 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))\" 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 (a#xs)\" by simp\n  finally show \"longitud (map f (a#xs)) = longitud (a#xs)\" by simp\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"longitud (map f xs) = longitud xs\"\nby (induct xs) auto\n\nsection {* Referencias *}\n\ntext {*\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*}\n\nend\n<\/pre>\n<p>Como tarea para la pr\u00f3xima clase se propuso la resoluci\u00f3n de los ejercicios de la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/ejerciciosRA2013\/index.php5\/R4\">relaci\u00f3n 4<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de Razonamiento autom\u00e1tico hemos continuado la presentaci\u00f3n de c\u00f3mo se puede demostrar detalladamente propiedades de programas funcionales con Isabelle\/HOL. Para ello, se visto c\u00f3mo representar en Isabelle\/HOL las demostraciones de propiedades de programas estudiadas en el tema 2a (que se corresponden con el cap\u00edtulo 13 del libro de&#8230;<\/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":[227],"tags":[144,302],"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\/3860"}],"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=3860"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3860\/revisions"}],"predecessor-version":[{"id":5376,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3860\/revisions\/5376"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3860"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3860"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3860"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}