{"id":7570,"date":"2021-01-18T17:41:26","date_gmt":"2021-01-18T16:41:26","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7570"},"modified":"2021-01-18T17:41:26","modified_gmt":"2021-01-18T16:41:26","slug":"pruebas-en-lean-de-la-relacion-menor-es-irreflexiva-en-los-reales","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/pruebas-en-lean-de-la-relacion-menor-es-irreflexiva-en-los-reales\/","title":{"rendered":"Pruebas en Lean de &#8220;La relaci\u00f3n menor es irreflexiva en los reales&#8221;"},"content":{"rendered":"<p>He a\u00f1adido a la lista <a href=\"https:\/\/bit.ly\/2QwnT30\">DAO (Demostraci\u00f3n Asistida por Ordenador) con Lean<\/a> el <a href=\"https:\/\/youtu.be\/2rs3fj-0RLU\">v\u00eddeo<\/a> en el que se comentan 16 pruebas en Lean de la propiedad<\/p>\n<blockquote><p>\n  La relaci\u00f3n menor es irreflexiva en los reales\n<\/p><\/blockquote>\n<p>usando los estilos declarativo, funcional, aplicativo y autom\u00e1tico.<\/p>\n<p>A continuaci\u00f3n, se muestra el v\u00eddeo<\/p>\n<p><iframe loading=\"lazy\" width=\"560\" height=\"315\" src=\"https:\/\/www.youtube.com\/embed\/2rs3fj-0RLU\" frameborder=\"0\" allow=\"accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture\" allowfullscreen><\/iframe><\/p>\n<p>y el <a href=\"https:\/\/bit.ly\/3oVo2wx\">c\u00f3digo<\/a> de la teor\u00eda utilizada<\/p>\n<pre lang=\"lean\">\nimport data.real.basic\nimport tactic\n\nvariable {x : \u211d}\n\n-- ----------------------------------------------------\n-- Ejercicio. Demostrar que la relaci\u00f3n menor es\n-- irreflexiva en los reales.\n-- ----------------------------------------------------\n\n-- 1\u00aa demostraci\u00f3n\nexample : \u00ac x < x :=\nbegin\n  intro h1,\n  rw lt_iff_le_and_ne at h1,\n  cases h1 with h2 h3,\n  -- clear h2,\n  -- change x = x \u2192 false at h3,\n  apply h3,\n  refl,\nend\n\n-- 2\u00aa demostraci\u00f3n\nexample : \u00ac x < x :=\nbegin\n  intro h1,\n  rw lt_iff_le_and_ne at h1,\n  cases h1 with h2 h3,\n  apply h3,\n  refl,\nend\n\n-- 3\u00aa demostraci\u00f3n\nexample : \u00ac x < x :=\nbegin\n  intro h1,\n  cases (lt_iff_le_and_ne.mp h1) with h2 h3,\n  apply h3,\n  refl,\nend\n\n-- 4\u00aa demostraci\u00f3n\nexample : \u00ac x < x :=\nbegin\n  intro h1,\n  apply (lt_iff_le_and_ne.mp h1).2,\n  refl,\nend\n\n-- 5\u00aa demostraci\u00f3n\nexample : \u00ac x < x :=\nbegin\n  intro h1,\n  exact absurd rfl (lt_iff_le_and_ne.mp h1).2,\nend\n\n-- 6\u00aa demostraci\u00f3n\nexample : \u00ac x < x :=\n\u03bb h, absurd rfl (lt_iff_le_and_ne.mp h).2\n\n-- 7\u00aa demostraci\u00f3n\nexample : \u00ac x < x :=\nassume h1 : x < x,\nhave h2 : x \u2264 x \u2227 x \u2260 x,\n  from lt_iff_le_and_ne.mp h1,\nhave h3 : x \u2260 x,\n  from and.right h2,\nhave h4 : x = x,\n  from rfl,\nshow false,\n  from absurd h4 h3\n\n-- 8\u00aa demostraci\u00f3n\nexample : \u00ac x < x :=\nassume h1 : x < x,\nhave h2 : x \u2264 x \u2227 x \u2260 x,\n  from lt_iff_le_and_ne.mp h1,\nabsurd rfl (and.right h2)\n\n-- 9\u00aa demostraci\u00f3n\nexample : \u00ac x < x :=\nassume h1 : x < x,\nabsurd rfl (and.right (lt_iff_le_and_ne.mp h1))\n\n-- 10\u00aa demostraci\u00f3n\nexample : \u00ac x < x :=\nassume h1 : x < x,\nabsurd rfl (lt_iff_le_and_ne.mp h1).2\n\n-- 11\u00aa demostraci\u00f3n\nexample : \u00ac x < x :=\n\u03bb h, absurd rfl (lt_iff_le_and_ne.mp h).2\n\n-- 12\u00aa demostraci\u00f3n\nexample : \u00ac x < x :=\n-- by library_search\nirrefl x\n\n-- 12\u00aa demostraci\u00f3n\nexample : \u00ac x < x :=\n-- by hint\nby simp\n\n-- 13\u00aa demostraci\u00f3n\nexample : \u00ac x < x :=\nby finish\n\n-- 14\u00aa demostraci\u00f3n\nexample : \u00ac x < x :=\nby norm_num\n\n-- 15\u00aa demostraci\u00f3n\nexample : \u00ac x < x :=\nby linarith\n\n-- 16\u00aa demostraci\u00f3n\nexample : \u00ac x < x :=\nby nlinarith\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>He a\u00f1adido a la lista DAO (Demostraci\u00f3n Asistida por Ordenador) con Lean el v\u00eddeo en el que se comentan 16 pruebas en Lean de la propiedad La relaci\u00f3n menor es irreflexiva en los reales usando los estilos declarativo, funcional, aplicativo y autom\u00e1tico. A continuaci\u00f3n, se muestra el v\u00eddeo y el c\u00f3digo de la teor\u00eda utilizada&#8230;<\/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":[335],"tags":[336],"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\/7570"}],"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=7570"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7570\/revisions"}],"predecessor-version":[{"id":7571,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7570\/revisions\/7571"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7570"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7570"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7570"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}