{"id":7573,"date":"2021-01-20T14:05:30","date_gmt":"2021-01-20T13:05:30","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7573"},"modified":"2021-01-20T14:05:30","modified_gmt":"2021-01-20T13:05:30","slug":"pruebas-en-lean-de-un-numero-es-par-si-y-solo-si-lo-es-su-cuadrado","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/pruebas-en-lean-de-un-numero-es-par-si-y-solo-si-lo-es-su-cuadrado\/","title":{"rendered":"Pruebas en Lean de &#8220;Un n\u00famero es par si, y s\u00f3lo si, lo es su cuadrado&#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\/-PczmYJOFak\">v\u00eddeo<\/a> en el que se comentan 3 pruebas en Lean de la propiedad<\/p>\n<blockquote><p>\n  Un n\u00famero es par si, y s\u00f3lo si, lo es su cuadrado-\n<\/p><\/blockquote>\n<p>usando los estilos declarativo, aplicativo y funcional.<\/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\/-PczmYJOFak\" 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\/3p5ytOa\">c\u00f3digo<\/a> de la teor\u00eda utilizada<\/p>\n<pre lang=\"lean\">\nimport data.int.parity\nopen int\n\nvariable (n : \u2124)\n\n-- ----------------------------------------------------\n-- Ejercicio. Demostrar que un n\u00famero es par syss lo es\n-- su cuadrado.\n-- ----------------------------------------------------\n\n-- 1\u00aa demostraci\u00f3n\nexample :\n  even (n^2) \u2194 even n :=\nbegin\n  split,\n  { contrapose,\n    rw \u2190 odd_iff_not_even,\n    rw \u2190 odd_iff_not_even,\n    unfold odd,\n    intro h,\n    cases h with k hk,\n    use 2*k*(k+1),\n    rw hk,\n    ring, },\n  { unfold even,\n    intro h,\n    cases h with k hk,\n    use 2*k^2,\n    rw hk,\n    ring, },\nend\n\n-- 2\u00aa demostraci\u00f3n\nexample :\n  even (n^2) \u2194 even n :=\nbegin\n  split,\n  { contrapose,\n    rw \u2190 odd_iff_not_even,\n    rw \u2190 odd_iff_not_even,\n    rintro \u27e8k, rfl\u27e9,\n    use 2*k*(k+1),\n    ring, },\n  { rintro \u27e8k, rfl\u27e9,\n    use 2*k^2,\n    ring, },\nend\n\n-- 3\u00aa demostraci\u00f3n\nexample :\n  even (n^2) \u2194 even n :=\niff.intro\n  ( have h : \u00aceven n \u2192 \u00aceven (n^2),\n      { assume h1 : \u00aceven n,\n        have h2 : odd n,\n          from odd_iff_not_even.mpr h1,\n        have h3: odd (n^2), from\n          exists.elim h2\n            ( assume k,\n              assume hk : n = 2*k+1,\n              have h4 : n^2 = 2*(2*k*(k+1))+1, from\n                calc  n^2\n                    = (2*k+1)^2       : by rw hk\n                ... = 4*k^2+4*k+1     : by ring\n                ... = 2*(2*k*(k+1))+1 : by ring,\n              show odd (n^2),\n                from exists.intro (2*k*(k+1)) h4),\n        show \u00aceven (n^2),\n          from odd_iff_not_even.mp h3 },\n    show even (n^2) \u2192 even n,\n      from not_imp_not.mp h )\n  ( assume h1 : even n,\n    show even (n^2), from\n      exists.elim h1\n        ( assume k,\n          assume hk : n = 2*k ,\n          have h2 : n^2 = 2*(2*k^2), from\n            calc  n^2\n                = (2*k)^2   : by rw hk\n            ... = 2*(2*k^2) : by ring,\n          show even (n^2),\n            from exists.intro (2*k^2) h2 ))\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 3 pruebas en Lean de la propiedad Un n\u00famero es par si, y s\u00f3lo si, lo es su cuadrado- usando los estilos declarativo, aplicativo y funcional. A continuaci\u00f3n, se muestra el v\u00eddeo y el c\u00f3digo de&#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\/7573"}],"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=7573"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7573\/revisions"}],"predecessor-version":[{"id":7574,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7573\/revisions\/7574"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7573"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7573"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7573"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}