La semana en Calculemus (5 de agosto de 2023)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. Si R es un anillo y a, b ∈ R, entonces (a + b) + -b = a
- 2. Si R es un anillo y a, b, c ∈ R tales que a+b=a+c, entonces b=c
- 3. Si R es un anillo y a, b, c ∈ R tales que a+b=c+b, entonces a=c
- 4. Si R es un anillo y a ∈ R, entonces a.0 = 0
- 5. Si R es un anillo y a ∈ R, entonces 0.a = 0
A continuación se muestran las soluciones.
1. Si R es un anillo y a, b ∈ R, entonces (a + b) + -b = a
En Lean4, se declara que R es un anillo mediante la expresión
|
1 |
variable {R : Type _} [Ring R] |
Como consecuencia, se tiene los siguientes axiomas
|
1 2 3 4 5 6 7 8 9 |
add_assoc : ∀ a b c : R, (a + b) + c = a + (b + c) add_comm : ∀ a b : R, a + b = b + a zero_add : ∀ a : R, 0 + a = a add_left_neg : ∀ a : R, -a + a = 0 mul_assoc : ∀ a b c : R, a * b * c = a * (b * c) mul_one : ∀ a : R, a * 1 = a one_mul : ∀ a : R, 1 * a = a mul_add : ∀ a b c : R, a * (b + c) = a * b + a * c add_mul : ∀ a b c : R, (a + b) * c = a * c + b * c |
Demostrar que si \(R\) es un anillo, entonces
\[\forall a, b \in R, (a + b) + -b = a\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Algebra.Ring.Defs variable {R : Type _} [Ring R] variable (a b : R) example : (a + b) + -b = a := sorry |
Demostración en lenguaje natural
Por la siguiente cadena de igualdades
\begin{align}
(a + b) + -b &= a + (b + -b) &&\text{[por la asociativa]} \\
&= a + 0 &&\text{[por suma con opuesto]} \\
&= a &&\text{[por suma con cero]}
\end{align}
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 |
import Mathlib.Algebra.Ring.Defs variable {R : Type _} [Ring R] variable (a b : R) -- 1ª demostración example : (a + b) + -b = a := calc (a + b) + -b = a + (b + -b) := by rw [add_assoc] _ = a + 0 := by rw [add_right_neg] _ = a := by rw [add_zero] -- 2ª demostración example : (a + b) + -b = a := by rw [add_assoc] rw [add_right_neg] rw [add_zero] -- 3ª demostración example : (a + b) + -b = a := by rw [add_assoc, add_right_neg, add_zero] -- 4ª demostración example : (a + b) + -b = a := add_neg_cancel_right a b -- 5ª demostración example : (a + b) + -b = a := add_neg_cancel_right _ _ -- 6ª demostración example : (a + b) + -b = a := by simp |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 11.
2. Si R es un anillo y a, b, c ∈ R tales que a+b=a+c, entonces b=c
Demostrar con Lean4 que si \(R\) es un anillo y \(a, b, c \in R\) tales que \(a + b = a + c\), entonces \(b = c\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable {a b c : R} example (h : a + b = a + c) : b = c := sorry |
Demostración en lenguaje natural (LN)
1ª demostración en LN
Por la siguiente cadena de igualdades
\begin{align}
b &= 0 + b &&\text{[por suma con cero]} \\
&= (-a + a) + b &&\text{[por suma con opuesto]} \\
&= -a + (a + b) &&\text{[por asociativa]} \\
&= -a + (a + c) &&\text{[por hipótesis]} \\
&= (-a + a) + c &&\text{[por asociativa]} \\
&= 0 + c &&\text{[por suma con opuesto]} \\
&= c &&\text{[por suma con cero]}
\end{align}
2ª demostración en LN
Por la siguiente cadena de implicaciones
\begin{align}
a + b = a + c
&\Longrightarrow -a + (a + b) = -a + (a + c) &&\text{[sumando -a]} \\
&\Longrightarrow (-a + a) + b = (-a + a) + c &&\text{[por la asociativa]} \\
&\Longrightarrow 0 + b = 0 + b &&\text{[suma con opuesto]} \\
&\Longrightarrow b = c &&\text{[suma con cero]}
\end{align}
3ª demostración en LN
Por la siguiente cadena de igualdades
\begin{align}
b &= -a + (a + b) \\
&= -a + (a + c) &&\text{[por la hipótesis]} \\
&= c
\end{align}
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable {a b c : R} -- 1ª demostración example (h : a + b = a + c) : b = c := calc b = 0 + b := by rw [zero_add] _ = (-a + a) + b := by rw [add_left_neg] _ = -a + (a + b) := by rw [add_assoc] _ = -a + (a + c) := by rw [h] _ = (-a + a) + c := by rw [←add_assoc] _ = 0 + c := by rw [add_left_neg] _ = c := by rw [zero_add] -- 2ª demostración example (h : a + b = a + c) : b = c := by have h1 : -a + (a + b) = -a + (a + c) := congrArg (HAdd.hAdd (-a)) h clear h rw [← add_assoc] at h1 rw [add_left_neg] at h1 rw [zero_add] at h1 rw [← add_assoc] at h1 rw [add_left_neg] at h1 rw [zero_add] at h1 exact h1 -- 3ª demostración example (h : a + b = a + c) : b = c := calc b = -a + (a + b) := by rw [neg_add_cancel_left a b] _ = -a + (a + c) := by rw [h] _ = c := by rw [neg_add_cancel_left] -- 4ª demostración example (h : a + b = a + c) : b = c := by rw [← neg_add_cancel_left a b] rw [h] rw [neg_add_cancel_left] -- 5ª demostración example (h : a + b = a + c) : b = c := by rw [← neg_add_cancel_left a b, h, neg_add_cancel_left] -- 6ª demostración example (h : a + b = a + c) : b = c := add_left_cancel h |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 11.
3. Si R es un anillo y a, b, c ∈ R tales que a+b=c+b, entonces a=c
Demostrar con Lean4 que si \(R\) es un anillo y \(a, b, c \in R\) tales que \(a + b = c + b\), entonces \(a = c\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable {a b c : R} example (h : a + b = c + b) : a = c := sorry |
Demostraciones en lenguaje natural (LN
1ª demostración en LN
Por la siguiente cadena de igualdades
\begin{align}
a &= a + 0 &&\text{[por suma con cero]} \\
&= a + (b + -b) &&\text{[por suma con opuesto]} \\
&= (a + b) + -b &&\text{[por asociativa]} \\
&= (c + b) + -b &&\text{[por hipótesis]} \\
&= c + (b + -b) &&\text{[por asociativa]} \\
&= c + 0 &&\text{[por suma con opuesto]} \\
&= c &&\text{[por suma con cero]}
\end{align}
2ª demostración en LN
Por la siguiente cadena de igualdades
\begin{align}
a &= (a + b) + -b \\
&= (c + b) + -b &&\text{[por hipótesis]} \\
&= c
\end{align}
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable {a b c : R} -- 1ª demostración con Lean4 -- ========================= example (h : a + b = c + b) : a = c := calc a = a + 0 := by rw [add_zero] _ = a + (b + -b) := by rw [add_right_neg] _ = (a + b) + -b := by rw [add_assoc] _ = (c + b) + -b := by rw [h] _ = c + (b + -b) := by rw [← add_assoc] _ = c + 0 := by rw [← add_right_neg] _ = c := by rw [add_zero] -- 2ª demostración con Lean4 -- ========================= example (h : a + b = c + b) : a = c := calc a = (a + b) + -b := (add_neg_cancel_right a b).symm _ = (c + b) + -b := by rw [h] _ = c := add_neg_cancel_right c b -- 3ª demostración con Lean4 -- ========================= example (h : a + b = c + b) : a = c := by rw [← add_neg_cancel_right a b] rw [h] rw [add_neg_cancel_right] -- 4ª demostración con Lean4 -- ========================= example (h : a + b = c + b) : a = c := by rw [← add_neg_cancel_right a b, h, add_neg_cancel_right] -- 5ª demostración con Lean4 -- ========================= example (h : a + b = c + b) : a = c := add_right_cancel h |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 11.
4. Si R es un anillo y a ∈ R, entonces a.0 = 0
Demostrar con Lean4 que si \(R\) es un anillo y \(a \in R\), entonces \(a·0 = 0\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable (a : R) example : a * 0 = 0 := sorry |
Demostración en lenguaje natural
Basta aplicar la propiedad cancelativa a
[a.0 + a.0 = a.0 + 0]
que se demuestra mediante la siguiente cadena de igualdades
\begin{align}
a.0 + a.0 &= a.(0 + 0) &&\text{[por la distributiva]} \\
&= a.0 &&\text{[por suma con cero]} \\
&= a.0 + 0 &&\text{[por suma con cero]}
\end{align}
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable (a : R) -- 1ª demostración -- =============== example : a * 0 = 0 := by have h : a * 0 + a * 0 = a * 0 + 0 := calc a * 0 + a * 0 = a * (0 + 0) := by rw [mul_add a 0 0] _ = a * 0 := by rw [add_zero 0] _ = a * 0 + 0 := by rw [add_zero (a * 0)] rw [add_left_cancel h] -- 2ª demostración -- =============== example : a * 0 = 0 := by have h : a * 0 + a * 0 = a * 0 + 0 := calc a * 0 + a * 0 = a * (0 + 0) := by rw [← mul_add] _ = a * 0 := by rw [add_zero] _ = a * 0 + 0 := by rw [add_zero] rw [add_left_cancel h] -- 3ª demostración -- =============== example : a * 0 = 0 := by have h : a * 0 + a * 0 = a * 0 + 0 := by rw [← mul_add, add_zero, add_zero] rw [add_left_cancel h] -- 4ª demostración -- =============== example : a * 0 = 0 := by have : a * 0 + a * 0 = a * 0 + 0 := calc a * 0 + a * 0 = a * (0 + 0) := by simp _ = a * 0 := by simp _ = a * 0 + 0 := by simp simp -- 5ª demostración -- =============== example : a * 0 = 0 := mul_zero a -- 6ª demostración -- =============== example : a * 0 = 0 := by simp |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 11.
5. Si R es un anillo y a ∈ R, entonces 0.a = 0
Demostrar con Lean4 que si \(R\) es un anillo y \(a \in R\), entonces \(0·a = 0\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable (a : R) example : 0 * a = 0 := sorry |
Demostración en lenguaje natural
Basta aplicar la propiedad cancelativa a
\[0.a + 0.a = 0.a + 0\]
que se demuestra mediante la siguiente cadena de igualdades
\begin{align}
0.a + 0.a &= (0 + 0).a &&\text{[por la distributiva]} \\
&= 0.a &&\text{[por suma con cero]} \\
&= 0.a + 0 &&\text{[por suma con cero]}
\end{align}
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable (a : R) -- 1ª demostración example : 0 * a = 0 := by have h : 0 * a + 0 * a = 0 * a + 0 := calc 0 * a + 0 * a = (0 + 0) * a := by rw [add_mul] _ = 0 * a := by rw [add_zero] _ = 0 * a + 0 := by rw [add_zero] rw [add_left_cancel h] -- 2ª demostración example : 0 * a = 0 := by have h : 0 * a + 0 * a = 0 * a + 0 := by rw [←add_mul, add_zero, add_zero] rw [add_left_cancel h] -- 3ª demostración example : 0 * a = 0 := by have : 0 * a + 0 * a = 0 * a + 0 := calc 0 * a + 0 * a = (0 + 0) * a := by simp _ = 0 * a := by simp _ = 0 * a + 0 := by simp simp -- 4ª demostración example : 0 * a = 0 := by have : 0 * a + 0 * a = 0 * a + 0 := by simp simp -- 5ª demostración example : 0 * a = 0 := by simp -- 6ª demostración example : 0 * a = 0 := zero_mul a |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 11.