{"id":1418,"date":"2023-08-01T06:00:53","date_gmt":"2023-08-01T04:00:53","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1418"},"modified":"2023-07-27T09:16:42","modified_gmt":"2023-07-27T07:16:42","slug":"01-ago-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/01-ago-23\/","title":{"rendered":"Si R es un anillo y a, b, c \u2208 R tales que a+b=a+c, entonces b=c"},"content":{"rendered":"

Demostrar con Lean4 que si R es un anillo y a, b, c \u2208 R tales que<\/p>\n

\r\n   a + b = a + c\r\n<\/pre>\n
entonces<\/p>\n
\r\n   b = c\r\n<\/pre>\n
Para 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 = a + c)\r\n  : b = c :=\r\nsorry\r\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural (LN)<\/b><\/p>\n

\n1\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Por la siguiente cadena de igualdades
\n\\begin{align}
\nb &= 0 + b           &&\\text{[por suma con cero]} \\\\
\n  &= (-a + a) + b    &&\\text{[por suma con opuesto]} \\\\
\n  &= -a + (a + b)    &&\\text{[por asociativa]} \\\\
\n  &= -a + (a + c)    &&\\text{[por hip\u00f3tesis]} \\\\
\n  &= (-a + a) + c    &&\\text{[por asociativa]} \\\\
\n  &= 0 + c           &&\\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 implicaciones
\n\\begin{align}
\na + b = a + c
\n&\\Longrightarrow -a + (a + b) = -a + (a + c)     &&\\text{[sumando -a]} \\\\
\n&\\Longrightarrow  (-a + a) + b = (-a + a) + c    &&\\text{[por la asociativa]} \\\\
\n&\\Longrightarrow  0 + b = 0 + b                  &&\\text{[suma con opuesto]} \\\\
\n&\\Longrightarrow  b = c                          &&\\text{[suma con cero]}
\n\\end{align}<\/p>\n
3\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Por la siguiente cadena de igualdades
\n\\begin{align}
\nb &= -a + (a + b)   \\\\
\n  &= -a + (a + c)   &&\\text{[por la 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\r\nexample\r\n  (h : a + b = a + c)\r\n  : b = c :=\r\ncalc\r\n  b = 0 + b        := by rw [zero_add]\r\n  _ = (-a + a) + b := by rw [add_left_neg]\r\n  _ = -a + (a + b) := by rw [add_assoc]\r\n  _ = -a + (a + c) := by rw [h]\r\n  _ = (-a + a) + c := by rw [\u2190add_assoc]\r\n  _ = 0 + c        := by rw [add_left_neg]\r\n  _ = c            := by rw [zero_add]\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n  (h : a + b = a + c)\r\n  : b = c :=\r\nby\r\n  have h1 : -a + (a + b) = -a + (a + c) :=\r\n    congrArg (HAdd.hAdd (-a)) h\r\n  clear h\r\n  rw [\u2190 add_assoc] at h1\r\n  rw [add_left_neg] at h1\r\n  rw [zero_add] at h1\r\n  rw [\u2190 add_assoc] at h1\r\n  rw [add_left_neg] at h1\r\n  rw [zero_add] at h1\r\n  exact h1\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample\r\n  (h : a + b = a + c)\r\n  : b = c :=\r\ncalc\r\n  b = -a + (a + b) := by rw [neg_add_cancel_left a b]\r\n  _ = -a + (a + c) := by rw [h]\r\n  _ = c            := by rw [neg_add_cancel_left]\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample\r\n  (h : a + b = a + c)\r\n  : b = c :=\r\nby\r\n  rw [\u2190 neg_add_cancel_left a b]\r\n  rw [h]\r\n  rw [neg_add_cancel_left]\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample\r\n  (h : a + b = a + c)\r\n  : b = c :=\r\nby\r\n  rw [\u2190 neg_add_cancel_left a b, h, neg_add_cancel_left]\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nexample\r\n  (h : a + b = a + c)\r\n  : b = c :=\r\nadd_left_cancel h\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