{"id":3261,"date":"2013-04-25T17:00:38","date_gmt":"2013-04-25T17:00:38","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3261"},"modified":"2013-04-26T12:12:11","modified_gmt":"2013-04-26T12:12:11","slug":"ra2012-razonamiento-sobre-programas-con-isabellehol-2","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2012-razonamiento-sobre-programas-con-isabellehol-2\/","title":{"rendered":"RA2012: Razonamiento sobre programas con Isabelle\/HOL (2)"},"content":{"rendered":"<p>En la primera parte de la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra\">Razonamiento autom\u00e1tico<\/a> se ha continuado la presentaci\u00f3n (iniciada en la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2012-razonamiento-sobre-programas-con-isabellehol-1\/\">clase anterior<\/a>) de c\u00f3mo se puede demostrar propiedades de programas funcionales 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 con los ejemplos presentados en la clase es la siguiente:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\nheader {* Tema 5: Razonamiento sobre programas *}\r\n\r\ntheory T5\r\nimports Main \r\nbegin\r\n\r\nsection {* Inducci\u00f3n correspondiente a una definici\u00f3n recursiva *}\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 14. Definir la funci\u00f3n\r\n     coge :: nat \u21d2 'a list \u21d2 'a list\r\n  tal que (coge n xs) es la lista de los n primeros elementos de xs. Por \r\n  ejemplo, \r\n     coge 2 [a,c,d,b,e] = [a,c]\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun coge :: \"nat \u21d2 'a list \u21d2 'a list\" where\r\n  \"coge n []           = []\"\r\n| \"coge 0 xs           = []\"\r\n| \"coge (Suc n) (x#xs) = x # (coge n xs)\"\r\n\r\nvalue \"coge 2 [a,c,d,b,e]\" -- \"= [a,c]\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 15. Definir la funci\u00f3n\r\n     elimina :: nat \u21d2 'a list \u21d2 'a list\r\n  tal que (elimina n xs) es la lista obtenida eliminando los n primeros\r\n  elementos de xs. Por ejemplo, \r\n     elimina 2 [a,c,d,b,e] = [d,b,e]\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun elimina :: \"nat \u21d2 'a list \u21d2 'a list\" where\r\n  \"elimina n []           = []\"\r\n| \"elimina 0 xs           = xs\"\r\n| \"elimina (Suc n) (x#xs) = elimina n xs\"\r\n\r\nvalue \"elimina 2 [a,c,d,b,e]\" -- \"= [d,b,e]\"\r\n\r\ntext {* \r\n  La definici\u00f3n coge genera el esquema de inducci\u00f3n coge.induct:\r\n     \u27e6\u22c0n. P n []; \r\n      \u22c0x xs. P 0 (x#xs); \r\n      \u22c0n x xs. P n xs \u27f9 P (Suc n) (x#xs)\u27e7\r\n     \u27f9 P n x\r\n\r\n  Puede verse usando \"thm coge.induct\". *}\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 16. (p. 35) Demostrar que \r\n     conc (coge n xs) (elimina n xs) = xs\r\n  ------------------------------------------------------------------- *}\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma \"conc (coge n xs) (elimina n xs) = xs\"\r\nproof (induct rule: coge.induct)\r\n  fix n\r\n  show \"conc (coge n []) (elimina n []) = []\" by simp\r\nnext\r\n  fix x xs\r\n  show \"conc (coge 0 (x#xs)) (elimina 0 (x#xs)) = x#xs\" by simp\r\nnext\r\n  fix n x xs\r\n  assume HI: \"conc (coge n xs) (elimina n xs) = xs\"\r\n  have \"conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = \r\n        conc (x#(coge n xs)) (elimina n xs)\" by simp\r\n  also have \"... = x#(conc (coge n xs) (elimina n xs))\" by simp\r\n  also have \"... = x#xs\" using HI by simp  \r\n  finally show \"conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = x#xs\"\r\n    by simp\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"conc (coge n xs) (elimina n xs) = xs\"\r\nby (induct rule: coge.induct) auto\r\n\r\nsection {* Razonamiento por casos *}\r\n\r\ntext {*\r\n  Distinci\u00f3n de casos sobre listas:\r\n  \u00b7 El m\u00e9todo de distinci\u00f3n de casos se activa con (cases xs) donde xs\r\n    es del tipo lista. \r\n  \u00b7 \"case Nil\" es una abreviatura de \r\n       \"assume Nil: xs =[]\".\r\n  \u00b7 \"case Cons\" es una abreviatura de \r\n       \"fix ? ?? assume Cons: xs = ? # ??\"\r\n    donde ? y ?? son variables an\u00f3nimas. *}\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 17. Definir la funci\u00f3n\r\n     esVacia :: 'a list \u21d2 bool\r\n  tal que (esVacia xs) se verifica si xs es la lista vac\u00eda. Por ejemplo,\r\n     esVacia []  = True\r\n     esVacia [1] = False\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun esVacia :: \"'a list \u21d2 bool\" where\r\n  \"esVacia []     = True\"\r\n| \"esVacia (x#xs) = False\"\r\n\r\nvalue \"esVacia []\"  -- \"= True\"\r\nvalue \"esVacia [1]\" -- \"= False\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 18 (p. 39) . Demostrar que \r\n     esVacia xs = esVacia (conc xs xs)\r\n  ------------------------------------------------------------------- *}\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma \"esVacia xs = esVacia (conc xs xs)\"\r\nproof (cases xs)\r\n  assume \"xs = []\"\r\n  thus \"esVacia xs = esVacia (conc xs xs)\" by simp\r\nnext\r\n  fix y ys\r\n  assume \"xs = y#ys\"\r\n  thus \"esVacia xs = esVacia (conc xs xs)\" by simp\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada simplificad es\"\r\nlemma \"esVacia xs = esVacia (conc xs xs)\"\r\nproof (cases xs)\r\n  case Nil\r\n  thus \"esVacia xs = esVacia (conc xs xs)\" by simp\r\nnext\r\n  case Cons\r\n  thus \"esVacia xs = esVacia (conc xs xs)\" by simp\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"esVacia xs = esVacia (conc xs xs)\"\r\nby (cases xs) auto\r\n\r\nsection {* Heur\u00edstica de generalizaci\u00f3n *}\r\n\r\ntext {* \r\n  Heur\u00edstica de generalizaci\u00f3n: Cuando se use demostraci\u00f3n estructural,\r\n  cuantificar universalmente las variables libres (o, equivalentemente,\r\n  considerar las variables libres como variables arbitrarias). *}\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 19. Definir la funci\u00f3n\r\n     inversaAc :: 'a list \u21d2 'a list\r\n  tal que (inversaAc xs) es a inversa de xs calculada usando\r\n  acumuladores. Por ejemplo, \r\n     inversaAc [a,c,b,e] = [e,b,c,a]\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun inversaAcAux :: \"'a list \u21d2 'a list \u21d2 'a list\" where\r\n  \"inversaAcAux [] ys     = ys\"\r\n| \"inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)\"\r\n\r\nfun inversaAc :: \"'a list \u21d2 'a list\" where\r\n  \"inversaAc xs = inversaAcAux xs []\"\r\n\r\nvalue \"inversaAc [a,c,b,e]\" -- \"= [e,b,c,a]\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 20. (p. 44) Demostrar que \r\n     inversaAcAux xs ys = (inversa xs) @ ys\r\n  ------------------------------------------------------------------- *}\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma inversaAcAux_es_inversa:\r\n  \"inversaAcAux xs ys = (inversa xs) @ ys\"\r\nproof (induct xs arbitrary: ys)\r\n  show \"\u22c0ys. inversaAcAux [] ys = inversa [] @ ys\" by simp\r\nnext\r\n  fix a xs \r\n  assume HI: \"\u22c0ys. inversaAcAux xs ys = inversa xs@ys\"\r\n  show \"\u22c0ys. inversaAcAux (a#xs) ys = inversa (a#xs)@ys\"\r\n  proof -\r\n    fix ys\r\n    have \"inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)\" by simp\r\n    also have \"\u2026 = inversa xs@(a#ys)\" using HI by simp\r\n    also have \"\u2026 = inversa (a#xs)@ys\" by simp \r\n    finally show \"inversaAcAux (a#xs) ys = inversa (a#xs)@ys\" by simp\r\n  qed\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"inversaAcAux xs ys = (inversa xs)@ys\"\r\nby (induct xs arbitrary: ys) auto\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 21. (p. 43) Demostrar que \r\n     inversaAc xs = inversa xs\r\n  ------------------------------------------------------------------- *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\ncorollary \"inversaAc xs = inversa xs\"\r\nby (simp add: inversaAcAux_es_inversa)\r\n\r\nsection {* Demostraci\u00f3n por inducci\u00f3n para funciones de orden superior *}\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 22. Definir la funci\u00f3n\r\n     sum :: nat list \u21d2 nat\r\n  tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,\r\n     sum [3,2,5] = 10\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun sum :: \"nat list \u21d2 nat\" where\r\n  \"sum []     = 0\"\r\n| \"sum (x#xs) = x + sum xs\"\r\n\r\nvalue \"sum [3,2,5]\" -- \"= 10\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 23. Definir la funci\u00f3n\r\n     map :: ('a \u21d2 'b) \u21d2 'a list \u21d2 'b list\r\n  tal que (map f xs) es la lista obtenida aplicando la funci\u00f3n f a los\r\n  elementos de xs. Por ejemplo,\r\n     map (\u03bbx. 2*x) [3,2,5] = [6,4,10]\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun map :: \"('a \u21d2 'b) \u21d2 'a list \u21d2 'b list\" where\r\n  \"map f []     = []\"\r\n| \"map f (x#xs) = (f x) # map f xs\"\r\n\r\nvalue \"map (\u03bbx. 2*x) [3::nat,2,5]\" -- \"= [6,4,10]\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 24. (p. 45) Demostrar que \r\n     sum (map (\u03bbx. 2*x) xs) = 2 * (sum xs)\r\n  ------------------------------------------------------------------- *}\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma \"sum (map (\u03bbx. 2*x) xs) = 2 * (sum xs)\"\r\nproof (induct xs)\r\n  show \"sum (map (\u03bbx. 2*x) []) = 2 * (sum [])\" by simp\r\nnext\r\n  fix a xs\r\n  assume HI: \"sum (map (\u03bbx. 2*x) xs) = 2 * (sum xs)\"\r\n  have \"sum (map (\u03bbx. 2*x) (a#xs)) = sum ((2*a)#(map (\u03bbx. 2*x) xs))\" \r\n    by simp\r\n  also have \"... = 2*a + sum (map (\u03bbx. 2*x) xs)\" by simp\r\n  also have \"... = 2*a + 2*(sum xs)\" using HI by simp\r\n  also have \"... = 2*(a + sum xs)\" by simp\r\n  also have \"... = 2*(sum (a#xs))\" by simp\r\n  finally show \"sum (map (\u03bbx. 2*x) (a#xs)) = 2*(sum (a#xs))\" by simp\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"sum (map (\u03bbx. 2*x) xs) = 2 * (sum xs)\"\r\nby (induct xs) auto\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 25. (p. 48) Demostrar que \r\n     longitud (map f xs) = longitud xs\r\n  ------------------------------------------------------------------- *}\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma \"longitud (map f xs) = longitud xs\"\r\nproof (induct xs)\r\n  show \"longitud (map f []) = longitud []\" by simp\r\nnext\r\n  fix a xs\r\n  assume HI: \"longitud (map f xs) = longitud xs\"\r\n  have \"longitud (map f (a#xs)) = longitud (f a # (map f xs))\" by simp\r\n  also have \"... = 1 + longitud (map f xs)\" by simp\r\n  also have \"... = 1 + longitud xs\" using HI by simp\r\n  also have \"... = longitud (a#xs)\" by simp\r\n  finally show \"longitud (map f (a#xs)) = longitud (a#xs)\" by simp\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"longitud (map f xs) = longitud xs\"\r\nby (induct xs) auto\r\n\r\nsection {* Referencias *}\r\n\r\ntext {*\r\n  \u00b7 J.A. Alonso. \"Razonamiento sobre programas\" http:\/\/goo.gl\/R06O3\r\n  \u00b7 G. Hutton. \"Programming in Haskell\". Cap. 13 \"Reasoning about\r\n    programms\". \r\n  \u00b7 S. Thompson. \"Haskell: the Craft of Functional Programming, 3rd\r\n    Edition. Cap. 8 \"Reasoning about programms\". \r\n  \u00b7 L. Paulson. \"ML for the Working Programmer, 2nd Edition\". Cap. 6. \r\n    \"Reasoning about functional programs\". \r\n*}\r\n\r\nend\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la primera parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se ha continuado la presentaci\u00f3n (iniciada en la clase anterior) de c\u00f3mo se puede demostrar propiedades de programas funcionales 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&#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":[1],"tags":[144,203],"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\/3261"}],"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=3261"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3261\/revisions"}],"predecessor-version":[{"id":3262,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3261\/revisions\/3262"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3261"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3261"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3261"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}