{"id":3890,"date":"2013-12-05T19:51:38","date_gmt":"2013-12-05T18:51:38","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3890"},"modified":"2013-12-06T07:53:03","modified_gmt":"2013-12-06T06:53:03","slug":"ra2013-razonamiento-por-casos-y-por-induccion-1","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2013-razonamiento-por-casos-y-por-induccion-1\/","title":{"rendered":"RA2013: Razonamiento por casos y por inducci\u00f3n (1)"},"content":{"rendered":"<p>La clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-13\">Razonamiento autom\u00e1tico<\/a> ha tenido dos partes: comentar las soluciones de los ejercicios de la relaci\u00f3n 4 y empezar el estudio del tema 4. <\/p>\n<p>En la relaci\u00f3n 4 se define la funci\u00f3n cons que a\u00f1ade un elemento al final de la lista y se demuestra algunas de sus propiedades. Lo interesante es el uso de algunas propiedades en la demostraci\u00f3n de otras (como en el ejercicio 5). Las ejercicios y sus soluciones son<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\nheader {* R4: Cons inverso *}\r\n\r\ntheory R4\r\nimports Main \r\nbegin\r\n\r\ntext {*\r\n  --------------------------------------------------------------------- \r\n  Ejercicio 1. Definir recursivamente la funci\u00f3n \r\n     snoc :: \"'a list \u21d2 'a \u21d2 'a list\"\r\n  tal que (snoc xs a) es la lista obtenida al a\u00f1adir el elemento a al\r\n  final de la lista xs. Por ejemplo, \r\n     value \"snoc [2,5] (3::int)\" == [2,5,3]\r\n\r\n  Nota: No usar @.\r\n  --------------------------------------------------------------------- \r\n*}\r\n\r\nfun snoc :: \"'a list \u21d2 'a \u21d2 'a list\" where\r\n  \"snoc [] a = [a]\"\r\n| \"snoc (x#xs) a = x # (snoc xs a)\"\r\n\r\ntext {*\r\n  --------------------------------------------------------------------- \r\n  Ejercicio 2. Demostrar autom\u00e1ticamente el siguiente teorema \r\n     snoc xs a = xs @ [a]\r\n  --------------------------------------------------------------------- \r\n*}\r\n\r\nlemma \"snoc xs a = xs @ [a]\"\r\nby (induct xs) auto\r\n\r\ntext {*\r\n  --------------------------------------------------------------------- \r\n  Ejercicio 3. Demostrar detalladamente el siguiente teorema \r\n     snoc xs a = xs @ [a]\r\n  --------------------------------------------------------------------- \r\n*}\r\n\r\nlemma snoc_append: \"snoc xs a = xs @ [a]\"\r\nproof (induct \"xs\") \r\n  show \"snoc [] a = [] @ [a]\"\r\n  proof -\r\n    have \"snoc [] a = [a]\" by simp\r\n    also have \"\u2026 = [] @ [a]\" by simp\r\n    finally show \"snoc [] a = [] @ [a]\" .\r\n  qed\r\nnext\r\n  fix b xs assume HI: \"snoc xs a = xs @ [a]\"\r\n  show \"snoc (b # xs) a = (b # xs) @ [a]\"\r\n  proof -\r\n    have \"snoc (b # xs) a = b # (snoc xs a)\" by simp\r\n    also have \"\u2026 = b # (xs @ [a])\" using HI by simp\r\n    also have \"\u2026 = (b # xs) @ [a]\" by simp\r\n    finally show \"snoc (b # xs) a = (b # xs) @ [a]\" .\r\n  qed\r\nqed\r\n\r\ntext {*\r\n  --------------------------------------------------------------------- \r\n  Ejercicio 4. Demostrar autom\u00e1ticamente el siguiente lema\r\n     rev (x # xs) = snoc (rev xs) x\"\r\n  --------------------------------------------------------------------- \r\n*}\r\n\r\nlemma \"rev (x # xs) = snoc (rev xs) x\"\r\nby (auto simp add: snoc_append)\r\n\r\ntext {*\r\n  --------------------------------------------------------------------- \r\n  Ejercicio 5. Demostrar detalladamente el siguiente lema\r\n     rev (x # xs) = snoc (rev xs) x\"\r\n  --------------------------------------------------------------------- \r\n*}\r\n\r\ntheorem \"rev (x # xs) = snoc (rev xs) x\"\r\nproof -\r\n  have \"rev (x # xs) = (rev xs) @ [x]\" by simp\r\n  also have \"\u2026 = snoc (rev xs) x\" by (simp add:snoc_append)\r\n  finally show \"rev (x # xs) = snoc (rev xs) x\" .\r\nqed\r\n\r\nend\r\n<\/pre>\n<p>En la segunda parte hememos profundizado en el estudio de las demostraciones por casos y por inducci\u00f3n. En concreto, se ha estudiado<\/p>\n<ul>\n<li>el razonamiento por casos booleanos,\n<li>el razonamiento por casos booleanos sobre una variable,\n<li>el razonamiento por casos sobre listas,\n<li>el razonamiento por inducci\u00f3n sobre n\u00fameros naturales con patrones,\n<li>el razonamiento sobre definiciones con existenciales,\n<li>el uso de librer\u00edas auxiliares (como Parity) y\n<li>el uso de otros m\u00e9todos de domtraci\u00f3n (como presburg).\n<\/ul>\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 4: Razonamiento por casos y por inducci\u00f3n *}\r\n\r\ntheory T4_Razonamiento_por_casos_y_por_induccion\r\nimports Main Parity\r\nbegin\r\n\r\ntext {*\r\n  En este tema se ampl\u00edan los m\u00e9todos de demostraci\u00f3n por casos y por\r\n  inducci\u00f3n iniciados en el tema anterior.\r\n*}\r\n\r\nsection {* Razonamiento por distinci\u00f3n de casos *}\r\n\r\nsubsection {* Distinci\u00f3n de casos booleanos *}\r\n\r\ntext {*\r\n  Ejemplo de demostraci\u00f3n por distinci\u00f3n de casos booleanos:\r\n  Demostrar \"\u00acA \u2228 A\".\r\n*}\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma \"\u00acA \u2228 A\" \r\nproof cases\r\n  assume \"A\" \r\n  then show \"\u00acA \u2228 A\" ..\r\nnext\r\n  assume \"\u00acA\" \r\n  then show \"\u00acA \u2228 A\" ..\r\nqed\r\n\r\ntext {*\r\n  Comentarios de la demostraci\u00f3n anterior:\r\n  \u00b7 \"proof cases\" indica que el m\u00e9todo de demostraci\u00f3n ser\u00e1 por distinci\u00f3n de \r\n    casos. \r\n  \u00b7 Se generan 2 casos:\r\n       1. ?P \u27f9 \u00acA \u2228 A\r\n       2. \u00ac?P \u27f9 \u00acA \u2228 A\r\n    donde ?P es una variable sobre las f\u00f3rmulas.\r\n  \u00b7 (assume \"A\") indica que se est\u00e1 usando \"A\" en lugar de la variable\r\n    ?P.\r\n  \u00b7 \"then\" indica usando la f\u00f3rmula anterior.\r\n  \u00b7 \"..\" indica usando la regla l\u00f3gica necesaria (las reglas l\u00f3gicas se\r\n    estudiar\u00e1n en los siguientes temas).\r\n  \u00b7 \"next\" indica el siguiente caso (se puede observar c\u00f3mo ha\r\n    sustituido \u00ac?P por \u00acA.\r\n*}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"\u00acA \u2228 A\" \r\nby auto\r\n\r\ntext {*\r\n  Ejemplo de demostraci\u00f3n por distinci\u00f3n de casos booleanos con nombres: \r\n  Demostrar \"\u00acA \u2228 A\".\r\n*}\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma \"\u00acA \u2228 A\" \r\nproof (cases \"A\")\r\n  case True \r\n  then show \"\u00acA \u2228 A\" ..\r\nnext\r\n  case False \r\n  thus \"\u00acA \u2228 A\" .. \r\nqed\r\n\r\ntext {*\r\n  Comentarios sobre la demostraci\u00f3n anterior:\r\n  \u00b7 (cases \"A\") indica que la demostraci\u00f3n se har\u00e1 por casos seg\u00fan los\r\n    distintos valores de \"A\".\r\n  \u00b7 Como \"A\" es una f\u00f3rmula, sus posibles valores son verdadero o falso.\r\n  \u00b7 \"case True\" indica que se est\u00e1 suponiendo que A es verdadera. Es\r\n    equivalente a \"assume A\".\r\n  \u00b7 \"case False\" indica que se est\u00e1 suponiendo que A es falsa. Es\r\n    equivalente a \"assume \u00acA\".\r\n  \u00b7 En general, \r\n    \u00b7 el m\u00e9todo (cases F) es una abreviatura de la aplicaci\u00f3n de la regla\r\n         \u27e6F \u27f9 Q; \u00acF \u27f9 Q\u27e7 \u27f9 Q  \r\n    \u00b7 La expresi\u00f3n \"case True\" es una abreviatura de F.\r\n    \u00b7 La expresi\u00f3n \"case False\" es una abreviatura de \u00acF.\r\n  \u00b7 Ventajas de \"cases\" con nombre: \r\n    \u00b7 reduce la escritura de la f\u00f3rmula y\r\n    \u00b7 es independiente del orden de los casos.\r\n*}\r\n\r\nsubsection {* Distinci\u00f3n de casos sobre otros tipos de datos *}\r\n\r\ntext {*\r\n  Ejemplo de distinci\u00f3n de casos sobre listas: \r\n  Demostrar que la longitud del resto de una lista es la longitud de la\r\n  lista menos 1. \r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma \"length (tl xs) = length xs - 1\" \r\nproof (cases xs)\r\n  assume \"xs = []\"\r\n  then show \"length (tl xs) = length xs - 1\" by simp\r\nnext\r\n  fix y ys\r\n  assume \"xs = y#ys\"\r\n  then show \"length(tl xs) = length xs - 1\" by simp \r\nqed\r\n\r\ntext {*\r\n  Comentarios sobre la demostraci\u00f3n anterior:\r\n  \u00b7 \"(cases xs)\" indica que la demostraci\u00f3n se har\u00e1 por casos sobre los\r\n    posibles valores de xs.\r\n  \u00b7 Como xs es una lista, sus posibles valores son la lista vac\u00eda ([]) o\r\n    una lista no vac\u00eda (de la forma (y#ys)).\r\n  \u00b7 Se generan 2 casos:\r\n       1. xs = [] \u27f9 length (tl xs) = length xs - 1\r\n       2. \u22c0a list. xs = a # list \u27f9 length (tl xs) = length xs - 1\r\n*}\r\n\r\n-- \"La demostraci\u00f3n simplificada es\"\r\nlemma \"length (tl xs) = length xs - 1\" \r\nproof (cases xs)\r\n  case Nil \r\n  then show ?thesis by simp\r\nnext\r\n  case Cons \r\n  then show ?thesis by simp \r\nqed\r\n\r\ntext {*\r\n  Comentarios sobre la dmostraci\u00f3n anterior:\r\n  \u00b7 \"case Nil\" es una abreviatura de \r\n       \"assume xs =[]\".\r\n  \u00b7 \"case Cons\" es una abreviatura de \r\n       \"fix y ys assume xs = y#ys\"\r\n  \u00b7 ?thesis es una abreviatura de la conclusi\u00f3n del lema.\r\n*}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"length (tl xs) = length xs - 1\" \r\nby auto\r\n\r\ntext {*\r\n  Een el siguiente ejemplo vamos a demostrar una propiedad de la funci\u00f3n\r\n  drop que est\u00e1 definida en la teor\u00eda List de forma que (drop n xs) la\r\n  lista obtenida eliminando en xs} los n primeros elementos. Su\r\n  definici\u00f3n es la siguiente   \r\n     drop_Nil:  \"drop n []     = []\" \r\n     drop_Cons: \"drop n (x#xs) = (case n of \r\n                                    0 => x#xs | \r\n                                    Suc(m) => drop m xs)\"\r\n*}\r\n\r\ntext {*\r\n  Ejemplo de an\u00e1lisis de casos:\r\n  Demostrar que el resultado de eliminar los n+1 primeros elementos de\r\n  xs es el mismo que eliminar los n primeros elementos del resto de xs.  \r\n*}\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma \"drop (n + 1) xs = drop n (tl xs)\"\r\nproof (cases xs)\r\n  case Nil \r\n  then show ?thesis by simp\r\nnext\r\n  case Cons \r\n  then show ?thesis by simp\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"drop (n + 1) xs = drop n (tl xs)\"\r\nby (cases xs) auto\r\n\r\nsection {* Inducci\u00f3n matem\u00e1tica *}\r\n\r\ntext {*\r\n  [Principio de inducci\u00f3n matem\u00e1tica]\r\n  Para demostrar una propiedad P para todos los n\u00fameros naturales basta\r\n  probar que el 0 tiene la propiedad P y que si n tiene la propiedad P,\r\n  entonces n+1 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 matem\u00e1tica est\u00e1 formalizado en\r\n  el teorema nat.induct y puede verse con\r\n     thm nat.induct\r\n*}\r\n\r\ntext {*  \r\n  Ejemplo de demostraci\u00f3n por inducci\u00f3n: Usaremos el principio de\r\n  inducci\u00f3n matem\u00e1tica para demostrar que \r\n     1 + 3 + ... + (2n-1) = n^2\r\n\r\n  Definici\u00f3n. [Suma de los primeros impares] \r\n  (suma_impares n) la suma de los n n\u00fameros impares. Por ejemplo,\r\n     suma_impares 3  =  9\r\n*}\r\n\r\nfun suma_impares :: \"nat \u21d2 nat\" where\r\n  \"suma_impares 0 = 0\" \r\n| \"suma_impares (Suc n) = (2*(Suc n) - 1) + suma_impares n\"\r\n\r\nvalue \"suma_impares 3\"\r\n\r\ntext {*\r\n  Ejemplo de demostraci\u00f3n por inducci\u00f3n matem\u00e1tica:\r\n  Demostrar que la suma de los n primeros n\u00fameros impares es n^2.\r\n*}\r\n\r\n-- \"Demostraci\u00f3n del lema anterior por inducci\u00f3n y razonamiento ecuacional\"\r\nlemma \"suma_impares n = n * n\"\r\nproof (induct n)\r\n  show \"suma_impares 0 = 0 * 0\" by simp\r\nnext\r\n  fix n assume HI: \"suma_impares n = n * n\"\r\n  have \"suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n\" by simp\r\n  also have \"\u2026 = (2 * (Suc n) - 1) + n * n\" using HI by simp\r\n  also have \"\u2026 = n * n + 2 * n + 1\" by simp\r\n  finally show \"suma_impares (Suc n) = (Suc n) * (Suc n)\" by simp\r\nqed\r\n\r\n-- \"Demostraci\u00f3n del lema anterior con patrones y razonamiento ecuacional\"\r\nlemma \"suma_impares n = n * n\" (is \"?P n\")\r\nproof (induct n)\r\n  show \"?P 0\" by simp\r\nnext\r\n  fix n \r\n  assume HI: \"?P n\"\r\n  have \"suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n\" by simp\r\n  also have \"\u2026 = (2 * (Suc n) - 1) + n * n\" using HI by simp\r\n  also have \"\u2026 = n * n + 2 * n + 1\" by simp\r\n  finally show \"?P (Suc n)\" by simp\r\nqed\r\n\r\ntext {*\r\n  Comentario sobre la demostraci\u00f3n anterior:\r\n  \u00b7 Con la expresi\u00f3n\r\n       \"suma_impares n = n * n\" (is \"?P n\")\r\n    se abrevia \"suma_impares n = n * n\" como \"?P n\". Por tanto, \r\n       \"?P 0\"       es una abreviatura de \"suma_impares 0 = 0 * 0\"\r\n       \"?P (Suc n)\" es una abreviatura de \"suma_impares (Suc n) = (Suc n) * (Suc n)\"\r\n  \u00b7 En general, cualquier f\u00f3rmula seguida de (is patr\u00f3n) equipara el\r\n    patr\u00f3n con la f\u00f3rmula. \r\n*}\r\n\r\n-- \"La demostraci\u00f3n usando patrones es\"\r\nlemma \"suma_impares n = n * n\" (is \"?P n\")\r\nproof (induct n)\r\n  show \"?P 0\" by simp\r\nnext\r\n  fix n \r\n  assume \"?P n\"\r\n  then show \"?P (Suc n)\" by simp\r\nqed\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma \"suma_impares n = n * n\"\r\nby (induct n) auto\r\n\r\n\r\ntext {* \r\n  Ejemplo de definici\u00f3n con existenciales. \r\n  Un n\u00famero natural n es par si existe un natural m tal que n=m+m.   \r\n*}\r\n\r\ndefinition par :: \"nat \u21d2 bool\" where\r\n  \"par n \u2261 \u2203m. n=m+m\"\r\n\r\ntext {* \r\n  Ejemplo de inducci\u00f3n y existenciales: \r\n  Demostrar que para todo n\u00famero natural n, se verifica que n*(n+1) par. \r\n*}\r\n\r\n-- \"Demostraci\u00f3n detallada por inducci\u00f3n\"\r\nlemma \r\n  fixes n :: \"nat\"\r\n  shows \"par (n*(n+1))\"\r\nproof (induct n)\r\n  show \"par (0*(0+1))\" by (simp add: par_def)\r\nnext\r\n  fix n \r\n  assume \"par (n*(n+1))\"\r\n  then have \"\u2203m. n*(n+1) = m+m\" by (simp add:par_def)\r\n  then obtain m where m: \"n*(n+1) = m+m\" ..\r\n  then have \"(Suc n)*((Suc n)+1) = (m+n+1)+(m+n+1)\" by auto\r\n  then have \"\u2203m. (Suc n)*((Suc n)+1) = m+m\" ..\r\n  then show \"par ((Suc n)*((Suc n)+1))\" by (simp add:par_def)\r\nqed\r\n\r\ntext {*\r\n  Comentarios sobre la demostraci\u00f3n anterior:\r\n  \u00b7 (fixes n :: \"nat\") es una abreviatura de \"sea n un n\u00famero natural\".\r\n*}\r\n\r\ntext {*\r\n  En Isabelle puede demostrarse de manera m\u00e1s simple un lema equivalente\r\n  usando en lugar de la funci\u00f3n \"par\" la funci\u00f3n \"even\" definida en la\r\n  teor\u00eda Parity por\r\n     even x \u27f7 x mod 2 = 0\"\r\n*}\r\n\r\nlemma \r\n  fixes n :: \"nat\"\r\n  shows \"even (n*(n+1))\"\r\nby auto\r\n\r\ntext {*\r\n  Comentarios sobre la demostraci\u00f3n anterior:\r\n  \u00b7 Para poder usar la funci\u00f3n \"even\" de la librer\u00eda Parity es necesario\r\n    importar dicha librer\u00eda. Por ello, anter del inicio de la teor\u00eda aparece\r\n       imports Main Parity\r\n*}\r\n\r\ntext {*\r\n  Para completar la demostraci\u00f3n basta demostrar la equivalencia de las\r\n  funciones \"par\" y \"even\". \r\n*}\r\n\r\nlemma \r\n  fixes n :: \"nat\"\r\n  shows \"par n = even n\"\r\nproof - \r\n  have \"par n = (\u2203m. n = m+m)\" by (simp add:par_def)\r\n  then show \"par n = even n\" by presburger\r\nqed\r\n\r\ntext {*\r\n  Comentarios sobre la demostraci\u00f3n anterior:\r\n  \u00b7 \"by presburger\" indica que se use como m\u00e9todo de demostraci\u00f3n el\r\n    algoritmo de decisi\u00f3n de la aritm\u00e9tica de Presburger.\r\n*}\r\n\r\nend\r\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\/R5\">relaci\u00f3n 5<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>La clase de hoy del curso de Razonamiento autom\u00e1tico ha tenido dos partes: comentar las soluciones de los ejercicios de la relaci\u00f3n 4 y empezar el estudio del tema 4. En la relaci\u00f3n 4 se define la funci\u00f3n cons que a\u00f1ade un elemento al final de la lista y se demuestra algunas de sus propiedades&#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\/3890"}],"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=3890"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3890\/revisions"}],"predecessor-version":[{"id":3891,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3890\/revisions\/3891"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3890"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3890"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3890"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}