{"id":587,"date":"2021-07-21T08:39:27","date_gmt":"2021-07-21T06:39:27","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=587"},"modified":"2021-07-21T08:39:27","modified_gmt":"2021-07-21T06:39:27","slug":"una-funcion-creciente-e-involutiva-es-la-identidad","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/una-funcion-creciente-e-involutiva-es-la-identidad\/","title":{"rendered":"Una funci\u00f3n creciente e involutiva es la identidad"},"content":{"rendered":"<p>Sea una funci\u00f3n f de \u211d en \u211d.<\/p>\n<ul>\n<li>Se dice que f es creciente si para todo x e y tales que x \u2264 y se tiene que f(x) \u2264 f(y).<\/li>\n<li>Se dice que f es involutiva si para todo x se tiene que f(f(x)) = x.<\/li>\n<\/ul>\n<p>En Lean que f sea creciente se representa por <code>monotone f<\/code> y que sea involutiva por <code>involutive f<\/code><\/p>\n<p>Demostrar que si f es creciente e involutiva, entonces f es la identidad.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport data.real.basic\nopen function\n\nvariable (f : \u211d \u2192 \u211d)\n\nexample\n  (hc : monotone f)\n  (hi : involutive f)\n  : f = id :=\nsorry\n<\/pre>\n<p>[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n<pre lang=\"lean\">\r\nimport data.real.basic\r\nopen function\r\n\r\nvariable (f : \u211d \u2192 \u211d)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n  (hc : monotone f)\r\n  (hi : involutive f)\r\n  : f = id :=\r\nbegin\r\n  unfold monotone involutive at *,\r\n  funext,\r\n  unfold id,\r\n  cases (le_total (f x) x) with h1 h2,\r\n  { apply antisymm h1,\r\n    have h3 : f (f x) \u2264 f x,\r\n      { apply hc,\r\n        exact h1, },\r\n    rwa hi at h3, },\r\n  { apply antisymm _ h2,\r\n    have h4 : f x \u2264 f (f x),\r\n      { apply hc,\r\n        exact h2, },\r\n    rwa hi at h4, },\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n  (hc : monotone f)\r\n  (hi : involutive f)\r\n  : f = id :=\r\nbegin\r\n  funext,\r\n  cases (le_total (f x) x) with h1 h2,\r\n  { apply antisymm h1,\r\n    have h3 : f (f x) \u2264 f x := hc h1,\r\n    rwa hi at h3, },\r\n  { apply antisymm _ h2,\r\n    have h4 : f x \u2264 f (f x) := hc h2,\r\n    rwa hi at h4, },\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample\r\n  (hc : monotone f)\r\n  (hi : involutive f)\r\n  : f = id :=\r\nbegin\r\n  funext,\r\n  cases (le_total (f x) x) with h1 h2,\r\n  { apply antisymm h1,\r\n    calc x\r\n         = f (f x) : (hi x).symm\r\n     ... \u2264 f x     : hc h1 },\r\n  { apply antisymm _ h2,\r\n    calc f x\r\n         \u2264 f (f x) : hc h2\r\n     ... = x       : hi x },\r\nend\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\/Una_funcion_creciente_e_involutiva_es_la_identidad.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 Una_funcion_creciente_e_involutiva_es_la_identidad\r\nimports Main HOL.Real\r\nbegin\r\n\r\ndefinition involutiva :: \"(real \u21d2 real) \u21d2 bool\"\r\n  where \"involutiva f \u27f7 (\u2200x. f (f x) = x)\"\r\n\r\n(* 1\u00aa demostraci\u00f3n *)\r\nlemma\r\n  fixes f :: \"real \u21d2 real\"\r\n  assumes \"mono f\"\r\n          \"involutiva f\"\r\n  shows   \"f = id\"\r\nproof (unfold fun_eq_iff; intro allI)\r\n  fix x\r\n  have \"x \u2264 f x \u2228 f x \u2264 x\"\r\n    by (rule linear)\r\n  then have \"f x = x\"\r\n  proof (rule disjE)\r\n    assume \"x \u2264 f x\"\r\n    then have \"f x \u2264 f (f x)\"\r\n      using assms(1) by (simp only: monoD)\r\n    also have \"\u2026 = x\"\r\n      using assms(2) by (simp only: involutiva_def)\r\n    finally have \"f x \u2264 x\"\r\n      by this\r\n    show \"f x = x\"\r\n      using \u2039f x \u2264 x\u203a \u2039x \u2264 f x\u203a by (simp only: antisym)\r\n  next\r\n    assume \"f x \u2264 x\"\r\n    have \"x = f (f x)\"\r\n      using assms(2) by (simp only: involutiva_def)\r\n    also have \"... \u2264 f x\"\r\n      using \u2039f x \u2264 x\u203a assms(1) by (simp only: monoD)\r\n    finally have \"x \u2264 f x\"\r\n      by this\r\n    show \"f x = x\"\r\n      using \u2039f x \u2264 x\u203a \u2039x \u2264 f x\u203a by (simp only: monoD)\r\n  qed\r\n  then show \"f x = id x\"\r\n    by (simp only: id_apply)\r\nqed\r\n\r\n(* 2\u00aa demostraci\u00f3n *)\r\nlemma\r\n  fixes f :: \"real \u21d2 real\"\r\n  assumes \"mono f\"\r\n          \"involutiva f\"\r\n  shows   \"f = id\"\r\nproof\r\n  fix x\r\n  have \"x \u2264 f x \u2228 f x \u2264 x\"\r\n    by (rule linear)\r\n  then have \"f x = x\"\r\n  proof\r\n    assume \"x \u2264 f x\"\r\n    then have \"f x \u2264 f (f x)\"\r\n      using assms(1) by (simp only: monoD)\r\n    also have \"\u2026 = x\"\r\n      using assms(2) by (simp only: involutiva_def)\r\n    finally have \"f x \u2264 x\"\r\n      by this\r\n    show \"f x = x\"\r\n      using \u2039f x \u2264 x\u203a \u2039x \u2264 f x\u203a by auto\r\n  next\r\n    assume \"f x \u2264 x\"\r\n    have \"x = f (f x)\"\r\n      using assms(2) by (simp only: involutiva_def)\r\n    also have \"... \u2264 f x\"\r\n      by (simp add: \u2039f x \u2264 x\u203a assms(1) monoD)\r\n    finally have \"x \u2264 f x\"\r\n      by this\r\n    show \"f x = x\"\r\n      using \u2039f x \u2264 x\u203a \u2039x \u2264 f x\u203a by auto\r\n  qed\r\n  then show \"f x = id x\"\r\n    by simp\r\nqed\r\n\r\n(* 3\u00aa demostraci\u00f3n *)\r\nlemma\r\n  fixes f :: \"real \u21d2 real\"\r\n  assumes \"mono f\"\r\n          \"involutiva f\"\r\n  shows   \"f = id\"\r\nproof\r\n  fix x\r\n  have \"x \u2264 f x \u2228 f x \u2264 x\"\r\n    by (rule linear)\r\n  then have \"f x = x\"\r\n  proof\r\n    assume \"x \u2264 f x\"\r\n    then have \"f x \u2264 x\"\r\n      by (metis assms involutiva_def mono_def)\r\n    then show \"f x = x\"\r\n      using \u2039x \u2264 f x\u203a by auto\r\n  next\r\n    assume \"f x \u2264 x\"\r\n    then have \"x \u2264 f x\"\r\n      by (metis assms involutiva_def mono_def)\r\n    then show \"f x = x\"\r\n      using \u2039f x \u2264 x\u203a by auto\r\n  qed\r\n  then show \"f x = id x\"\r\n    by simp\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>Sea una funci\u00f3n f de \u211d en \u211d. Se dice que f es creciente si para todo x e y tales que x \u2264 y se tiene que f(x) \u2264 f(y). Se dice que f es involutiva si para todo x se tiene que f(f(x)) = x. En Lean que f sea creciente se representa por monotone f y que sea involutiva por involutive f Demostrar que si f es creciente e involutiva, entonces f es la identidad. Para ello, completar la siguiente teor\u00eda de Lean: import data.real.basic open function variable (f : \u211d \u2192 \u211d) example (hc : monotone f) (hi : involutive f) : f = id := sorry [expand title=\u00bbSoluciones con Lean\u00bb] import data.real.basic open function variable (f : \u211d \u2192 \u211d)&#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\/587"}],"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=587"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/587\/revisions"}],"predecessor-version":[{"id":588,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/587\/revisions\/588"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=587"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=587"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=587"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}