{"id":791,"date":"2021-09-26T10:37:41","date_gmt":"2021-09-26T08:37:41","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=791"},"modified":"2021-09-26T10:44:54","modified_gmt":"2021-09-26T08:44:54","slug":"identidad-de-brahmagupta-fibonacci","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/identidad-de-brahmagupta-fibonacci\/","title":{"rendered":"Identidad de Brahmagupta-Fibonacci"},"content":{"rendered":"<p>Demostrar la <a href=\"https:\/\/bit.ly\/3ucEc80\">identidad de Brahmagupta-Fibonacci<\/a><\/p>\n<pre lang=\"text\">\n   (a\u00b2 + b\u00b2)(c\u00b2 + d\u00b2) = (ac - bd)\u00b2 + (ad + bc)\u00b2\n<\/pre>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport data.real.basic\n\nvariables (a b c d : \u211d)\n\nexample :\n  (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 :=\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 (a b c d : \u211d)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample : (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 :=\r\ncalc (a^2 + b^2) * (c^2 + d^2)\r\n     = a^2 * (c^2 + d^2) + b^2 * (c^2 + d^2)\r\n         : right_distrib (a^2) (b^2) (c^2 + d^2)\r\n ... = (a^2*c^2 + a^2*d^2) + b^2 * (c^2 + d^2)\r\n         : congr_arg2 (+) (left_distrib (a^2) (c^2) (d^2)) rfl\r\n ... = (a^2*c^2 + a^2*d^2) + (b^2*c^2 + b^2*d^2)\r\n         : congr_arg2 (+) rfl (left_distrib (b^2) (c^2) (d^2))\r\n ... = ((a*c)^2 + (b*d)^2) + ((a*d)^2 + (b*c)^2)\r\n         : by ring\r\n ... = ((a*c)^2 - 2*a*c*b*d + (b*d)^2) + ((a*d)^2 + 2*a*d*b*c + (b*c)^2)\r\n         : by ring\r\n ... = (a*c - b*d)^2 + (a*d + b*c)^2\r\n         : by ring\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample : (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 :=\r\nby ring\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\/Identidad_de_Brahmagupta-Fibonacci.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 \"Identidad_de_Brahmagupta-Fibonacci\"\r\nimports Main HOL.Real\r\nbegin\r\n\r\n(* 1\u00aa demostraci\u00f3n *)\r\nlemma\r\n  fixes a b c d :: real\r\n  shows \"(a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2\"\r\nproof -\r\n  have \"(a^2 + b^2) * (c^2 + d^2) = a^2 * (c^2 + d^2) + b^2 * (c^2 + d^2)\"\r\n    by (simp only: distrib_right)\r\n  also have \"\u2026 = (a^2*c^2 + a^2*d^2) + b^2 * (c^2 + d^2)\"\r\n    by (simp only: distrib_left)\r\n  also have \"\u2026 = (a^2*c^2 + a^2*d^2) + (b^2*c^2 + b^2*d^2)\"\r\n    by (simp only: distrib_left)\r\n  also have \"\u2026 = ((a*c)^2 + (b*d)^2) + ((a*d)^2 + (b*c)^2)\"\r\n    by algebra\r\n  also have \"\u2026 = ((a*c)^2 - 2*a*c*b*d + (b*d)^2) + ((a*d)^2 + 2*a*d*b*c + (b*c)^2)\"\r\n    by algebra\r\n  also have \"\u2026 = (a*c - b*d)^2 + (a*d + b*c)^2\"\r\n    by algebra\r\n  finally show \"(a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2\" .\r\nqed\r\n\r\n(* 2\u00aa demostraci\u00f3n *)\r\nlemma\r\n  fixes a b c d :: real\r\n  shows \"(a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2\"\r\nby algebra\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>Demostrar la identidad de Brahmagupta-Fibonacci (a\u00b2 + b\u00b2)(c\u00b2 + d\u00b2) = (ac &#8211; bd)\u00b2 + (ad + bc)\u00b2 Para ello, completar la siguiente teor\u00eda de Lean: import data.real.basic variables (a b c d : \u211d) example : (a^2 + b^2) * (c^2 + d^2) = (a*c &#8211; b*d)^2 + (a*d + b*c)^2 := sorry [expand title=\u00bbSoluciones con Lean\u00bb] import data.real.basic variables (a b c d : \u211d) &#8212; 1\u00aa demostraci\u00f3n example : (a^2 + b^2) * (c^2 + d^2) = (a*c &#8211; b*d)^2 + (a*d + b*c)^2 := calc (a^2 + b^2) * (c^2 + d^2) = a^2 * (c^2 + d^2) + b^2 * (c^2 + d^2) : right_distrib (a^2) (b^2) (c^2 + d^2) &#8230; = (a^2*c^2 + a^2*d^2) + b^2 * (c^2 +&#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":[24],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/791"}],"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=791"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/791\/revisions"}],"predecessor-version":[{"id":793,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/791\/revisions\/793"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=791"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=791"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=791"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}