{"id":1229,"date":"2022-12-01T06:00:52","date_gmt":"2022-12-01T04:00:52","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1229"},"modified":"2022-11-30T18:31:47","modified_gmt":"2022-11-30T16:31:47","slug":"01-dic-22","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/01-dic-22\/","title":{"rendered":"Si x e y son sumas de dos cuadrados, entonces xy tambi\u00e9n lo es"},"content":{"rendered":"

Demostrar que si x e y son sumas de dos cuadrados, entonces xy tambi\u00e9n lo es.<\/p>\n

Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n

\nimport tactic\nvariables {\u03b1 : Type*} [comm_ring \u03b1]\nvariables {x y : \u03b1}\n\n-- (es_suma_de_cuadrados x) se verifica si x se puede escribir como la\n-- suma de dos cuadrados.\ndef es_suma_de_cuadrados (x : \u03b1) := \u2203 a b, x = a^2 + b^2\n\nexample\n  (hx : es_suma_de_cuadrados x)\n  (hy : es_suma_de_cuadrados y)\n  : es_suma_de_cuadrados (x * y) :=\nsorry\n<\/pre>\n
<\/p>\n
Soluciones con Lean<\/b><\/p>\n
\nimport tactic\nvariables {\u03b1 : Type*} [comm_ring \u03b1]\nvariables {x y : \u03b1}\n\n-- (es_suma_de_cuadrados x) se verifica si x se puede escribir como la\n-- suma de dos cuadrados.\ndef es_suma_de_cuadrados (x : \u03b1) := \u2203 a b, x = a^2 + b^2\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hx : es_suma_de_cuadrados x)\n  (hy : es_suma_de_cuadrados y)\n  : es_suma_de_cuadrados (x * y) :=\nbegin\n  rcases hx with \u27e8a, b, hab : x = a^2 + b^2\u27e9,\n  rcases hy with \u27e8c, d, hcd : y = c^2 + d^2\u27e9,\n  have h1: x * y = (a*c - b*d)^2 + (a*d + b*c)^2,\n    calc x * y\n         = (a^2 + b^2) * (c^2 + d^2)     : by rw [hab, hcd]\n     ... = (a*c - b*d)^2 + (a*d + b*c)^2 : by ring,\n  have h2 : \u2203 f, x * y = (a*c - b*d)^2 + f^2,\n    by exact Exists.intro (a*d + b*c) h1,\n  have h3 : \u2203 e f, x * y = e^2 + f^2,\n    by exact Exists.intro (a*c - b*d) h2,\n  show es_suma_de_cuadrados (x * y),\n    by exact h3,\nend\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hx : es_suma_de_cuadrados x)\n  (hy : es_suma_de_cuadrados y)\n  : es_suma_de_cuadrados (x * y) :=\nbegin\n  rcases hx with \u27e8a, b, hab : x = a^2 + b^2\u27e9,\n  rcases hy with \u27e8c, d, hcd : y = c^2 + d^2\u27e9,\n  have h1: x * y = (a*c - b*d)^2 + (a*d + b*c)^2,\n    calc x * y\n         = (a^2 + b^2) * (c^2 + d^2)     : by rw [hab, hcd]\n     ... = (a*c - b*d)^2 + (a*d + b*c)^2 : by ring,\n  have h2 : \u2203 e f, x * y = e^2 + f^2,\n    by tauto,\n  show es_suma_de_cuadrados (x * y),\n    by exact h2,\nend\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hx : es_suma_de_cuadrados x)\n  (hy : es_suma_de_cuadrados y)\n  : es_suma_de_cuadrados (x * y) :=\nbegin\n  rcases hx with \u27e8a, b, hab\u27e9,\n  rcases hy with \u27e8c, d, hcd\u27e9,\n  rw [hab, hcd],\n  use [a*c - b*d, a*d + b*c],\n  ring,\nend\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hx : es_suma_de_cuadrados x)\n  (hy : es_suma_de_cuadrados y)\n  : es_suma_de_cuadrados (x * y) :=\nbegin\n  rcases hx with \u27e8a, b, rfl\u27e9,\n  rcases hy with \u27e8c, d, rfl\u27e9,\n  use [a*c - b*d, a*d + b*c],\n  ring\nend\n<\/pre>\n
Se puede interactuar con la prueba anterior en esta sesi\u00f3n con Lean<\/a>.<\/p>\n
Referencias<\/b><\/p>\n