Demostrar con Lean4 que si a, b, c y d son n\u00fameros reales tales<\/p>\n
\r\n c = b * a - d\r\n d = a * b\r\n<\/pre>\nentonces<\/p>\n
\r\n c = 0\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\nexample\r\n (a b c d : \u211d)\r\n (h1 : c = b * a - d)\r\n (h2 : d = a * b)\r\n : c = 0 :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nPor la siguiente cadena de igualdades
\n\\[
\n\\begin{align}
\n c &= ba – d &&\\text{[por la primera hip\u00f3tesis]} \\\\
\n &= ab – d &&\\text{[por la conmutativa]} \\\\
\n &= ab – ab &&\\text{[por la segunda hip\u00f3tesis]} \\\\
\n &= 0
\n\\end{align}
\n\\]<\/p>\n
Demostraciones con Lean<\/b><\/p>\n\r\nimport Mathlib.Data.Real.Basic\r\nimport Mathlib.Tactic\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n (a b c d : \u211d)\r\n (h1 : c = b * a - d)\r\n (h2 : d = a * b)\r\n : c = 0 :=\r\ncalc\r\n c = b * a - d := by rw [h1]\r\n _ = a * b - d := by rw [mul_comm]\r\n _ = a * b - a * b := by rw [h2]\r\n _ = 0 := by rw [sub_self]\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n (a b c d : \u211d)\r\n (h1 : c = b * a - d)\r\n (h2 : d = a * b)\r\n : c = 0 :=\r\nby\r\n rw [h1]\r\n rw [mul_comm]\r\n rw [h2]\r\n rw [sub_self]\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample\r\n (a b c d : \u211d)\r\n (h1 : c = b * a - d)\r\n (h2 : d = a * b)\r\n : c = 0 :=\r\nby\r\n rw [h1, mul_comm, h2, sub_self]\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