La semana en Calculemus (12 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 tales que a+b=0, entonces -a=b
- 2. Si R es un anillo y a, b ∈ R tales que a+b=0, entonces a=-b
- 3. Si R es un anillo, entonces -0 = 0
- 4. Si R es un anillo y a ∈ R, entonces -(-a) = a
- 5. Si R es un anillo y a, b ∈ R, entonces a – b = a + -b
A continuación se muestran las soluciones.
1. Si R es un anillo y a, b ∈ R tales que a+b=0, entonces -a=b
Demostrar con Lean4 que si \(R\) es un anillo y \(a, b \in R\) tales que \(a + b = 0\) entonces \(-a = b\).
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 : R} example (h : a + b = 0) : -a = b := 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 cero]} \\
&= -a + (a + b) &&\text{[por hipótesis]} \\
&= b &&\text{[por cancelativa]}
\end{align}
2ª demostración en LN
Sumando \(-a\) a ambos lados de la hipótesis, se tiene
\[-a + (a + b) = -a + 0\]
El término de la izquierda se reduce a \(b\) (por la cancelativa) y el de la derecha a \(-a\) (por la suma con cero). Por tanto, se tiene
\[b = -a\]
Por la simetría de la igualdad, se tiene
\[-a = b\]
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 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable {a b : R} -- 1ª demostración (basada en la 1º en LN) example (h : a + b = 0) : -a = b := calc -a = -a + 0 := by rw [add_zero] _ = -a + (a + b) := by rw [h] _ = b := by rw [neg_add_cancel_left] -- 2ª demostración (basada en la 1º en LN) example (h : a + b = 0) : -a = b := calc -a = -a + 0 := by simp _ = -a + (a + b) := by rw [h] _ = b := by simp -- 3ª demostración (basada en la 2º en LN) example (h : a + b = 0) : -a = b := by have h1 : -a + (a + b) = -a + 0 := congrArg (HAdd.hAdd (-a)) h have h2 : -a + (a + b) = b := neg_add_cancel_left a b have h3 : -a + 0 = -a := add_zero (-a) rw [h2, h3] at h1 exact h1.symm -- 4ª demostración (con la librería mathlib) example (h : a + b = 0) : -a = b := neg_eq_iff_add_eq_zero.mpr 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.
2. Si R es un anillo y a, b ∈ R tales que a+b=0, entonces a=-b
Demostrar con Lean4 que si \(R\) es un anillo y \(a, b \in R\) tales que \(a + b = 0\) entonces \(a = -b\).
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 : R} example (h : a + b = 0) : a = -b := sorry |
Demostración en lenguaje natural
1ª demostración en LN
Por la siguiente cadena de igualdades
\begin{align}
a &= (a + b) + -b &&\text{[por la concelativa]} \\
&= 0 + -b &&\text{[por la hipótesis]} \\
&= -b &&\text{[por la suma con cero]}
\end{align}
2ª demostración en LN
Sumando \(-a\) a ambos lados de la hipótesis, se tiene
\[(a + b) + -b = 0 + -b\]
El término de la izquierda se reduce a \(a\) (por la cancelativa) y el de la derecha a \(-b\) (por la suma con cero). Por tanto, se tiene
\[a = -b\]
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 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable {a b : R} -- 1ª demostración (basada en la 1ª en LN) example (h : a + b = 0) : a = -b := calc a = (a + b) + -b := by rw [add_neg_cancel_right] _ = 0 + -b := by rw [h] _ = -b := by rw [zero_add] -- 2ª demostración (basada en la 1ª en LN) example (h : a + b = 0) : a = -b := calc a = (a + b) + -b := by simp _ = 0 + -b := by rw [h] _ = -b := by simp -- 3ª demostración (basada en la 1ª en LN) example (h : a + b = 0) : a = -b := by have h1 : (a + b) + -b = 0 + -b := by rw [h] have h2 : (a + b) + -b = a := add_neg_cancel_right a b have h3 : 0 + -b = -b := zero_add (-b) rwa [h2, h3] at h1 -- 4ª demostración example (h : a + b = 0) : a = -b := add_eq_zero_iff_eq_neg.mp 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, entonces -0 = 0
Demostrar con Lean4 que si \(R\) es un anillo, entonces \(-0 = 0\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] example : (-0 : R) = 0 := sorry |
Demostraciones en lenguaje natural (LN)
1ª demostración en LN
Por la suma con cero se tiene
\[0 + 0 = 0\]
Aplicándole la propiedad
\[\forall a b ∈ R, a + b = 0 \to -a = b\]
se obtiene
\[-0 = 0\]
2ª demostración en LN
Puesto que
\[\forall a b ∈ R, a + b = 0 \to -a = b\]
basta demostrar que
\[0 + 0 = 0\]
que es cierta por la suma con cero.
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 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] -- 1ª demostración (basada en la 1ª en LN) example : (-0 : R) = 0 := by have h1 : (0 : R) + 0 = 0 := add_zero 0 show (-0 : R) = 0 exact neg_eq_of_add_eq_zero_left h1 -- 2ª demostración (basada en la 2ª en LN) example : (-0 : R) = 0 := by apply neg_eq_of_add_eq_zero_left rw [add_zero] -- 3ª demostración example : (-0 : R) = 0 := neg_zero -- 4ª demostración example : (-0 : R) = 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.
4. Si R es un anillo y a ∈ R, entonces -(-a) = a
Demostrar con Lean4 que si \(R\) es un anillo y \(a \in R\), entonces
\(-(-a) = a\).
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) = a := sorry |
Demostración en lenguaje natural
Es consecuencia de las siguiente propiedades demostradas en ejercicios anteriores:
\begin{align}
&\forall a \ b \in R, a + b = 0 \to -a = b \\
&\forall a \in R, -a + a = 0
\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 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable {a : R} -- 1ª demostración example : -(-a) = a := by have h1 : -a + a = 0 := add_left_neg a show -(-a) = a exact neg_eq_of_add_eq_zero_right h1 -- 2ª demostración example : -(-a) = a := by apply neg_eq_of_add_eq_zero_right rw [add_left_neg] -- 3ª demostración example : -(-a) = a := neg_neg a -- 4ª demostración example : -(-a) = 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.
5. Si R es un anillo y a, b ∈ R, entonces a – b = a + -b
Demostrar con Lean4 que si \(R\) es un anillo y \(a, b \in R\), entonces
\[a – b = a + -b\]
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 = a + -b := sorry |
Demostración en lenguaje natural
Por la definición de la resta.
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 |
import Mathlib.Algebra.Ring.Defs variable {R : Type _} [Ring R] variable (a b : R) example : a - b = a + -b := -- by exact? sub_eq_add_neg a b |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 12.