{"id":2410,"date":"2012-12-13T19:33:26","date_gmt":"2012-12-13T19:33:26","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/dao2012-razonamiento-sobre-programas-con-isabelle\/"},"modified":"2013-03-08T05:47:36","modified_gmt":"2013-03-08T05:47:36","slug":"dao2012-razonamiento-sobre-programas-con-isabelle","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/dao2012-razonamiento-sobre-programas-con-isabelle\/","title":{"rendered":"DAO2012: Razonamiento sobre programas con Isabelle"},"content":{"rendered":"<p>En la sesi\u00f3n de hoy del seminario <a href=\"https:\/\/www.glc.us.es\/~jalonso\/DAO2012\">Demostraci\u00f3n asistida por ordenador (DAO2012)<\/a> se ha presentado c\u00f3mo se puede demostrar con Isabelle propiedades de programas.<\/p>\n<p>En el <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-11\/temas\/tema-8t.pdf\">tema 8<\/a> del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-11\">I1M<\/a> vimos c\u00f3mo se puede razonar sobre programas funcionales. Hoy hemos visto c\u00f3mo Isabelle puede hacer autom\u00e1ticamente las demostraciones de dicho tema. Los m\u00e9todos que hemos usado son<\/p>\n<ul>\n<li> simplificaci\u00f3n (con <i>simp<\/i>),\n<li> autom\u00e1tico (con <i>auto<\/i>),\n<li> inducci\u00f3n sobre n\u00fameros naturales y listas (con <i>induct<\/i>),\n<li> inducci\u00f3n con variables libres (con <i>arbitrary<\/i>) y\n<li> inducci\u00f3n en varias variables (con <i>induct rule<\/i>).\n<\/ul>\n<p>La teor\u00eda correspondiente a la clase es <a href=\"https:\/\/www.glc.us.es\/~jalonso\/DAO2012\/index.php5\/Tema_3:_Razonamiento_sobre_programas\">T3_Razonamiento_sobre_programas.thy<\/a> cuyo contenido se muestra a continuaci\u00f3n<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\nheader {* Tema 3: Razonamiento sobre programas *}\r\n\r\ntheory T3_Razonamiento_sobre_programas\r\nimports Main \r\nbegin\r\n\r\ntext {* ----------------------------------------------------------------\r\n  Ejemplo 1. Definir, por recursi\u00f3n, la funci\u00f3n\r\n     longitud :: 'a list \u21d2 nat\r\n  tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,\r\n     longitud [4,2,5] = 3\r\n  ------------------------------------------------------------------- *}\r\n\r\nfun longitud :: \"'a list \u21d2 nat\" where\r\n  \"longitud []     = 0\"\r\n| \"longitud (x#xs) = 1 + longitud xs\"\r\n   \r\nvalue \"longitud [4,2,5]\" -- \"= 3\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 2. Demostrar que \r\n     longitud [4,2,5] = 3\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"longitud [4,2,5] = 3\"\r\nby simp\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 3. Definir la funci\u00f3n\r\n     fun intercambia :: 'a \u00d7 'b \u21d2 'b \u00d7 'a\r\n  tal que (intercambia p) es el par obtenido intercambiando las\r\n  componentes del par p. Por ejemplo,\r\n     intercambia (u,v) = (v,u)\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun intercambia :: \"'a \u00d7 'b \u21d2 'b \u00d7 'a\" where\r\n  \"intercambia (x,y) = (y,x)\"\r\n\r\nvalue \"intercambia (u,v)\" -- \"= (v,u)\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 4. Demostrar que \r\n     intercambia (intercambia (x,y)) = (x,y)\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"intercambia (intercambia (x,y)) = (x,y)\"\r\nby simp\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 5. Definir, por recursi\u00f3n, la funci\u00f3n\r\n     inversa :: 'a list \u21d2 'a list\r\n  tal que (inversa xs) es la lista obtenida invirtiendo el orden de los\r\n  elementos de xs. Por ejemplo,\r\n     inversa [a,d,c] = [c,d,a]\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun inversa :: \"'a list \u21d2 'a list\" where\r\n  \"inversa []     = []\"\r\n| \"inversa (x#xs) = inversa xs @ [x]\"\r\n\r\nvalue \"inversa [a,d,c]\" -- \"= [c,d,a]\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 6. Demostrar que \r\n     inversa [x] = [x]\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"inversa [x] = [x]\"\r\nby simp\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 7. Definir la funci\u00f3n\r\n     repite :: nat \u21d2 'a \u21d2 'a list\r\n  tal que (repite n x) es la lista formada por n copias del elemento\r\n  x. Por ejemplo, \r\n     repite 3 a = [a,a,a]\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun repite :: \"nat \u21d2 'a \u21d2 'a list\" where\r\n  \"repite 0 x       = []\"\r\n| \"repite (Suc n) x = x # (repite n x)\"\r\n\r\nvalue \"repite 3 a\" -- \"= [a,a,a]\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 8. Demostrar que \r\n     longitud (repite n x) = n\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"longitud (repite n x) = n\"\r\nby (induct n) auto\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 9. Definir la funci\u00f3n\r\n     conc :: 'a list \u21d2 'a list \u21d2 'a list\r\n  tal que (conc xs ys) es la concatenci\u00f3n de las listas xs e ys. Por\r\n  ejemplo, \r\n     conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]\r\n  ------------------------------------------------------------------ *}\r\n\r\nfun conc :: \"'a list \u21d2 'a list \u21d2 'a list\" where\r\n  \"conc []     ys = ys\"\r\n| \"conc (x#xs) ys = x # (conc xs ys)\"\r\n\r\nvalue \"conc [a,d] [b,d,a,c]\" -- \"= [a,d,b,d,a,c]\"\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 10. Demostrar que \r\n     conc xs (conc ys zs) = (conc xs ys) zs\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"conc xs (conc ys zs) = conc (conc xs ys) zs\"\r\nby (induct xs) auto\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 11. Refutar que \r\n     conc xs ys = conc ys xs\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"conc xs ys = conc ys xs\"\r\nquickcheck\r\noops\r\n\r\ntext {* Encuentra el contraejemplo, \r\n  xs = [a\\<^isub>2]\r\n  ys = [a\\<^isub>1] *}\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 12. Demostrar que \r\n     conc xs [] = xs\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"conc xs [] = xs\"\r\nby (induct xs) auto\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 13. Demostrar que \r\n     longitud (conc xs ys) = longitud xs + longitud ys\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"longitud (conc xs ys) = longitud xs + longitud ys\"\r\nby (induct xs) auto\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  Ejemplo 16. Demostrar que \r\n     conc (coge n xs) (elimina n xs) = xs\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"conc (coge n xs) (elimina n xs) = xs\"\r\nby (induct rule: coge.induct) auto\r\n\r\ntext {* coge.induct es el esquema de inducci\u00f3n asociado a la definici\u00f3n\r\n  de la funci\u00f3n coge. \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  Puede verse usando \"thm coge.induct\". *}\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. Demostrar que \r\n     esVacia xs = esVacia (conc xs xs)\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"esVacia xs = esVacia (conc xs xs)\"\r\nby (induct xs) auto\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. Demostrar que \r\n     inversaAcAux xs ys = (inversa xs)@ys\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma inversaAcAux_es_inversa:\r\n  \"inversaAcAux xs ys = (inversa xs)@ys\"\r\nby (induct xs arbitrary: ys) auto\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 21. Demostrar que \r\n     inversaAc xs = inversa xs\r\n  ------------------------------------------------------------------- *}\r\n\r\ncorollary \"inversaAc xs = inversa xs\"\r\nby (simp add: inversaAcAux_es_inversa)\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. Demostrar que \r\n     sum (map (\u03bbx. 2*x) xs) = 2 * (sum xs)\r\n  ------------------------------------------------------------------- *}\r\n\r\nlemma \"sum (map (\u03bbx. 2*x) xs) = 2 * (sum xs)\"\r\nby (induct xs) auto\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 25. Demostrar que \r\n     longitud (map f xs) = longitud xs\r\n  ------------------------------------------------------------------- *}\r\n\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 sesi\u00f3n de hoy del seminario Demostraci\u00f3n asistida por ordenador (DAO2012) se ha presentado c\u00f3mo se puede demostrar con Isabelle propiedades de programas. En el tema 8 del curso de I1M vimos c\u00f3mo se puede razonar sobre programas funcionales. Hoy hemos visto c\u00f3mo Isabelle puede hacer autom\u00e1ticamente las demostraciones de dicho tema. Los m\u00e9todos&#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":[201,144],"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\/2410"}],"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=2410"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2410\/revisions"}],"predecessor-version":[{"id":2722,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2410\/revisions\/2722"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2410"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2410"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2410"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}