{"id":709,"date":"2021-08-30T06:00:33","date_gmt":"2021-08-30T04:00:33","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=709"},"modified":"2021-08-25T12:46:18","modified_gmt":"2021-08-25T10:46:18","slug":"las-funciones-de-extraccion-no-estan-acotadas","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/las-funciones-de-extraccion-no-estan-acotadas\/","title":{"rendered":"Las funciones de extracci\u00f3n no est\u00e1n acotadas"},"content":{"rendered":"<p>Para extraer una subsucesi\u00f3n se aplica una funci\u00f3n de extracci\u00f3n que conserva el orden; por ejemplo, la subsucesi\u00f3n<\/p>\n<pre lang=\"text\">\n   u\u2092, u\u2082, u\u2084, u\u2086, ...\n<\/pre>\n<p>se ha obtenido con la funci\u00f3n de extracci\u00f3n \u03c6 tal que \u03c6(n) = 2*n.<\/p>\n<p>En Lean, se puede definir que \u03c6 es una funci\u00f3n de extracci\u00f3n por<\/p>\n<pre lang=\"text\">\n   def extraccion (\u03c6 : \u2115 \u2192 \u2115) :=\n     \u2200 n m, n < m \u2192 \u03c6 n < \u03c6 m\n<\/pre>\n<p>Demostrar que las funciones de extracci\u00f3n no est\u00e1 acotadas; es decir, que si \u03c6 es una funci\u00f3n de extracci\u00f3n, entonces<\/p>\n<pre lang=\"text\">\n    \u2200 N N', \u2203 n \u2265 N', \u03c6 n \u2265 N\n<\/pre>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport tactic\nopen nat\n\nvariable {\u03c6 : \u2115 \u2192 \u2115}\n\ndef extraccion (\u03c6 : \u2115 \u2192 \u2115) :=\n  \u2200 n m, n < m \u2192 \u03c6 n < \u03c6 m\n\nexample\n  (h : extraccion \u03c6)\n  : \u2200 N N', \u2203 n \u2265 N', \u03c6 n \u2265 N :=\nsorry\n<\/pre>\n<p>[expand title=\"Soluciones con Lean\"]<\/p>\n<pre lang=\"lean\">\r\nimport tactic\r\nopen nat\r\n\r\nvariable {\u03c6 : \u2115 \u2192 \u2115}\r\n\r\ndef extraccion (\u03c6 : \u2115 \u2192 \u2115) :=\r\n  \u2200 n m, n < m \u2192 \u03c6 n < \u03c6 m\r\n\r\nlemma aux\r\n  (h : extraccion \u03c6)\r\n  : \u2200 n, n \u2264 \u03c6 n :=\r\nbegin\r\n  intro n,\r\n  induction n with m HI,\r\n  { exact nat.zero_le (\u03c6 0), },\r\n  { apply nat.succ_le_of_lt,\r\n    calc m \u2264 \u03c6 m        : HI\r\n       ... < \u03c6 (succ m) : h m (m+1) (lt_add_one m), },\r\nend\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n  (h : extraccion \u03c6)\r\n  : \u2200 N N', \u2203 n \u2265 N', \u03c6 n \u2265 N :=\r\nbegin\r\n  intros N N',\r\n  let n := max N N',\r\n  use n,\r\n  split,\r\n  { exact le_max_right N N', },\r\n  { calc N \u2264 n   : le_max_left N N'\r\n       ... \u2264 \u03c6 n : aux h n, },\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n  (h : extraccion \u03c6)\r\n  : \u2200 N N', \u2203 n \u2265 N', \u03c6 n \u2265 N :=\r\nbegin\r\n  intros N N',\r\n  let n := max N N',\r\n  use n,\r\n  split,\r\n  { exact le_max_right N N', },\r\n  { exact le_trans (le_max_left N N')\r\n                   (aux h n), },\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample\r\n  (h : extraccion \u03c6)\r\n  : \u2200 N N', \u2203 n \u2265 N', \u03c6 n \u2265 N :=\r\nbegin\r\n  intros N N',\r\n  use max N N',\r\n  split,\r\n  { exact le_max_right N N', },\r\n  { exact le_trans (le_max_left N N')\r\n                   (aux h (max N N')), },\r\nend\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample\r\n  (h : extraccion \u03c6)\r\n  : \u2200 N N', \u2203 n \u2265 N', \u03c6 n \u2265 N :=\r\nbegin\r\n  intros N N',\r\n  use max N N',\r\n  exact \u27e8le_max_right N N',\r\n         le_trans (le_max_left N N')\r\n                  (aux h (max N N'))\u27e9,\r\nend\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample\r\n  (h : extraccion \u03c6)\r\n  : \u2200 N N', \u2203 n \u2265 N', \u03c6 n \u2265 N :=\r\n\u03bb N N',\r\n  \u27e8max N N', \u27e8le_max_right N N',\r\n              le_trans (le_max_left N N')\r\n                       (aux h (max N N'))\u27e9\u27e9\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nexample\r\n  (h : extraccion \u03c6)\r\n  : \u2200 N N', \u2203 n \u2265 N', \u03c6 n \u2265 N :=\r\nassume N N',\r\nlet n := max N N' in\r\nhave h1 : n \u2265 N',\r\n  from le_max_right N N',\r\nshow \u2203 n \u2265 N', \u03c6 n \u2265 N, from\r\nexists.intro n\r\n  (exists.intro h1\r\n    (show \u03c6 n \u2265 N, from\r\n       calc N \u2264 n   : le_max_left N N'\r\n          ... \u2264 \u03c6 n : aux h n))\r\n\r\n-- 7\u00aa demostraci\u00f3n\r\nexample\r\n  (h : extraccion \u03c6)\r\n  : \u2200 N N', \u2203 n \u2265 N', \u03c6 n \u2265 N :=\r\nassume N N',\r\nlet n := max N N' in\r\nhave h1 : n \u2265 N',\r\n  from le_max_right N N',\r\nshow \u2203 n \u2265 N', \u03c6 n \u2265 N, from\r\n\u27e8n, h1, calc N \u2264 n   : le_max_left N N'\r\n          ...  \u2264 \u03c6 n : aux h n\u27e9\r\n\r\n-- 8\u00aa demostraci\u00f3n\r\nexample\r\n  (h : extraccion \u03c6)\r\n  : \u2200 N N', \u2203 n \u2265 N', \u03c6 n \u2265 N :=\r\nassume N N',\r\nlet n := max N N' in\r\nhave h1 : n \u2265 N',\r\n  from le_max_right N N',\r\nshow \u2203 n \u2265 N', \u03c6 n \u2265 N, from\r\n\u27e8n, h1, le_trans (le_max_left N N')\r\n                 (aux h (max N N'))\u27e9\r\n\r\n-- 9\u00aa demostraci\u00f3n\r\nexample\r\n  (h : extraccion \u03c6)\r\n  : \u2200 N N', \u2203 n \u2265 N', \u03c6 n \u2265 N :=\r\nassume N N',\r\nlet n := max N N' in\r\nhave h1 : n \u2265 N',\r\n  from le_max_right N N',\r\n\u27e8n, h1, le_trans (le_max_left N N')\r\n                 (aux h n)\u27e9\r\n\r\n-- 10\u00aa demostraci\u00f3n\r\nexample\r\n  (h : extraccion \u03c6)\r\n  : \u2200 N N', \u2203 n \u2265 N', \u03c6 n \u2265 N :=\r\nassume N N',\r\n\u27e8max N N', le_max_right N N',\r\n           le_trans (le_max_left N N')\r\n                    (aux h (max N N'))\u27e9\r\n\r\n-- 11\u00aa demostraci\u00f3n\r\nlemma extraccion_mye\r\n  (h : extraccion \u03c6)\r\n  : \u2200 N N', \u2203 n \u2265 N', \u03c6 n \u2265 N :=\r\n\u03bb N N',\r\n  \u27e8max N N', le_max_right N N',\r\n             le_trans (le_max_left N N')\r\n             (aux h (max N N'))\u27e9\r\n<\/pre>\n<p>Se puede interactuar con la prueba anterior en <a href=\"https:\/\/leanprover-community.github.io\/lean-web-editor\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus\/main\/src\/Las_funciones_de_extraccion_no_estan_acotadas.lean\" rel=\"noopener noreferrer\" target=\"_blank\">esta sesi\u00f3n con Lean<\/a>.<\/p>\n<p>En los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con &#60;pre lang=&quot;lean&quot;&#62; y otra con &#60;\/pre&#62;<br \/>\n[\/expand]<\/p>\n<p>[expand title=\"Soluciones con Isabelle\/HOL\"]<\/p>\n<pre lang=\"isar\">\r\ntheory Las_funciones_de_extraccion_no_estan_acotadas\r\nimports Main\r\nbegin\r\n\r\ndefinition extraccion :: \"(nat \u21d2 nat) \u21d2 bool\" where\r\n  \"extraccion \u03c6 \u27f7 (\u2200 n m. n < m \u27f6 \u03c6 n < \u03c6 m)\"\r\n\r\n(* En la demostraci\u00f3n se usar\u00e1 el siguiente lema *)\r\nlemma aux :\r\n  assumes \"extraccion \u03c6\"\r\n  shows   \"n \u2264 \u03c6 n\"\r\nproof (induct n)\r\n  show \"0 \u2264 \u03c6 0\"\r\n    by simp\r\nnext\r\n  fix n\r\n  assume HI : \"n \u2264 \u03c6 n\"\r\n  also have \"\u03c6 n < \u03c6 (Suc n)\"\r\n    using assms extraccion_def by blast\r\n  finally show \"Suc n \u2264 \u03c6 (Suc n)\"\r\n    by simp\r\nqed\r\n\r\n(* 1\u00aa demostraci\u00f3n *)\r\nlemma\r\n  assumes \"extraccion \u03c6\"\r\n  shows   \"\u2200 N N'. \u2203 k \u2265 N'. \u03c6 k \u2265 N\"\r\nproof (intro allI)\r\n  fix N N' :: nat\r\n  let ?k = \"max N N'\"\r\n  have \"max N N' \u2264 ?k\"\r\n    by (rule le_refl)\r\n  then have hk : \"N \u2264 ?k \u2227 N' \u2264 ?k\"\r\n    by (simp only: max.bounded_iff)\r\n  then have \"?k \u2265 N'\"\r\n    by (rule conjunct2)\r\n  moreover\r\n  have \"N \u2264 \u03c6 ?k\"\r\n  proof -\r\n    have \"N \u2264 ?k\"\r\n      using hk by (rule conjunct1)\r\n    also have \"\u2026 \u2264 \u03c6 ?k\"\r\n      using assms by (rule aux)\r\n    finally show \"N \u2264 \u03c6 ?k\"\r\n      by this\r\n  qed\r\n  ultimately have \"?k \u2265 N' \u2227 \u03c6 ?k \u2265 N\"\r\n    by (rule conjI)\r\n  then show \"\u2203k \u2265 N'. \u03c6 k \u2265 N\"\r\n    by (rule exI)\r\nqed\r\n\r\n(* 2\u00aa demostraci\u00f3n *)\r\nlemma\r\n  assumes \"extraccion \u03c6\"\r\n  shows   \"\u2200 N N'. \u2203 k \u2265 N'. \u03c6 k \u2265 N\"\r\nproof (intro allI)\r\n  fix N N' :: nat\r\n  let ?k = \"max N N'\"\r\n  have \"?k \u2265 N'\"\r\n    by simp\r\n  moreover\r\n  have \"N \u2264 \u03c6 ?k\"\r\n  proof -\r\n    have \"N \u2264 ?k\"\r\n      by simp\r\n    also have \"\u2026 \u2264 \u03c6 ?k\"\r\n      using assms by (rule aux)\r\n    finally show \"N \u2264 \u03c6 ?k\"\r\n      by this\r\n  qed\r\n  ultimately show \"\u2203k \u2265 N'. \u03c6 k \u2265 N\"\r\n    by blast\r\nqed\r\n\r\nend\r\n<\/pre>\n<p>En los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con &#60;pre lang=&quot;isar&quot;&#62; y otra con &#60;\/pre&#62;<br \/>\n[\/expand]<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Para extraer una subsucesi\u00f3n se aplica una funci\u00f3n de extracci\u00f3n que conserva el orden; por ejemplo, la subsucesi\u00f3n u\u2092, u\u2082, u\u2084, u\u2086, &#8230; se ha obtenido con la funci\u00f3n de extracci\u00f3n \u03c6 tal que \u03c6(n) = 2*n. En Lean, se puede definir que \u03c6 es una funci\u00f3n de extracci\u00f3n por def extraccion (\u03c6 : \u2115 \u2192 \u2115) := \u2200 n m, n < m \u2192 \u03c6 n < \u03c6 m Demostrar que las funciones de extracci\u00f3n no est\u00e1 acotadas; es decir, que si \u03c6 es una funci\u00f3n de extracci\u00f3n, entonces \u2200 N N', \u2203 n \u2265 N', \u03c6 n \u2265 N Para ello, completar la siguiente teor\u00eda de Lean: import tactic open nat variable {\u03c6 : \u2115 \u2192 \u2115} def extraccion (\u03c6 : \u2115 \u2192...\n<\/p>\n","protected":false},"author":1,"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,"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[168],"tags":[90,92,58,53,57,94,177,115,185,186,51,100,98,49,169,43,63,183,182,184,173,181,171,170,48,46],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/709"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/comments?post=709"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/709\/revisions"}],"predecessor-version":[{"id":717,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/709\/revisions\/717"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=709"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=709"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=709"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}