Demostrar en Lean4 que si R es un anillo, entonces<\/p>\n
\r\n \u2200 a, b : R, -a + (a + b) = b\r\n<\/pre>\nPara ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Algebra.Ring.Defs\r\n\r\nvariable {R : Type _} [Ring R]\r\nvariable (a b : R)\r\n\r\nexample : -a + (a + b) = b :=\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 + (a + b) &= (-a + a) + b &&\\text{[por la asociativa]} \\\\
\n &= 0 + b &&\\text{[por inverso por la izquierda]} \\\\
\n &= b &&\\text{[por cero por la izquierda]}
\n\\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample : -a + (a + b) = b :=\r\ncalc -a + (a + b) = (-a + a) + b := by rw [\u2190 add_assoc]\r\n _ = 0 + b := by rw [add_left_neg]\r\n _ = b := by rw [zero_add]\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample : -a + (a + b) = b :=\r\nby\r\n rw [\u2190add_assoc]\r\n rw [add_left_neg]\r\n rw [zero_add]\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample : -a + (a + b) = b :=\r\nby rw [\u2190add_assoc, add_left_neg, zero_add]\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample : -a + (a + b) = b :=\r\nby exact neg_add_cancel_left a b\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample : -a + (a + b) = b :=\r\n neg_add_cancel_left a b\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nexample : -a + (a + b) = b :=\r\nby simp\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