{"id":6881,"date":"2019-11-28T23:49:15","date_gmt":"2019-11-28T22:49:15","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6881"},"modified":"2019-12-06T13:50:33","modified_gmt":"2019-12-06T12:50:33","slug":"ra2019-ejercicios-de-razonamiento-estructurado-sobre-programas-en-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2019-ejercicios-de-razonamiento-estructurado-sobre-programas-en-isabelle-hol\/","title":{"rendered":"RA2019: Ejercicios de razonamiento estructurado sobre programas en Isabelle\/HOL"},"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-19\">Razonamiento autom\u00e1tico<\/a> se han comentado las soluciones de la 3\u00aa relaci\u00f3n de ejercicios de razonamiento estructurado sobre programas. Para cada propiedad se dan tres demostraciones en Isabelle\/HOL: la primera autom\u00e1tica, la segunda estructurada y la tercera totalmente detallada mostrando todos los lemas de HOL que se utilizan en cada paso.<\/p>\n<p>La teor\u00eda con las soluciones de los ejercicios es la siguiente<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter \u2039R3: Razonamiento estructurado sobre programas\u203a\n\ntheory R3_Razonamiento_estructurado_sobre_programas_sol\nimports Main \nbegin\n\ntext \u2039Nota: De cada propiedad se debe de escribir primero la \n  demostraci\u00f3n autom\u00e1tica, a continuaci\u00f3n la estructurada y finalmente \n  la detallada (en la que se indica todos los detalles usando s\u00f3lo\n  \"by simp only: ...\" y \"by this\").\u203a\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 1.1. Definir la funci\u00f3n\n     sumaImpares :: nat \u21d2 nat\n  tal que (sumaImpares n) es la suma de los n primeros n\u00fameros\n  impares. Por ejemplo,\n     sumaImpares 5  =  25\n  ------------------------------------------------------------------\u203a\n\nfun sumaImpares :: \"nat \u21d2 nat\" where\n  \"sumaImpares 0 = 0\"\n| \"sumaImpares (Suc n) = sumaImpares n + (2*n+1)\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 1.2. Escribir la demostraci\u00f3n detallada de \n     sumaImpares n = n*n\n  -------------------------------------------------------------------\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma \"sumaImpares n = n*n\"\n  by (induct n) simp_all\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma \"sumaImpares n = n*n\"\nproof (induct n)\n  show \"sumaImpares 0 = 0 * 0\" by simp\nnext\n  fix n\n  assume HI: \"sumaImpares n = n * n\"\n  have \"sumaImpares (Suc n) = sumaImpares n + (2*n+1)\" by simp\n  also have \"... = n*n + (2*n+1)\" using HI by simp\n  also have \"... = Suc n * Suc n\" by simp\n  finally show \"sumaImpares (Suc n) = Suc n * Suc n\" by simp\nqed\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma \"sumaImpares n = n*n\"\nproof (induct n)\n  have \"sumaImpares 0 = 0\"\n    by (simp only: sumaImpares.simps(1))\n  also have \"... = 0*0\"\n    by (simp only: mult_0)\n  finally show \"sumaImpares 0 = 0*0\"\n    by this\nnext\n  fix n\n  assume HI: \"sumaImpares n = n*n\"\n  have \"sumaImpares (Suc n) = sumaImpares n + (2*n+1)\"\n    by (simp only: sumaImpares.simps(2))\n  also have \"... = n*n+(2*n+1)\"\n    by (simp only: HI)\n  also have \"... = n*(n+1)+1*(n+1)\"\n    by (simp only: add_mult_distrib2)\n  also have \"... = (n+1)*(n+1)\"\n    by (simp only: add_mult_distrib)\n  also have \"... = (Suc n)*(Suc n)\"\n    by (simp only: Suc_eq_plus1)\n  finally show \"sumaImpares (Suc n) = (Suc n)*(Suc n)\"\n    by this\nqed\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 2.1. Definir la funci\u00f3n\n     sumaPotenciasDeDosMasUno :: nat \u21d2 nat\n  tal que \n     (sumaPotenciasDeDosMasUno n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n. \n  Por ejemplo, \n     sumaPotenciasDeDosMasUno 3  =  16\n  ------------------------------------------------------------------\u203a\n\nfun sumaPotenciasDeDosMasUno :: \"nat \u21d2 nat\" where\n  \"sumaPotenciasDeDosMasUno 0 = 2\"\n| \"sumaPotenciasDeDosMasUno (Suc n) = \n      sumaPotenciasDeDosMasUno n + 2^(n+1)\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 2.2. Escribir la demostraci\u00f3n detallada de \n     sumaPotenciasDeDosMasUno n = 2^(n+1)\n  -------------------------------------------------------------------\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma \"sumaPotenciasDeDosMasUno n = 2^(n+1)\"\n  by (induct n) simp_all\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma \"sumaPotenciasDeDosMasUno n = 2^(n+1)\"\nproof (induct n) \n  show \"sumaPotenciasDeDosMasUno 0 = 2^(0+1)\" by simp\nnext\n  fix n\n  assume HI: \"sumaPotenciasDeDosMasUno n = 2^(n+1)\"\n  have \"sumaPotenciasDeDosMasUno (Suc n) = \n        sumaPotenciasDeDosMasUno n + 2^(n+1)\" by simp\n  also have \"... = 2^(n+1) + 2^(n+1)\" using HI by simp\n  also have \"... = 2 ^ (Suc n + 1)\" by simp\n  finally show \"sumaPotenciasDeDosMasUno (Suc n) = 2 ^ (Suc n + 1)\"\n    by simp\nqed\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma \"sumaPotenciasDeDosMasUno n = 2^(n+1)\"\nproof (induct n)\n  have \"sumaPotenciasDeDosMasUno 0 = 2\"\n    by (simp only: sumaPotenciasDeDosMasUno.simps(1))\n  also have \"... = 2^1\"\n    by (simp only: monoid_mult_class.power_one_right)\n  also have \"... = 2^(0+1)\"\n    by (simp only: add_0)\n  finally show \"sumaPotenciasDeDosMasUno 0 = 2^(0+1)\"\n    by this\nnext\n  fix n\n  assume HI: \"sumaPotenciasDeDosMasUno n = 2^(n+1)\"\n  have \"sumaPotenciasDeDosMasUno (Suc n) =  \n        sumaPotenciasDeDosMasUno n + 2^(n+1)\"\n    by (simp only: sumaPotenciasDeDosMasUno.simps(2))\n  also have \"... = 2^(n+1)+2^(n+1)\"\n    by (simp only: HI)\n  also have \"... = 2^(n+1)*2\"\n    by (simp only: mult_2_right)\n  also have \"... = 2^(Suc(n+1))\"\n    by (simp only: power_Suc2)\n  also have \"... = 2^((Suc n)+1)\"\n    by (simp only: Suc_eq_plus1)\n  finally show \"sumaPotenciasDeDosMasUno (Suc n) = 2^((Suc n)+1)\"\n    by this\nqed\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 3.1. Definir la funci\u00f3n\n     copia :: nat \u21d2 'a \u21d2 'a list\n  tal que (copia n x) es la lista formado por n copias del elemento\n  x. Por ejemplo, \n     copia 3 x = [x,x,x]\n  ------------------------------------------------------------------\u203a\n\nfun copia :: \"nat \u21d2 'a \u21d2 'a list\" where\n  \"copia 0 x       = []\"\n| \"copia (Suc n) x = x # copia n x\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 3.2. Definir la funci\u00f3n\n     todos :: ('a \u21d2 bool) \u21d2 'a list \u21d2 bool\n  tal que (todos p xs) se verifica si todos los elementos de xs cumplen\n  la propiedad p. Por ejemplo,\n     todos (\u03bbx. x>(1::nat)) [2,6,4] = True\n     todos (\u03bbx. x>(2::nat)) [2,6,4] = False\n  ------------------------------------------------------------------\u203a\n\nfun todos :: \"('a \u21d2 bool) \u21d2 'a list \u21d2 bool\" where\n  \"todos p []     = True\"\n| \"todos p (x#xs) = (p x \u2227 todos p xs)\"\n\nvalue \"todos (\u03bbx. x>(1::nat)) [2,6,4] = True\"\nvalue \"todos (\u03bbx. x>(2::nat)) [2,6,4] = False\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 3.2. Demostrar detalladamente que todos los elementos de\n  (copia n x) son iguales a x. \n  -------------------------------------------------------------------\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma \"todos (\u03bby. y=x) (copia n x)\"\n  by (induct n) simp_all\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma \"todos (\u03bby. y=x) (copia n x)\"\nproof (induct n)\n  show \"todos (\u03bby. y=x) (copia 0 x)\"\n    by simp\nnext\n  fix n\n  assume \"todos (\u03bby. y = x) (copia n x)\"\n  then show \"todos (\u03bby. y = x) (copia (Suc n) x)\"\n    by simp\nqed\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma \"todos (\u03bby. y=x) (copia n x)\"\nproof (induct n)\n  have \"todos (\u03bby. y=x) []\"\n    by (simp only: todos.simps(1))\n  then show \"todos (\u03bby. y=x) (copia 0 x)\"\n    by (simp only: copia.simps(1))\nnext\n  fix n\n  assume HI: \"todos (\u03bby. y = x) (copia n x)\"\n  then have \"todos (\u03bby. y = x) (x # copia n x)\"\n    by (simp only: todos.simps(2))\n  then show \"todos (\u03bby. y = x) (copia (Suc n) x)\"\n    by (simp only: copia.simps(2))\nqed\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 4.1. Definir la funci\u00f3n\n    factR :: nat \u21d2 nat\n  tal que (factR n) es el factorial de n. Por ejemplo,\n    factR 4 = 24\n  ------------------------------------------------------------------\u203a\n\nfun factR :: \"nat \u21d2 nat\" where\n  \"factR 0       = 1\"\n| \"factR (Suc n) = Suc n * factR n\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 4.2. Se considera la siguiente definici\u00f3n iterativa de la\n  funci\u00f3n factorial \n     factI :: \"nat \u21d2 nat\" where\n     factI n = factI' n 1\n     \n     factI' :: nat \u21d2 nat \u21d2 nat\" where\n     factI' 0       x = x\n     factI' (Suc n) x = factI' n (Suc n)*x\n  Demostrar que, para todo n y todo x, se tiene \n     factI' n x = x * factR n\n  Indicaci\u00f3n: La propiedad mult_Suc es \n     (Suc m) * n = n + m * n\n  Puede que se necesite desactivarla en un paso con \n     (simp del: mult_Suc)\n  -------------------------------------------------------------------\u203a\n\nfun factI' :: \"nat \u21d2 nat \u21d2 nat\" where\n  \"factI' 0       x = x\"\n| \"factI' (Suc n) x = factI' n (x * Suc n)\"\n\nfun factI :: \"nat \u21d2 nat\" where\n  \"factI n = factI' n 1\"\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a     \nlemma \"factI' n x = x * factR n\"\nby (induct n arbitrary: x) \n   (auto simp del: mult_Suc)\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a     \nlemma \"factI' n x = x * factR n\"\nproof (induct n arbitrary: x)\n  show \"\u22c0x. factI' 0 x = x * factR 0\" by simp\nnext\n  fix n\n  assume HI: \"\u22c0x. factI' n x = x * factR n\"\n  show \"\u22c0x. factI' (Suc n) x = x * factR (Suc n)\"\n  proof -\n    fix x\n    have \"factI' (Suc n) x = factI' n (x * Suc n)\" by simp\n    also have \"... = (x * Suc n) * factR n\" using HI by simp\n    also have \"... = x * (Suc n * factR n)\" by (simp del: mult_Suc)\n    also have \"... = x * factR (Suc n)\" by simp\n    finally show \"factI' (Suc n) x = x * factR (Suc n)\" by simp\n  qed\nqed\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a     \nlemma fact: \"factI' n x = x * factR n\"\nproof (induct n arbitrary: x)\nfix x\n  have \"factI' 0 x = x\"\n    by (simp only: factI'.simps(1))\n  also have \"... = x * 1\"\n    by (simp only: mult_1_right)\n  also have \"... = x * factR 0\"\n    by (simp only: factR.simps(1))\n  finally show \"factI' 0 x= x* factR 0\"\n    by this\nnext\n  fix n \n  assume HI: \" \u22c0x. factI' n x = x *factR n\"\n  show \"\u22c0x. factI' (Suc n) x = x*factR (Suc n)\"\n  proof -\n    fix x\n    have \"factI' (Suc n) x = factI' n (x*Suc n)\"\n      by (simp only: factI'.simps(2))\n    also have \"... = (x*Suc n)*factR n\"\n      by (simp only: HI)\n    also have \"... = x*(Suc n*factR n)\"\n      by (simp only: mult.assoc)\n    also have \"... = x*factR (Suc n)\"\n      by (simp only: factR.simps(2))\n    finally show \"factI' (Suc n) x= x*factR (Suc n)\"\n      by this\n  qed\nqed\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 4.3. Escribir la demostraci\u00f3n detallada de\n     factI n = factR n\n  -------------------------------------------------------------------\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\ncorollary \"factI n = factR n\"\n  by (simp add: fact)\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\ncorollary \"factI n = factR n\"\nproof -\n  have \"factI n = factI' n 1\"\n    by simp\n  also have \"\u2026 = 1 * factR n\"\n    by (simp add: fact)\n  also have \"\u2026 = factR n\"\n    by simp \n  finally show \"factI n = factR n\"\n    by this\nqed\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\ncorollary \"factI n = factR n\"\nproof -\n  have \"factI n = factI' n 1\"\n    by (simp only: factI.simps)\n  also have \"\u2026 = 1 * factR n\"\n    by (simp only: fact)\n  also have \"\u2026 = factR n\"\n    by (simp only: nat_mult_1)\n  finally show \"factI n = factR n\"\n    by this\nqed\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 5.1. Definir, recursivamente y sin usar (@), la funci\u00f3n\n     amplia :: 'a list \u21d2 'a \u21d2 'a list\n  tal que (amplia xs y) es la lista obtenida a\u00f1adiendo el elemento y al\n  final de la lista xs. Por ejemplo,\n     amplia [d,a] t = [d,a,t]\n  ------------------------------------------------------------------\u203a\n\nfun amplia :: \"'a list \u21d2 'a \u21d2 'a list\" where\n  \"amplia []     y = [y]\"\n| \"amplia (x#xs) y = x # amplia xs y\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 5.2. Escribir la demostraci\u00f3n detallada de\n     amplia xs y = xs @ [y]\n  -------------------------------------------------------------------\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma \"amplia xs y = xs @ [y]\"\n  by (induct xs) simp_all\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma \"amplia xs y = xs @ [y]\"\nproof (induct xs)\n  show \"amplia [] y = [] @ [y]\" by simp\nnext\n  fix x xs\n  assume HI: \"amplia xs y = xs @ [y]\"\n  have \"amplia (x # xs) y = x # amplia xs y\" by simp\n  also have \"... = x # (xs @ [y])\" using HI by simp\n  also have \"... = (x # xs) @ [y]\" by simp\n  finally show \"amplia (x # xs) y = (x # xs) @ [y]\" by simp\nqed\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma \"amplia xs y = xs @ [y]\"\n proof (induct xs)\n  have \"amplia [] y = [y]\"\n    by (simp only: amplia.simps(1))\n  also have \"... = [] @ [y]\"\n    by (simp only: append_Nil)\n  finally show \"amplia [] y = [] @ [y]\"\n    by this\nnext\n  fix x xs\n  assume HI: \"amplia xs y = xs @ [y]\"\n  have \"amplia (x#xs) y = x # amplia xs y\"\n    by (simp only: amplia.simps(2))\n  also have \"... = x # (xs @ [y])\"\n    by (simp only: HI)\n  also have \"... = (x # xs) @ [y]\"\n    by (simp only: append_Cons)\n  finally show \"amplia (x#xs) y = (x # xs) @ [y]\"\n    by this\nqed\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la segunda parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se han comentado las soluciones de la 3\u00aa relaci\u00f3n de ejercicios de razonamiento estructurado sobre programas. Para cada propiedad se dan tres demostraciones en Isabelle\/HOL: la primera autom\u00e1tica, la segunda estructurada y la tercera totalmente detallada mostrando todos los lemas de&#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":[333],"tags":[],"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\/6881"}],"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=6881"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6881\/revisions"}],"predecessor-version":[{"id":6883,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6881\/revisions\/6883"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6881"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6881"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6881"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}