{"id":5649,"date":"2016-12-01T20:21:29","date_gmt":"2016-12-01T19:21:29","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5649"},"modified":"2016-12-06T10:22:25","modified_gmt":"2016-12-06T09:22:25","slug":"ra2016-ejercicios-de-eliminacion-de-duplicados-en-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2016-ejercicios-de-eliminacion-de-duplicados-en-isabellehol\/","title":{"rendered":"RA2016: Ejercicios de eliminaci\u00f3n de duplicados 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-16\">Razonamiento autom\u00e1tico<\/a> se han comentado las soluciones de la 5\u00aa relaci\u00f3n de ejercicios sobre eliminaci\u00f3n de elementos duplicados de listas en Isabelle\/HOL.<\/p>\n<p>La teor\u00eda con las soluciones de los ejercicios es la siguiente<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter {* R5: Eliminaci\u00f3n de duplicados *}\n\ntheory R5\nimports Main \nbegin\n        \ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 1. Definir la funcion primitiva recursiva \n     estaEn :: 'a \u21d2 'a list \u21d2 bool\n  tal que (estaEn x xs) se verifica si el elemento x est\u00e1 en la lista\n  xs. Por ejemplo, \n     estaEn (2::nat) [3,2,4] = True\n     estaEn (1::nat) [3,2,4] = False\n  --------------------------------------------------------------------- \n*}\n\nfun estaEn :: \"'a \u21d2 'a list \u21d2 bool\" where\n  \"estaEn x []     = False\"\n| \"estaEn x (a#xs) = (x=a \u2228 estaEn x xs)\"  \n\nvalue \"estaEn (2::nat) [3,2,4] = True\"\nvalue \"estaEn (1::nat) [3,2,4] = False\"\n\ntext {* \n  --------------------------------------------------------------------- \n  Ejercicio 2. Definir la funci\u00f3n primitiva recursiva \n     sinDuplicados :: 'a list \u21d2 bool\n  tal que (sinDuplicados xs) se verifica si la lista xs no contiene\n  duplicados. Por ejemplo,  \n     sinDuplicados [1::nat,4,2]   = True\n     sinDuplicados [1::nat,4,2,4] = False\n  --------------------------------------------------------------------- \n*}\n\nfun sinDuplicados :: \"'a list \u21d2 bool\" where\n  \"sinDuplicados [] = True\"\n| \"sinDuplicados (a#xs) = ((\u00ac estaEn a xs) \u2227 sinDuplicados xs)\"\n\nvalue \"sinDuplicados [1::nat,4,2]   = True\"\nvalue \"sinDuplicados [1::nat,4,2,4] = False\"\n\ntext {* \n  --------------------------------------------------------------------- \n  Ejercicio 3. Definir la funci\u00f3n primitiva recursiva \n     borraDuplicados :: 'a list \u21d2 bool\n  tal que (borraDuplicados xs) es la lista obtenida eliminando los\n  elementos duplicados de la lista xs. Por ejemplo, \n     borraDuplicados [1::nat,2,4,2,3] = [1,4,2,3]\n\n  Nota: La funci\u00f3n borraDuplicados es equivalente a la predefinida\n  remdups.  \n  --------------------------------------------------------------------- \n*}\n\nfun borraDuplicados :: \"'a list \u21d2 'a list\" where\n  \"borraDuplicados []     = []\"\n| \"borraDuplicados (a#xs) = (if estaEn a xs \n                             then borraDuplicados xs \n                             else (a#borraDuplicados xs))\"\n\nvalue \"borraDuplicados [1::nat,2,4,2,3] = [1,4,2,3]\"\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 4.1. Demostrar o refutar autom\u00e1ticamente\n     length (borraDuplicados xs) \u2264 length xs\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma length_borraDuplicados:\n  \"length (borraDuplicados xs) \u2264 length xs\"\nby (induct xs) simp_all\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 4.2. Demostrar o refutar detalladamente\n     length (borraDuplicados xs) \u2264 length xs\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma length_borraDuplicados_2: \n  \"length (borraDuplicados xs) \u2264 length xs\"\nproof (induct xs)\n  show \"length (borraDuplicados []) \u2264 length []\" by simp\nnext\n  fix a xs\n  assume HI: \"length (borraDuplicados xs) \u2264 length xs\"\n  thus \"length (borraDuplicados (a#xs)) \u2264 length (a#xs)\"\n  proof (cases)\n    assume \"estaEn a xs\"\n    thus \"length (borraDuplicados (a#xs)) \u2264 length (a#xs)\" \n      using HI by auto\n  next\n    assume \"(\u00ac estaEn a xs)\"\n    thus \"length (borraDuplicados (a#xs)) \u2264 length (a#xs)\" \n      using HI by auto\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma length_borraDuplicados_3: \n  \"length (borraDuplicados xs) \u2264 length xs\"\nproof (induct xs)\n  show \"length (borraDuplicados []) \u2264 length []\" by simp\nnext\n  fix a xs\n  assume HI: \"length (borraDuplicados xs) \u2264 length xs\"\n  show \"length (borraDuplicados (a#xs)) \u2264 length (a#xs)\"\n  proof (cases)\n    assume \"estaEn a xs\"\n    hence \"length (borraDuplicados (a#xs)) = length (borraDuplicados xs)\" \n      by simp\n    also have \"\u2026 \u2264 length xs\" using HI by simp\n    also have \"\u2026 \u2264 length (a#xs)\" by simp\n    finally show ?thesis .\n  next\n    assume \"(\u00ac estaEn a xs)\"\n    hence \"length (borraDuplicados (a#xs)) = length (a#(borraDuplicados xs))\"\n      by simp\n    also have \"\u2026 = 1 + length (borraDuplicados xs)\" by simp\n    also have \"\u2026 \u2264 1 + length xs\" using HI by simp\n    also have \"\u2026 = length (a#xs)\" by simp\n    finally show ?thesis .\n  qed\nqed\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 5.1. Demostrar o refutar autom\u00e1ticamente\n     estaEn a (borraDuplicados xs) = estaEn a xs\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma estaEn_borraDuplicados: \n  \"estaEn a (borraDuplicados xs) = estaEn a xs\"\nby (induct xs) auto\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 5.2. Demostrar o refutar detalladamente\n     estaEn a (borraDuplicados xs) = estaEn a xs\n  Nota: Para la demostraci\u00f3n de la equivalencia se puede usar\n     proof (rule iffI)\n  La regla iffI es\n     \u27e6P \u27f9 Q ; Q \u27f9 P\u27e7 \u27f9 P = Q\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma estaEn_borraDuplicados_2: \n  \"estaEn a (borraDuplicados xs) = estaEn a xs\"\nproof (induct xs)\n  show \"estaEn a (borraDuplicados []) = estaEn a []\" by simp\nnext\n  fix b xs\n  assume HI: \"estaEn a (borraDuplicados xs) = estaEn a xs\"\n  show \"estaEn a (borraDuplicados (b#xs)) = estaEn a (b#xs)\"\n  proof (rule iffI)\n    assume c1: \"estaEn a (borraDuplicados (b#xs))\"\n    show \"estaEn a (b#xs)\"\n    proof (cases)\n      assume \"estaEn b xs\"\n      thus \"estaEn a (b#xs)\" using c1 HI by auto\n    next\n      assume \"\u00ac estaEn b xs\"\n      thus \"estaEn a (b#xs)\" using c1 HI by auto\n    qed\n  next\n    assume c2: \"estaEn a (b#xs)\"\n    show \"estaEn a (borraDuplicados (b#xs))\"\n    proof (cases)\n      assume \"a=b\"\n      thus \"estaEn a (borraDuplicados (b#xs))\" using HI by auto\n    next\n      assume \"a\u2260b\"\n      thus \"estaEn a (borraDuplicados (b#xs))\" using `a\u2260b` c2 HI by auto\n    qed\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma estaEn_borraDuplicados_3: \n  \"estaEn a (borraDuplicados xs) = estaEn a xs\"\nproof (induct xs)\n  show \"estaEn a (borraDuplicados []) = estaEn a []\" by simp\nnext\n  fix b xs\n  assume HI: \"estaEn a (borraDuplicados xs) = estaEn a xs\"\n  show \"estaEn a (borraDuplicados (b#xs)) = estaEn a (b#xs)\"\n  proof (rule iffI)\n    assume c1: \"estaEn a (borraDuplicados (b#xs))\"\n    show \"estaEn a (b#xs)\"\n    proof (cases)\n      assume \"estaEn b xs\"\n      hence \"estaEn a (borraDuplicados xs)\" using c1 by simp\n      hence \"estaEn a xs\" using HI by simp\n      thus \"estaEn a (b#xs)\" by simp\n    next\n      assume \"\u00ac estaEn b xs\"\n      hence \"estaEn a (b#(borraDuplicados xs))\" using c1 by simp\n      hence \"a=b \u2228 (estaEn a (borraDuplicados xs))\" by simp\n      hence \"a=b \u2228 (estaEn a xs)\" using HI by simp\n      thus \"estaEn a (b#xs)\" by simp\n    qed\n  next\n    assume c2: \"estaEn a (b#xs)\"\n    show \"estaEn a (borraDuplicados (b#xs))\"\n    proof (cases)\n      assume \"a=b\"\n      thus \"estaEn a (borraDuplicados (b#xs))\" using HI by auto\n    next\n      assume \"a\u2260b\"\n      hence \"estaEn a xs\" using c2 by simp\n      hence \"estaEn a (borraDuplicados xs)\" using HI by simp\n      thus \"estaEn a (borraDuplicados (b#xs))\" using `a\u2260b` by simp\n    qed\n  qed\nqed\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 6.1. Demostrar o refutar autom\u00e1ticamente\n     sinDuplicados (borraDuplicados xs)\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica\"\nlemma sinDuplicados_borraDuplicados:\n  \"sinDuplicados (borraDuplicados xs)\"\nby (induct xs) (auto simp add: estaEn_borraDuplicados)\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 6.2. Demostrar o refutar detalladamente\n     sinDuplicados (borraDuplicados xs)\n  --------------------------------------------------------------------- \n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma sinDuplicados_borraDuplicados_2:\n  \"sinDuplicados (borraDuplicados xs)\"\nproof (induct xs)\n  show \"sinDuplicados (borraDuplicados [])\" by simp\nnext\n  fix a xs\n  assume HI: \"sinDuplicados (borraDuplicados xs)\"\n  show \"sinDuplicados (borraDuplicados (a#xs))\"\n  proof (cases)\n    assume \"estaEn a xs\"\n    thus \"sinDuplicados (borraDuplicados (a#xs))\" using HI by simp\n  next\n    assume \"\u00ac estaEn a xs\"\n    thus \"sinDuplicados (borraDuplicados (a#xs))\" \n      using `\u00ac estaEn a xs` HI \n      by (auto simp add: estaEn_borraDuplicados)\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma sinDuplicados_borraDuplicados_3:\n  \"sinDuplicados (borraDuplicados xs)\"\nproof (induct xs)\n  show \"sinDuplicados (borraDuplicados [])\" by simp\nnext\n  fix a xs\n  assume HI: \"sinDuplicados (borraDuplicados xs)\"\n  show \"sinDuplicados (borraDuplicados (a#xs))\"\n  proof (cases)\n    assume \"estaEn a xs\"\n    thus \"sinDuplicados (borraDuplicados (a#xs))\" using HI by simp\n  next\n    assume \"\u00ac estaEn a xs\"\n    hence \"\u00ac (estaEn a xs) \u2227 sinDuplicados (borraDuplicados xs)\" \n      using HI by simp\n    hence \"\u00ac estaEn a (borraDuplicados xs) \u2227 \n           sinDuplicados (borraDuplicados xs)\" \n      by (simp add: estaEn_borraDuplicados)\n    hence \"sinDuplicados (a#borraDuplicados xs)\" by simp\n    thus \"sinDuplicados (borraDuplicados (a#xs))\" \n      using `\u00ac estaEn a xs` by simp\n  qed\nqed\n\ntext {*\n  --------------------------------------------------------------------- \n  Ejercicio 7. Demostrar o refutar:\n    borraDuplicados (rev xs) = rev (borraDuplicados xs)\n  --------------------------------------------------------------------- \n*}\n\n-- \"Se busca un contraejemplo con\"\nlemma \"borraDuplicados (rev xs) = rev (borraDuplicados xs)\"\nquickcheck\noops\n\ntext {*\n  El contraejemplo encontrado es\n     xs = [3, 2, 3]\n  En efecto,\n      borraDuplicados (rev xs) = borraDuplicados (rev [3,2,3]) = [2,3] \n      rev (borraDuplicados xs) = rev (borraDuplicados [3,2,3]) = [3,2] \n*}\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 5\u00aa relaci\u00f3n de ejercicios sobre eliminaci\u00f3n de elementos duplicados de listas en Isabelle\/HOL. La teor\u00eda con las soluciones de los ejercicios es la siguiente<\/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":[261],"tags":[144,314],"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\/5649"}],"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=5649"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5649\/revisions"}],"predecessor-version":[{"id":5650,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5649\/revisions\/5650"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5649"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5649"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5649"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}