Demostrar con Lean4 que si R es un anillo y a, b, c \u2208 R tales que<\/p>\n
\r\n a + b = c + b\r\n<\/pre>\nentonces<\/p>\n
\r\n a = c\r\n<\/pre>\nPara ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Algebra.Ring.Defs\r\nimport Mathlib.Tactic\r\n\r\nvariable {R : Type _} [Ring R]\r\nvariable {a b c : R}\r\n\r\nexample\r\n (h : a + b = c + b)\r\n : a = c :=\r\nsorry\r\n<\/pre>\n<\/p>\n
Demostraciones en lenguaje natural (LN<\/b><\/p>\n\n
1\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Por la siguiente cadena de igualdades
\n\\begin{align}
\n a &= a + 0 &&\\text{[por suma con cero]} \\\\
\n &= a + (b + -b) &&\\text{[por suma con opuesto]} \\\\
\n &= (a + b) + -b &&\\text{[por asociativa]} \\\\
\n &= (c + b) + -b &&\\text{[por hip\u00f3tesis]} \\\\
\n &= c + (b + -b) &&\\text{[por asociativa]} \\\\
\n &= c + 0 &&\\text{[por suma con opuesto]} \\\\
\n &= c &&\\text{[por suma con cero]}
\n\\end{align}<\/p>\n
2\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Por la siguiente cadena de igualdades
\n\\begin{align}
\n a &= (a + b) + -b \\\\
\n &= (c + b) + -b &&\\text{[por hip\u00f3tesis]} \\\\
\n &= c
\n\\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Algebra.Ring.Defs\r\nimport Mathlib.Tactic\r\n\r\nvariable {R : Type _} [Ring R]\r\nvariable {a b c : R}\r\n\r\n-- 1\u00aa demostraci\u00f3n con Lean4\r\n-- =========================\r\n\r\nexample\r\n (h : a + b = c + b)\r\n : a = c :=\r\ncalc\r\n a = a + 0 := by rw [add_zero]\r\n _ = a + (b + -b) := by rw [add_right_neg]\r\n _ = (a + b) + -b := by rw [add_assoc]\r\n _ = (c + b) + -b := by rw [h]\r\n _ = c + (b + -b) := by rw [\u2190 add_assoc]\r\n _ = c + 0 := by rw [\u2190 add_right_neg]\r\n _ = c := by rw [add_zero]\r\n\r\n-- 2\u00aa demostraci\u00f3n con Lean4\r\n-- =========================\r\n\r\nexample\r\n (h : a + b = c + b)\r\n : a = c :=\r\ncalc\r\n a = (a + b) + -b := (add_neg_cancel_right a b).symm\r\n _ = (c + b) + -b := by rw [h]\r\n _ = c := add_neg_cancel_right c b\r\n\r\n-- 3\u00aa demostraci\u00f3n con Lean4\r\n-- =========================\r\n\r\nexample\r\n (h : a + b = c + b)\r\n : a = c :=\r\nby\r\n rw [\u2190 add_neg_cancel_right a b]\r\n rw [h]\r\n rw [add_neg_cancel_right]\r\n\r\n-- 4\u00aa demostraci\u00f3n con Lean4\r\n-- =========================\r\n\r\nexample\r\n (h : a + b = c + b)\r\n : a = c :=\r\nby\r\n rw [\u2190 add_neg_cancel_right a b, h, add_neg_cancel_right]\r\n\r\n-- 5\u00aa demostraci\u00f3n con Lean4\r\n-- =========================\r\n\r\nexample\r\n (h : a + b = c + b)\r\n : a = c :=\r\nadd_right_cancel h\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