{"id":3225,"date":"2013-04-11T21:34:08","date_gmt":"2013-04-11T21:34:08","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3225"},"modified":"2013-04-13T11:34:59","modified_gmt":"2013-04-13T11:34:59","slug":"ra2012-razonamiento-sobre-programas-con-isabellehol-1","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2012-razonamiento-sobre-programas-con-isabellehol-1\/","title":{"rendered":"RA2012: Razonamiento sobre programas con Isabelle\/HOL (1)"},"content":{"rendered":"<p>En la segunda 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 presentado 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\ntext {* \r\n  En este tema se demuestra con Isabelle las propiedades de los\r\n  programas funcionales como se expone en el tema 8 del curso\r\n  \"Inform\u00e1tica\" que puede leerse en http:\/\/goo.gl\/Imvyt *}\r\n\r\nsection {* Razonamiento ecuacional *}\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. (p.6) Demostrar que \r\n     intercambia (intercambia (x,y)) = (x,y)\r\n  ------------------------------------------------------------------- *}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma \"intercambia (intercambia (x,y)) = (x,y)\"\r\nproof -\r\n  have \"intercambia (intercambia (x,y)) = intercambia (y,x)\"  \r\n    by (simp only: intercambia.simps)\r\n  also have \"... = (x,y)\" \r\n    by (simp only: intercambia.simps)\r\n  finally show \"intercambia (intercambia (x,y)) = (x,y)\" by simp\r\nqed\r\n\r\ntext {* \r\n  El razonamiento ecuacional se realiza usando la combinaci\u00f3n de \"also\"\r\n  (adem\u00e1s) y \"finally\" (finalmente). *}\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma \"intercambia (intercambia (x,y)) = (x,y)\"\r\nproof -\r\n  have \"intercambia (intercambia (x,y)) = intercambia (y,x)\"  by simp\r\n  also have \"... = (x,y)\" by simp \r\n  finally show \"intercambia (intercambia (x,y)) = (x,y)\" by simp\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\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. (p. 9) Demostrar que \r\n     inversa [x] = [x]\r\n  ------------------------------------------------------------------- *}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma \"inversa [x] = [x]\"\r\nproof -\r\n  have \"inversa [x] = inversa (x#[])\" by simp\r\n  also have \"... = (inversa []) @ [x]\" by (simp only: inversa.simps(2))\r\n  also have \"... = [] @ [x]\" by (simp only: inversa.simps(1))\r\n  also have \"... = [x]\" by (simp only: append_Nil) \r\n  finally show \"inversa [x] = [x]\" by simp\r\nqed\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma \"inversa [x] = [x]\"\r\nproof -\r\n  have \"inversa [x] = inversa (x#[])\" by simp\r\n  also have \"... = (inversa []) @ [x]\" by simp\r\n  also have \"... = [] @ [x]\" by simp\r\n  also have \"... = [x]\" by simp \r\n  finally show \"inversa [x] = [x]\" by simp\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"inversa [x] = [x]\"\r\nby simp\r\n\r\nsection {* Razonamiento por inducci\u00f3n sobre los naturales *}\r\n\r\ntext {*\r\n  [Principio de inducci\u00f3n sobre los naturales] Para demostrar una\r\n  propiedad P para todos los n\u00fameros naturales basta probar que el 0\r\n  tiene la propiedad P y que si n tiene la propiedad P, entonces n+1\r\n  tambi\u00e9n la tiene.  \r\n     \u27e6P 0; \u22c0n. P n \u27f9 P (Suc n)\u27e7 \u27f9 P m\r\n\r\n  En Isabelle el principio de inducci\u00f3n sobre los naturales est\u00e1\r\n  formalizado en el teorema nat.induct y puede verse con\r\n     thm nat.induct\r\n*}\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. (p. 18) Demostrar que \r\n     longitud (repite n x) = n\r\n  ------------------------------------------------------------------- *}\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma \"longitud (repite n x) = n\"\r\nproof (induct n)\r\n  show \"longitud (repite 0 x) = 0\" by simp\r\nnext \r\n  fix n\r\n  assume HI: \"longitud (repite n x) = n\"\r\n  have \"longitud (repite (Suc n) x) = longitud (x # (repite n x))\" \r\n    by simp\r\n  also have \"... = 1 + longitud (repite n x)\" by simp\r\n  also have \"... = 1 + n\" using HI by simp\r\n  finally show \"longitud (repite (Suc n) x) = Suc n\" by simp\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"longitud (repite n x) = n\"\r\nby (induct n) auto\r\n\r\nsection {* Razonamiento por inducci\u00f3n sobre listas *}\r\n\r\ntext {*\r\n  Para demostrar una propiedad para todas las listas basta demostrar\r\n  que la lista vac\u00eda tiene la propiedad y que al a\u00f1adir un elemento a una\r\n  lista que tiene la propiedad se obtiene otra lista que tambi\u00e9n tiene la\r\n  propiedad. \r\n\r\n  En Isabelle el principio de inducci\u00f3n sobre listas est\u00e1 formalizado\r\n  mediante el teorema list.induct que puede verse con \r\n     thm list.induct\r\n*}\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. (p. 24) Demostrar que \r\n     conc xs (conc ys zs) = (conc xs ys) zs\r\n  ------------------------------------------------------------------- *}\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma \"conc xs (conc ys zs) = conc (conc xs ys) zs\"\r\nproof (induct xs)\r\n  show \"conc [] (conc ys zs) = conc (conc [] ys) zs\" by simp\r\nnext\r\n  fix x xs\r\n  assume HI: \"conc xs (conc ys zs) = conc (conc xs ys) zs\" \r\n  have \"conc (x # xs) (conc ys zs) = x # (conc xs (conc ys zs))\" by simp\r\n  also have \"... = x # (conc (conc xs ys) zs)\" using HI by simp\r\n  also have \"... = conc (conc (x # xs) ys) zs\" by simp\r\n  finally show \"conc (x # xs) (conc ys zs) = conc (conc (x # xs) ys) zs\" by simp\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\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. (p. 28) Demostrar que \r\n     conc xs [] = xs\r\n  ------------------------------------------------------------------- *}\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma \"conc xs [] = xs\"\r\nproof (induct xs)\r\n  show \"conc [] [] = []\" by simp\r\nnext \r\n  fix x xs\r\n  assume HI: \"conc xs [] = xs\" \r\n  have \"conc (x # xs) [] = x # (conc xs [])\" by simp\r\n  also have \"... = x # xs\" using HI by simp\r\n  finally show \"conc (x # xs) [] = x # xs\" by simp\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"conc xs [] = xs\"\r\nby (induct xs) auto\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejemplo 13. (p. 30) Demostrar que \r\n     longitud (conc xs ys) = longitud xs + longitud ys\r\n  ------------------------------------------------------------------- *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"longitud (conc xs ys) = longitud xs + longitud ys\"\r\nproof (induct xs)\r\n  show \"longitud (conc [] ys) = longitud [] + longitud ys\" by simp\r\nnext\r\n  fix x xs\r\n  assume HI: \"longitud (conc xs ys) = longitud xs + longitud ys\"\r\n  have \"longitud (conc (x # xs) ys) = longitud (x # (conc xs ys))\" \r\n    by simp\r\n  also have \"... = 1 + longitud (conc xs ys)\" by simp\r\n  also have \"... = 1 + longitud xs + longitud ys\" using HI by simp\r\n  also have \"... = longitud (x # xs) + longitud ys\" by simp\r\n  finally show \"longitud (conc (x # xs) ys) = \r\n                longitud (x # xs) + longitud ys\" by simp\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"longitud (conc xs ys) = longitud xs + longitud ys\"\r\nby (induct xs) auto\r\n\r\nsection {* Inducci\u00f3n correspondiente a la 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\nend\r\n<\/pre>\n<p>Como tarea se propuso la resoluci\u00f3n de los ejercicios de la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/DAO\/index.php5\/RA12_Relaci%C3%B3n_8h\">relaci\u00f3n 8<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la segunda parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se ha presentado 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 Matem\u00e1ticas). La teor\u00eda con los ejemplos presentados 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\/3225"}],"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=3225"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3225\/revisions"}],"predecessor-version":[{"id":3226,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3225\/revisions\/3226"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3225"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3225"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3225"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}