Identidad de Brahmagupta-Fibonacci
Demostrar la identidad de Brahmagupta-Fibonacci
1 |
(a² + b²)(c² + d²) = (ac - bd)² + (ad + bc)² |
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 |
import data.real.basic variables (a b c d : ℝ) example : (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 := sorry |
[expand title=»Soluciones con Lean»]
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 |
import data.real.basic variables (a b c d : ℝ) -- 1ª demostración example : (a^2 + b^2) * (c^2 + d^2) = (a*c - 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) ... = (a^2*c^2 + a^2*d^2) + b^2 * (c^2 + d^2) : congr_arg2 (+) (left_distrib (a^2) (c^2) (d^2)) rfl ... = (a^2*c^2 + a^2*d^2) + (b^2*c^2 + b^2*d^2) : congr_arg2 (+) rfl (left_distrib (b^2) (c^2) (d^2)) ... = ((a*c)^2 + (b*d)^2) + ((a*d)^2 + (b*c)^2) : by ring ... = ((a*c)^2 - 2*a*c*b*d + (b*d)^2) + ((a*d)^2 + 2*a*d*b*c + (b*c)^2) : by ring ... = (a*c - b*d)^2 + (a*d + b*c)^2 : by ring -- 2ª demostración example : (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 := by ring |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]
[expand title=»Soluciones con Isabelle/HOL»]
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 |
theory "Identidad_de_Brahmagupta-Fibonacci" imports Main HOL.Real begin (* 1ª demostración *) lemma fixes a b c d :: real shows "(a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2" proof - have "(a^2 + b^2) * (c^2 + d^2) = a^2 * (c^2 + d^2) + b^2 * (c^2 + d^2)" by (simp only: distrib_right) also have "… = (a^2*c^2 + a^2*d^2) + b^2 * (c^2 + d^2)" by (simp only: distrib_left) also have "… = (a^2*c^2 + a^2*d^2) + (b^2*c^2 + b^2*d^2)" by (simp only: distrib_left) also have "… = ((a*c)^2 + (b*d)^2) + ((a*d)^2 + (b*c)^2)" by algebra also have "… = ((a*c)^2 - 2*a*c*b*d + (b*d)^2) + ((a*d)^2 + 2*a*d*b*c + (b*c)^2)" by algebra also have "… = (a*c - b*d)^2 + (a*d + b*c)^2" by algebra finally show "(a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2" . qed (* 2ª demostración *) lemma fixes a b c d :: real shows "(a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2" by algebra end |
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]