{"id":583,"date":"2021-07-19T06:00:56","date_gmt":"2021-07-19T04:00:56","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=583"},"modified":"2021-07-18T19:03:31","modified_gmt":"2021-07-18T17:03:31","slug":"la-composicion-de-crecientes-es-creciente","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/la-composicion-de-crecientes-es-creciente\/","title":{"rendered":"La composici\u00f3n de crecientes es creciente"},"content":{"rendered":"<p>Se dice que una funci\u00f3n f de \u211d en \u211d es <a href=\"https:\/\/bit.ly\/2UShggL\">creciente<\/a> si para todo x e y tales que x \u2264 y se tiene que f(x) \u2264 f(y).<\/p>\n<p>En Lean que f sea creciente se representa por <code>monotone f<\/code>.<\/p>\n<p>Demostrar que la composici\u00f3n de dos funciones crecientes es una funci\u00f3n creciente.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport data.real.basic\n\nvariables (f g : \u211d \u2192 \u211d)\n\nexample\n  (hf : monotone f)\n  (hg : monotone g)\n  : monotone (g \u2218 f) :=\nsorry\n<\/pre>\n<p>[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n<pre lang=\"lean\">\r\nimport data.real.basic\r\n\r\nvariables (f g : \u211d \u2192 \u211d)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n  (hf : monotone f)\r\n  (hg : monotone g)\r\n  : monotone (g \u2218 f) :=\r\nbegin\r\n  intros x y hxy,\r\n  calc (g \u2218 f) x\r\n       = g (f x)   : rfl\r\n   ... \u2264 g (f y)   : hg (hf hxy)\r\n   ... = (g \u2218 f) y : rfl,\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n  (hf : monotone f)\r\n  (hg : monotone g)\r\n  : monotone (g \u2218 f) :=\r\nbegin\r\n  unfold monotone at *,\r\n  intros x y h,\r\n  unfold function.comp,\r\n  apply hg,\r\n  apply hf,\r\n  exact h,\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample\r\n  (hf : monotone f)\r\n  (hg : monotone g)\r\n  : monotone (g \u2218 f) :=\r\nbegin\r\n  intros x y h,\r\n  apply hg,\r\n  apply hf,\r\n  exact h,\r\nend\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample\r\n  (hf : monotone f)\r\n  (hg : monotone g)\r\n  : monotone (g \u2218 f) :=\r\nbegin\r\n  intros x xy h,\r\n  apply hg,\r\n  exact hf h,\r\nend\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample\r\n  (hf : monotone f)\r\n  (hg : monotone g)\r\n  : monotone (g \u2218 f) :=\r\nbegin\r\n  intros x y h,\r\n  exact hg (hf h),\r\nend\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nexample\r\n  (hf : monotone f)\r\n  (hg : monotone g)\r\n  : monotone (g \u2218 f) :=\r\n\u03bb x y h, hg (hf h)\r\n\r\n-- 7\u00aa demostraci\u00f3n\r\nexample\r\n  (hf : monotone f)\r\n  (hg : monotone g)\r\n  : monotone (g \u2218 f) :=\r\nbegin\r\n  intros x y h,\r\n  specialize hf h,\r\n  exact hg hf,\r\nend\r\n\r\n-- 8\u00aa demostraci\u00f3n\r\nexample\r\n  (hf : monotone f)\r\n  (hg : monotone g)\r\n  : monotone (g \u2218 f) :=\r\nassume x y,\r\nassume h1 : x \u2264 y,\r\nhave h2 : f x \u2264 f y,\r\n  from hf h1,\r\nshow (g \u2218 f) x \u2264 (g \u2218 f) y, from\r\n  calc (g \u2218 f) x\r\n       = g (f x)   : rfl\r\n   ... \u2264 g (f y)   : hg h2\r\n   ... = (g \u2218 f) y : by refl\r\n\r\n-- 9\u00aa demostraci\u00f3n\r\nexample\r\n  (hf : monotone f)\r\n  (hg : monotone g)\r\n  : monotone (g \u2218 f) :=\r\n-- by hint\r\nby tauto\r\n\r\n-- 10\u00aa demostraci\u00f3n\r\nexample\r\n  (hf : monotone f)\r\n  (hg : monotone g)\r\n  : monotone (g \u2218 f) :=\r\n-- by library_search\r\nmonotone.comp hg hf\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\/La_composicion_de_crecientes_es_creciente.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=\u00bbSoluciones con Isabelle\/HOL\u00bb]<\/p>\n<pre lang=\"isar\">\r\ntheory La_composicion_de_crecientes_es_creciente\r\nimports Main HOL.Real\r\nbegin\r\n\r\n(* 1\u00aa demostraci\u00f3n *)\r\nlemma\r\n  fixes f g :: \"real \u21d2 real\"\r\n  assumes \"mono f\"\r\n          \"mono g\"\r\n  shows   \"mono (g \u2218 f)\"\r\nproof (rule monoI)\r\n  fix x y :: real\r\n  assume \"x \u2264 y\"\r\n  have \"(g \u2218 f) x = g (f x)\"\r\n    by (simp only: o_apply)\r\n  also have \"\u2026 \u2264 g (f y)\"\r\n    using assms \u2039x \u2264 y\u203a\r\n    by (simp only: monoD)\r\n  also have \"\u2026 = (g \u2218 f) y\"\r\n    by (simp only: o_apply)\r\n  finally show \"(g \u2218 f) x \u2264 (g \u2218 f) y\"\r\n    by this\r\nqed\r\n\r\n(* 2\u00aa demostraci\u00f3n *)\r\nlemma\r\n  fixes f g :: \"real \u21d2 real\"\r\n  assumes \"mono f\"\r\n          \"mono g\"\r\n  shows   \"mono (g \u2218 f)\"\r\nproof (rule monoI)\r\n  fix x y :: real\r\n  assume \"x \u2264 y\"\r\n  have \"(g \u2218 f) x = g (f x)\"   by simp\r\n  also have \"\u2026 \u2264 g (f y)\"      by (simp add: \u2039x \u2264 y\u203a assms monoD)\r\n  also have \"\u2026 = (g \u2218 f) y\"    by simp\r\n  finally show \"(g \u2218 f) x \u2264 (g \u2218 f) y\" .\r\nqed\r\n\r\n(* 3\u00aa demostraci\u00f3n *)\r\nlemma\r\n  assumes \"mono f\"\r\n          \"mono g\"\r\n  shows   \"mono (g \u2218 f)\"\r\n  by (metis assms comp_def mono_def)\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>Se dice que una funci\u00f3n f de \u211d en \u211d es creciente si para todo x e y tales que x \u2264 y se tiene que f(x) \u2264 f(y). En Lean que f sea creciente se representa por monotone f. Demostrar que la composici\u00f3n de dos funciones crecientes es una funci\u00f3n creciente. Para ello, completar la siguiente teor\u00eda de Lean: import data.real.basic variables (f g : \u211d \u2192 \u211d) example (hf : monotone f) (hg : monotone g) : monotone (g \u2218 f) := sorry [expand title=\u00bbSoluciones con Lean\u00bb] import data.real.basic variables (f g : \u211d \u2192 \u211d) &#8212; 1\u00aa demostraci\u00f3n example (hf : monotone f) (hg : monotone g) : monotone (g \u2218 f) := begin intros x y hxy, calc (g \u2218 f)&#8230;<\/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":[13],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/583"}],"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=583"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/583\/revisions"}],"predecessor-version":[{"id":584,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/583\/revisions\/584"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=583"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=583"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=583"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}