{"id":7029,"date":"2020-02-13T18:02:21","date_gmt":"2020-02-13T17:02:21","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7029"},"modified":"2020-02-16T18:03:19","modified_gmt":"2020-02-16T17:03:19","slug":"ra2019-verificacion-de-la-ordenacion-por-insercion-con-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2019-verificacion-de-la-ordenacion-por-insercion-con-isabelle-hol\/","title":{"rendered":"RA2019: Verificaci\u00f3n de la ordenaci\u00f3n por inserci\u00f3n con Isabelle\/HOL"},"content":{"rendered":"<p>En 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 ha estudiado c\u00f3mo verificar con Isabelle\/HOL la correcci\u00f3n del algoritmo de  ordenaci\u00f3n por inserci\u00f3n.<\/p>\n<p>La correspondiente teor\u00eda Isabelle\/HOL se muestra a continuaci\u00f3n<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter \u2039T11: Verificaci\u00f3n de la ordenaci\u00f3n por inserci\u00f3n\u203a\n\ntheory T11_Verificacion_de_la_ordenacion_por_insercion\nimports Main\nbegin\n\ntext \u2039En este de tema se define el algoritmo de ordenaci\u00f3n de listas \n  por inserci\u00f3n y se demuestra que es correcto.\u203a\n\ntext \u2039----------------------------------------------------------------- \n  Ejercicio 1. Definir la funci\u00f3n\n     inserta :: int \u21d2 int list \u21d2 int list\n  tal que (inserta a xs) es la lista obtenida insertando a delante del\n  primer elemento de xs que es mayor o igual que a. Por ejemplo,\n     inserta 3 [2,5,1,7] = [2,3,5,1,7]\n  ------------------------------------------------------------------\u203a\n\nfun inserta :: \"int \u21d2 int list \u21d2 int list\" where\n  \"inserta a []     = [a]\"\n| \"inserta a (x#xs) = (if a \u2264 x \n                       then a # x # xs \n                       else x # inserta a xs)\"\n\nvalue \"inserta 3 [2,5,1,7] = [2,3,5,1,7]\"\n\ntext \u2039----------------------------------------------------------------- \n  Ejercicio 2. Definir la funci\u00f3n\n     ordena :: int list \u21d2 int list\n  tal que (ordena xs) es la lista obtenida ordenando xs por inserci\u00f3n. \n  Por ejemplo, \n     ordena [3,2,5,3] = [2,3,3,5]\n  ------------------------------------------------------------------\u203a\n\nfun ordena :: \"int list \u21d2 int list\" where\n  \"ordena []     = []\"\n| \"ordena (x#xs) = inserta x (ordena xs)\"\n\nvalue \"ordena [3,2,5,3] = [2,3,3,5]\"\n\ntext \u2039----------------------------------------------------------------- \n  Ejercicio 3. Definir la funci\u00f3n\n     menor :: int \u21d2 int list \u21d2 bool\n  tal que (menor a xs) se verifica si a es menor o igual que todos los\n  elementos de xs.Por ejemplo,  \n     menor 2 [3,2,5] = True\n     menor 2 [3,0,5] = False\n  ------------------------------------------------------------------\u203a\n\nfun menor :: \"int \u21d2 int list \u21d2 bool\" where\n  \"menor a []     = True\"\n| \"menor a (x#xs) = (a \u2264 x \u2227 menor a xs)\"\n\nvalue \"menor 2 [3,2,5] = True\"\nvalue \"menor 2 [3,0,5] = False\"\n\ntext \u2039----------------------------------------------------------------- \n  Ejercicio 4. Definir la funci\u00f3n\n     ordenada :: int list \u21d2 bool\n  tal que (ordenada xs) se verifica si xs es una lista ordenada de\n  manera creciente. Por ejemplo,  \n     ordenada [2,3,3,5] = True \n     ordenada [2,4,3,5] = False \n  ------------------------------------------------------------------\u203a\n\nfun ordenada :: \"int list \u21d2 bool\" where\n  \"ordenada []     = True\"\n| \"ordenada (x#xs) = (menor x xs \u2227 ordenada xs)\"\n\nvalue \"ordenada [2,3,3,5] = True\" \nvalue \"ordenada [2,4,3,5] = False\" \n\ntext \u2039----------------------------------------------------------------- \n  Ejercicio 5. Demostrar que si y es una cota inferior de zs y x \u2264 y,\n  entonces x es una cota inferior de zs.\n  ------------------------------------------------------------------\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma menor_menor: \n  assumes \"x \u2264 y\"  \n  shows   \"menor y zs \u27f6 menor x zs\"\n  using assms\n  by (induct zs) auto\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma menor_menor_2: \n  assumes \"x \u2264 y\"  \n  shows   \"menor y zs \u27f6 menor x zs\"\nproof (induct zs)\n  show \"menor y [] \u27f6 menor x []\"\n    by (simp only: menor.simps(1) \n                   simp_thms(17))\nnext\n  fix z zs\n  assume HI: \"menor y zs \u27f6 menor x zs\"  \n  show \"menor y (z # zs) \u27f6 menor x (z # zs)\"\n  proof (rule impI)\n    assume sup: \"menor y (z # zs)\"\n    show \"menor x (z # zs)\"\n    proof (simp only: menor.simps(2))\n      show \"x \u2264 z \u2227 menor x zs\"\n      proof (rule conjI)\n        have \"x \u2264 y\" \n          using assms \n          by this\n        also have \"y \u2264 z\" \n          using sup \n          by (simp only: menor.simps(2))\n        finally show \"x \u2264 z\" \n          by this\n      next\n        have \"menor y zs\" \n          using sup \n          by (simp only: menor.simps(2))\n        with HI show \"menor x zs\" \n          by (rule mp)\n      qed\n    qed\n  qed\nqed\n\ntext \u2039----------------------------------------------------------------- \n  Ejercicio 6. Demostrar el siguiente teorema de correcci\u00f3n: x es una\n  cota inferior de la lista obtenida insertando y en zs syss x \u2264 y y x\n  es una cota inferior de zs.\n  ------------------------------------------------------------------\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma menor_inserta:\n  \"menor x (inserta y zs) = (x \u2264 y \u2227 menor x zs)\"\n  by (induct zs) auto\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma menor_inserta_2: \n  \"menor x (inserta y zs) = (x \u2264 y \u2227 menor x zs)\"\nproof (induct zs)\n  show \"menor x (inserta y []) = (x \u2264 y \u2227 menor x [])\"\n    by (simp only: menor.simps(2)\n                   inserta.simps(1))\nnext \n  fix z zs\n  assume HI: \"menor x (inserta y zs) = (x \u2264 y \u2227 menor x zs)\"\n  show \"menor x (inserta y (z#zs)) = (x \u2264 y \u2227 menor x (z#zs))\" \n  proof (cases \"y \u2264 z\")\n    assume \"y \u2264 z\"\n    then have \"menor x (inserta y (z#zs)) = menor x (y#z#zs)\" \n      by (simp only: inserta.simps(2)\n                     if_True)\n    also have \"\u2026 = (x \u2264 y \u2227 menor x (z#zs))\" \n      by (simp only: menor.simps(2))\n    finally show ?thesis \n      by this\n  next\n    assume \"\u00ac(y \u2264 z)\"\n    then have \"menor x (inserta y (z#zs)) = \n               menor x (z # inserta y zs)\" \n      by (simp only: inserta.simps(2)\n                     if_False)\n    also have \"\u2026 = (x \u2264 z \u2227 menor x (inserta y zs))\" \n      by (simp only: menor.simps(2))\n    also have \"\u2026 = (x \u2264 z \u2227 (x \u2264 y \u2227 menor x zs))\" \n      by (simp only: HI)\n    also have \"\u2026 = ((x \u2264 z \u2227 x \u2264 y) \u2227 menor x zs)\"\n      by (simp only: conj_assoc)\n    also have \"\u2026 = ((x \u2264 y \u2227 x \u2264 z) \u2227 menor x zs)\"\n      by (simp only: conj_commute)\n    also have \"\u2026 = (x \u2264 y \u2227 (x \u2264 z \u2227 menor x zs))\"\n      by (simp only: conj_assoc)\n    also have \"\u2026 = (x \u2264 y \u2227 menor x (z#zs))\"\n      by (simp only: menor.simps(2))\n    finally show ?thesis \n      by this\n  qed\nqed\n\ntext \u2039----------------------------------------------------------------- \n  Ejercicio 6. Demostrar que al insertar un elemento la lista obtenida\n  est\u00e1 ordenada syss lo estaba la original.\n  ------------------------------------------------------------------\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma \n  \"ordenada (inserta a xs) = ordenada xs\"\n  by (induct xs) (auto simp add: menor_menor menor_inserta)\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma \n  \"ordenada (inserta a xs) = ordenada xs\"\nproof (induct xs)\n  case Nil\n  then show ?case try\n    by simp\nnext\n  case (Cons a xs)\n  then show ?case \n    using menor_inserta \n         menor_menor \n    by auto\nqed\n\nlemma ordenada_inserta:\n  \"ordenada (inserta a xs) = ordenada xs\"\nproof (induct xs)\n  show \"ordenada (inserta a []) = ordenada []\"\n  proof -\n    have \"ordenada (inserta a []) = ordenada [a]\"\n      by (simp only: inserta.simps(1))\n    also have \"\u2026 = (menor a [] \u2227 ordenada [])\"\n      by (simp only: ordenada.simps(2))\n    also have \"\u2026 = (True \u2227 ordenada [])\"\n      by (simp only: menor.simps(1))\n    also have \"\u2026 = ordenada []\"\n      by (simp only: simp_thms(22))\n    finally show ?thesis\n      by this\n  qed\nnext\n  fix x xs\n  assume HI: \"ordenada (inserta a xs) = ordenada xs\" \n  show \"ordenada (inserta a (x # xs)) = ordenada (x # xs)\" \n  proof (cases \"a \u2264 x\")\n    assume \"a \u2264 x\"\n    then show \"ordenada (inserta a (x # xs)) = ordenada (x # xs)\"\n      using menor_menor by auto\n  next\n    assume \"\u00ac(a \u2264 x)\"\n    then have \"ordenada (inserta a (x # xs)) = \n           ordenada (x # inserta a xs)\" by simp\n    also have \"\u2026 = (menor x (inserta a xs) \u2227 ordenada (inserta a xs))\" \n      by simp\n    also have \"\u2026 = (menor x (inserta a xs) \u2227 ordenada xs)\" \n      using HI by simp\n    also have \"\u2026 = (menor x xs \u2227 ordenada xs)\" \n      using \u2039\u00ac(a \u2264 x)\u203a \n      by (simp add: menor_inserta)\n    also have \"\u2026 = ordenada (x # xs)\" \n      by simp\n    finally show \"ordenada (inserta a (x # xs)) = ordenada (x # xs)\" \n      by simp\n  qed\nqed\n\ntext \u2039---------------------------------------------------------------- \n  Ejercicio 7. Demostrar que, para toda lista xs, (ordena xs) est\u00e1\n  ordenada. \n  ------------------------------------------------------------------\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\ntheorem \n  \"ordenada (ordena xs)\"\nby (induct xs) (auto simp add: ordenada_inserta)\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\ntheorem \n  \"ordenada (ordena xs)\"\nproof (induct xs) \n  case Nil\n  then show ?case \n    by simp\nnext\n  case (Cons a xs)\n  then show ?case \n    by (simp add: ordenada_inserta)\nqed\n\ntheorem ordenada_ordena:\n  \"ordenada (ordena xs)\"\nproof (induct xs) \n  show \"ordenada (ordena [])\" by simp\nnext\n  fix x xs\n  assume \"ordenada (ordena xs)\" \n  then have \"ordenada (inserta x (ordena xs))\" \n    by (simp add: ordenada_inserta)  \n  then show \"ordenada (ordena (x # xs))\" by simp\nqed\n\ntext \u2039------------------------------------------------------------------ \n  Nota. El teorema anterior no garantiza que ordena sea correcta, ya que\n  puede que (ordena xs) no tenga los mismos elementos que xs. Por\n  ejemplo, si se define (ordena xs) como [] se tiene que (ordena xs)\n  est\u00e1 ordenada pero no es una ordenaci\u00f3n de xs. \n\n  Para garantizarlo, definimos la funci\u00f3n cuenta.\n  ------------------------------------------------------------------\u203a\n\ntext \u2039----------------------------------------------------------------- \n  Ejercicio 8. Definir la funci\u00f3n\n     cuenta :: int list \u21d2 int \u21d2 nat\n  tal que (cuenta xs y) es el n\u00famero de veces que aparece el elemento y\n  en la lista xs. Por ejemplo, \n     cuenta [1,3,4,3,5] 3 = 2\n  ------------------------------------------------------------------\u203a\n\nfun cuenta :: \"int list \u21d2 int \u21d2 nat\" where\n  \"cuenta []     y = 0\"\n| \"cuenta (x#xs) y = (if x=y \n                      then Suc (cuenta xs y) \n                      else cuenta xs y)\"\n\nvalue \"cuenta [1,3,4,3,5] 3 = 2\"\n\ntext \u2039----------------------------------------------------------------- \n  Ejercicio 9. Demostrar que el n\u00famero de veces que aparece y en \n  (inserta x xs) es \n  * uno m\u00e1s el n\u00famero de veces que aparece en xs, si y = x; \n  * el n\u00famero de veces que aparece en xs, si y \u2260 x; \n  ------------------------------------------------------------------\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma cuenta_inserta:\n  \"cuenta (inserta x xs) y =\n   (if x=y then Suc (cuenta xs y) else cuenta xs y)\"\n  by (induct xs) auto\n\ntext \u2039----------------------------------------------------------------- \n  Ejercicio 10. Demostrar que el n\u00famero de veces que aparece y en \n  (ordena xs) es el n\u00famero de veces que aparece en xs.\n  ------------------------------------------------------------------\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\ntheorem \n  \"cuenta (ordena xs) y = cuenta xs y\"\n  by (induct xs) (auto simp add: cuenta_inserta)\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\ntheorem \n  \"cuenta (ordena xs) y = cuenta xs y\"\nproof (induct xs)\n  case Nil\n  then show ?case \n    by simp\nnext\n  case (Cons a xs)\n  then show ?case \n    by (simp add: cuenta_inserta)\nqed\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\ntheorem cuenta_ordena:\n  \"cuenta (ordena xs) y = cuenta xs y\"\nproof (induct xs)\n  show \"cuenta (ordena []) y = cuenta [] y\" by simp\nnext\n  fix x xs\n  assume HI: \"cuenta (ordena xs) y = cuenta xs y\"\n  show \"cuenta (ordena (x # xs)) y = cuenta (x # xs) y\" \n  proof (cases \"x = y\")\n    assume \"x = y\"\n    have \"cuenta (ordena (x # xs)) y = cuenta (inserta x (ordena xs)) y\" \n      by simp\n    also have \"\u2026 = Suc (cuenta (ordena xs) y)\" using \u2039x = y\u203a \n      by (simp add: cuenta_inserta) \n    also have \"\u2026 = Suc (cuenta xs y)\" using HI by simp\n    also have \"\u2026 = cuenta (x # xs) y\" using \u2039x = y\u203a by simp\n    finally show \"cuenta (ordena (x # xs)) y = cuenta (x # xs) y\" by simp\n  next\n    assume \"x \u2260 y\"\n    have \"cuenta (ordena (x # xs)) y = cuenta (inserta x (ordena xs)) y\" \n      by simp\n    also have \"\u2026 = cuenta (ordena xs) y\" using \u2039x \u2260 y\u203a \n      by (simp add: cuenta_inserta) \n    also have \"\u2026 = cuenta xs y\" using HI by simp\n    also have \"\u2026 = cuenta (x # xs) y\" using \u2039x \u2260 y\u203a by simp\n    finally show \"cuenta (ordena (x # xs)) y = cuenta (x # xs) y\" \n      by simp\n  qed\nqed\n\ntext \u2039Para exportar el c\u00f3digo Haskell de la funci\u00f3n snoc se usa\u203a\n\nexport_code ordena in Haskell \n  module_name OrdInsercion \n  file_prefix \"CodigoGenerado\/\"\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En segunda parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se ha estudiado c\u00f3mo verificar con Isabelle\/HOL la correcci\u00f3n del algoritmo de ordenaci\u00f3n por inserci\u00f3n. La correspondiente teor\u00eda Isabelle\/HOL se muestra a continuaci\u00f3n<\/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\/7029"}],"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=7029"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7029\/revisions"}],"predecessor-version":[{"id":7030,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7029\/revisions\/7030"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7029"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7029"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7029"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}