{"id":1291,"date":"2023-07-24T06:00:39","date_gmt":"2023-07-24T04:00:39","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1291"},"modified":"2023-07-21T18:31:22","modified_gmt":"2023-07-21T16:31:22","slug":"24-jul-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/24-jul-23\/","title":{"rendered":"Si c = da+b y b = ad, entonces c = 2ad"},"content":{"rendered":"

Demostrar con Lean4 que si a, b, c y d son n\u00fameros reales tales que<\/p>\n

\r\n   c = d * a + b\r\n   b = a * d\r\n<\/pre>\n
entonces<\/p>\n
\r\n   c = 2 * a * d\r\n<\/pre>\n
Para 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 c d : \u211d)\r\n\r\nexample\r\n  (h1 : c = d * a + b)\r\n  (h2 : b = a * d)\r\n  : c = 2 * a * d :=\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   c &= da + b     &&\\text{[por la primera hip\u00f3tesis]} \\\\
\n     &= da + ad    &&\\text{[por la segunda hip\u00f3tesis]} \\\\
\n     &= ad + ad    &&\\text{[por la conmutativa]} \\\\
\n     &= 2(ad)      &&\\text{[por la def. de doble]} \\\\
\n     &= 2ad        &&\\text{[por la asociativa]}
\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 c d : \u211d)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n  (h1 : c = d * a + b)\r\n  (h2 : b = a * d)\r\n  : c = 2 * a * d :=\r\ncalc\r\n  c = d * a + b     := by rw [h1]\r\n  _ = d * a + a * d := by rw [h2]\r\n  _ = a * d + a * d := by rw [mul_comm d a]\r\n  _ = 2 * (a * d)   := by rw [\u2190 two_mul (a * d)]\r\n  _ = 2 * a * d     := by rw [mul_assoc]\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n  (h1 : c = d * a + b)\r\n  (h2 : b = a * d)\r\n  : c = 2 * a * d :=\r\nby\r\n  rw [h2] at h1\r\n  clear h2\r\n  rw [mul_comm d a] at h1\r\n  rw [\u2190 two_mul (a*d)] at h1\r\n  rw [\u2190 mul_assoc 2 a d] at h1\r\n  exact h1\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample\r\n  (h1 : c = d * a + b)\r\n  (h2 : b = a * d)\r\n  : c = 2 * a * d :=\r\nby rw [h1, h2, mul_comm d a, \u2190 two_mul (a * d), mul_assoc]\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample\r\n  (h1 : c = d * a + b)\r\n  (h2 : b = a * d)\r\n  : c = 2 * a * d :=\r\nby\r\n  rw [h1]\r\n  rw [h2]\r\n  ring\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample\r\n  (h1 : c = d * a + b)\r\n  (h2 : b = a * d)\r\n  : c = 2 * a * d :=\r\nby\r\n  rw [h1, h2]\r\n  ring\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nexample\r\n  (h1 : c = d * a + b)\r\n  (h2 : b = a * d)\r\n  : c = 2 * a * d :=\r\nby rw [h1, h2] ; ring\r\n\r\n-- 7\u00aa demostraci\u00f3n\r\nexample\r\n  (h1 : c = d * a + b)\r\n  (h2 : b = a * d)\r\n  : c = 2 * a * d :=\r\nby linarith\r\n<\/pre>\n
Demostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
Referencias<\/b><\/p>\n