Demostrar con Lean4 que si a y b son n\u00fameros reales, entonces<\/p>\n
\r\n (a + b) * (a - b) = a^2 - b^2\r\n<\/pre>\nPara ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Data.Real.Basic\r\nimport Mathlib.Tactic\r\n\r\nvariable (a b : \u211d)\r\n\r\nexample : (a + b) * (a - b) = a^2 - b^2 :=\r\nsorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nPor la siguiente cadena de igualdades:
\n\\begin{align}
\n(a + b)(a – b)
\n&= a(a – b) + b(a – b) &&\\text{[por la distributiva]} \\\\
\n&= (aa – ab) + b(a – b) &&\\text{[por la distributiva]} \\\\
\n&= (a^2 – ab) + b(a – b) &&\\text{[por def. de cuadrado]} \\\\
\n&= (a^2 – ab) + (ba – bb) &&\\text{[por la distributiva]} \\\\
\n&= (a^2 – ab) + (ba – b^2) &&\\text{[por def. de cuadrado]} \\\\
\n&= (a^2 + -(ab)) + (ba – b^2) &&\\text{[por def. de resta]} \\\\
\n&= a^2 + (-(ab) + (ba – b^2)) &&\\text{[por la asociativa]} \\\\
\n&= a^2 + (-(ab) + (ba + -b^2)) &&\\text{[por def. de resta]} \\\\
\n&= a^2 + ((-(ab) + ba) + -b^2) &&\\text{[por la asociativa]} \\\\
\n&= a^2 + ((-(ab) + ab) + -b^2) &&\\text{[por la conmutativa]} \\\\
\n&= a^2 + (0 + -b^2) &&\\text{[por def. de opuesto]} \\\\
\n&= (a^2 + 0) + -b^2 &&\\text{[por asociativa]} \\\\
\n&= a^2 + -b^2 &&\\text{[por def. de cero]} \\\\
\n&= a^2 – b^2 &&\\text{[por def. de resta]}
\n\\end{align}<\/p>\n
Demostraciones con Lean<\/b><\/p>\n\r\nimport Mathlib.Data.Real.Basic\r\nimport Mathlib.Tactic\r\n\r\nvariable (a b : \u211d)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : (a + b) * (a - b) = a^2 - b^2 :=\r\ncalc\r\n (a + b) * (a - b)\r\n = a * (a - b) + b * (a - b) := by rw [add_mul]\r\n _ = (a * a - a * b) + b * (a - b) := by rw [mul_sub]\r\n _ = (a^2 - a * b) + b * (a - b) := by rw [\u2190 pow_two]\r\n _ = (a^2 - a * b) + (b * a - b * b) := by rw [mul_sub]\r\n _ = (a^2 - a * b) + (b * a - b^2) := by rw [\u2190 pow_two]\r\n _ = (a^2 + -(a * b)) + (b * a - b^2) := by ring\r\n _ = a^2 + (-(a * b) + (b * a - b^2)) := by rw [add_assoc]\r\n _ = a^2 + (-(a * b) + (b * a + -b^2)) := by ring\r\n _ = a^2 + ((-(a * b) + b * a) + -b^2) := by rw [\u2190 add_assoc\r\n (-(a * b)) (b * a) (-b^2)]\r\n _ = a^2 + ((-(a * b) + a * b) + -b^2) := by rw [mul_comm]\r\n _ = a^2 + (0 + -b^2) := by rw [neg_add_self (a * b)]\r\n _ = (a^2 + 0) + -b^2 := by rw [\u2190 add_assoc]\r\n _ = a^2 + -b^2 := by rw [add_zero]\r\n _ = a^2 - b^2 := by linarith\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : (a + b) * (a - b) = a^2 - b^2 :=\r\ncalc\r\n (a + b) * (a - b)\r\n = a * (a - b) + b * (a - b) := by ring\r\n _ = (a * a - a * b) + b * (a - b) := by ring\r\n _ = (a^2 - a * b) + b * (a - b) := by ring\r\n _ = (a^2 - a * b) + (b * a - b * b) := by ring\r\n _ = (a^2 - a * b) + (b * a - b^2) := by ring\r\n _ = (a^2 + -(a * b)) + (b * a - b^2) := by ring\r\n _ = a^2 + (-(a * b) + (b * a - b^2)) := by ring\r\n _ = a^2 + (-(a * b) + (b * a + -b^2)) := by ring\r\n _ = a^2 + ((-(a * b) + b * a) + -b^2) := by ring\r\n _ = a^2 + ((-(a * b) + a * b) + -b^2) := by ring\r\n _ = a^2 + (0 + -b^2) := by ring\r\n _ = (a^2 + 0) + -b^2 := by ring\r\n _ = a^2 + -b^2 := by ring\r\n _ = a^2 - b^2 := by ring\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : (a + b) * (a - b) = a^2 - b^2 :=\r\nby ring\r\n\r\n-- 4\u00aa demostraci\u00f3n (por reescritura usando el lema anterior)\r\n-- =========================================================\r\n\r\n-- El lema anterior es\r\nlemma aux : (a + b) * (c + d) = a * c + a * d + b * c + b * d :=\r\nby ring\r\n\r\n-- La demostraci\u00f3n es\r\nexample : (a + b) * (a - b) = a^2 - b^2 :=\r\nby\r\n rw [sub_eq_add_neg]\r\n rw [aux]\r\n rw [mul_neg]\r\n rw [add_assoc (a * a)]\r\n rw [mul_comm b a]\r\n rw [neg_add_self]\r\n rw [add_zero]\r\n rw [\u2190 pow_two]\r\n rw [mul_neg]\r\n rw [\u2190 pow_two]\r\n rw [\u2190 sub_eq_add_neg]\r\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n