La semana en Calculemus (22 de julio de 2023)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. Si bc = ef, entonces ((ab)c)d = ((ae)f)d
- 2. Si c = ba-d y d = ab, entonces c = 0
- 3. (a+b)(a+b) = aa+2ab+bb
- 4. (a+b)(c+d) = ac+ad+bc+bd
- 5. (a+b)(a-b) = a²-b²
A continuación se muestran las soluciones.
1. Si bc = ef, entonces ((ab)c)d = ((ae)f)d
Demostrar con Lean4 que si bc = ef, entonces ((ab)c)d = ((ae)f)d.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic example (a b c d e f : ℝ) (h : b * c = e * f) : ((a * b) * c) * d = ((a * e) * f) * d := by sorry |
Demostración en lenguaje natural
Por la siguiente cadena de igualdades
\begin{align}
((ab)c)d
&= (a(bc))d &&\text{[por la asociativa]} \\
&= (a(ef))d &&\text{[por la hipótesis]} \\
&= ((ae)f)d &&\text{[por la asociativa]}
\end{align}
Demostraciones con Lean
|
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 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic -- 1ª demostración example (a b c d e f : ℝ) (h : b * c = e * f) : ((a * b) * c) * d = ((a * e) * f) * d := calc ((a * b) * c) * d = (a * (b * c)) * d := by rw [mul_assoc a] _ = (a * (e * f)) * d := by rw [h] _ = ((a * e) * f) * d := by rw [←mul_assoc a] -- 2ª demostración example (a b c d e f : ℝ) (h : b * c = e * f) : ((a * b) * c) * d = ((a * e) * f) * d := by rw [mul_assoc a] rw [h] rw [←mul_assoc a] -- 3ª demostración example (a b c d e f : ℝ) (h : b * c = e * f) : ((a * b) * c) * d = ((a * e) * f) * d := by rw [mul_assoc a, h, ←mul_assoc a] |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 6.
2. Si c = ba-d y d = ab, entonces c = 0
Demostrar con Lean4 que si a, b, c y d son números reales tales
|
1 2 |
c = b * a - d d = a * b |
entonces
|
1 |
c = 0 |
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic example (a b c d : ℝ) (h1 : c = b * a - d) (h2 : d = a * b) : c = 0 := by sorry |
Demostración en lenguaje natural
Por la siguiente cadena de igualdades
\begin{align}
c &= ba – d &&\text{[por la primera hipótesis]} \\
&= ab – d &&\text{[por la conmutativa]} \\
&= ab – ab &&\text{[por la segunda hipótesis]} \\
&= 0
\end{align}
Demostraciones con Lean
|
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 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic -- 1ª demostración example (a b c d : ℝ) (h1 : c = b * a - d) (h2 : d = a * b) : c = 0 := calc c = b * a - d := by rw [h1] _ = a * b - d := by rw [mul_comm] _ = a * b - a * b := by rw [h2] _ = 0 := by rw [sub_self] -- 2ª demostración example (a b c d : ℝ) (h1 : c = b * a - d) (h2 : d = a * b) : c = 0 := by rw [h1] rw [mul_comm] rw [h2] rw [sub_self] -- 3ª demostración example (a b c d : ℝ) (h1 : c = b * a - d) (h2 : d = a * b) : c = 0 := by rw [h1, mul_comm, h2, sub_self] |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 7.
3. (a+b)(a+b) = aa+2ab+bb
Demostrar con Lean4 que si a y b son números reales, entonces
|
1 |
(a + b) * (a + b) = a * a + 2 * (a * b) + b * b |
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a b c : ℝ) example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := sorry |
Demostración en lenguaje natural
Por la siguiente cadena de igualdades
\begin{align}
(a + b)(a + b)
&= (a + b)a + (a + b)b &&\text{[por la distributiva]} \\
&= aa + ba + (a + b)b &&\text{[por la distributiva]} \\
&= aa + ba + (ab + bb) &&\text{[por la distributiva]} \\
&= aa + ba + ab + bb &&\text{[por la asociativa]} \\
&= aa + (ba + ab) + bb &&\text{[por la asociativa]} \\
&= aa + (ab + ab) + bb &&\text{[por la conmutativa]} \\
&= aa + 2(ab) + bb &&\text{[por def. de doble]} \\
\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.Data.Real.Basic import Mathlib.Tactic variable (a b c : ℝ) -- 1ª demostración example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := calc (a + b) * (a + b) = (a + b) * a + (a + b) * b := by rw [mul_add] _ = a * a + b * a + (a + b) * b := by rw [add_mul] _ = a * a + b * a + (a * b + b * b) := by rw [add_mul] _ = a * a + b * a + a * b + b * b := by rw [←add_assoc] _ = a * a + (b * a + a * b) + b * b := by rw [add_assoc (a * a)] _ = a * a + (a * b + a * b) + b * b := by rw [mul_comm b a] _ = a * a + 2 * (a * b) + b * b := by rw [←two_mul] -- 2ª demostración example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := calc (a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by rw [mul_add, add_mul, add_mul] _ = a * a + (b * a + a * b) + b * b := by rw [←add_assoc, add_assoc (a * a)] _ = a * a + 2 * (a * b) + b * b := by rw [mul_comm b a, ←two_mul] -- 3ª demostración example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := calc (a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by ring _ = a * a + (b * a + a * b) + b * b := by ring _ = a * a + 2 * (a * b) + b * b := by ring -- 4ª demostración example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by ring -- 5ª demostración example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by rw [mul_add] rw [add_mul] rw [add_mul] rw [←add_assoc] rw [add_assoc (a * a)] rw [mul_comm b a] rw [←two_mul] -- 6ª demostración example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by rw [mul_add, add_mul, add_mul] rw [←add_assoc, add_assoc (a * a)] rw [mul_comm b a, ←two_mul] -- 7ª demostración example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by linarith |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 7.
4. (a+b)(c+d) = ac+ad+bc+bd
Demostrar con Lean4 que si a, b, c y d son números reales, entonces
|
1 |
(a + b) * (c + d) = a * c + a * d + b * c + b * d |
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a b c d : ℝ) example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := sorry |
Demostración en lenguaje natural
Por la siguiente cadena de igualdades
\begin{align}
(a + b)(c + d)
&= a(c + d) + b(c + d) &&\text{[por la distributiva]} \\
&= ac + ad + b(c + d) &&\text{[por la distributiva]} \\
&= ac + ad + (bc + bd) &&\text{[por la distributiva]} \\
&= ac + ad + bc + bd &&\text{[por la asociativa]}
\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 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a b c d : ℝ) -- 1ª demostración example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := calc (a + b) * (c + d) = a * (c + d) + b * (c + d) := by rw [add_mul] _ = a * c + a * d + b * (c + d) := by rw [mul_add] _ = a * c + a * d + (b * c + b * d) := by rw [mul_add] _ = a * c + a * d + b * c + b * d := by rw [←add_assoc] -- 2ª demostración example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := calc (a + b) * (c + d) = a * (c + d) + b * (c + d) := by ring _ = a * c + a * d + b * (c + d) := by ring _ = a * c + a * d + (b * c + b * d) := by ring _ = a * c + a * d + b * c + b * d := by ring -- 3ª demostración example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by ring -- 4ª demostración example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by rw [add_mul] rw [mul_add] rw [mul_add] rw [← add_assoc] -- 5ª demostración example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by rw [add_mul, mul_add, mul_add, ←add_assoc] |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 8.
5. (a+b)(a-b) = a²-b²
Demostrar con Lean4 que si a y b son números reales, entonces
|
1 |
(a + b) * (a - b) = a^2 - b^2 |
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a b : ℝ) example : (a + b) * (a - b) = a^2 - b^2 := sorry |
Demostración en lenguaje natural
Por la siguiente cadena de igualdades:
\begin{align}
(a + b)(a – b)
&= a(a – b) + b(a – b) &&\text{[por la distributiva]} \\
&= (aa – ab) + b(a – b) &&\text{[por la distributiva]} \\
&= (a^2 – ab) + b(a – b) &&\text{[por def. de cuadrado]} \\
&= (a^2 – ab) + (ba – bb) &&\text{[por la distributiva]} \\
&= (a^2 – ab) + (ba – b^2) &&\text{[por def. de cuadrado]} \\
&= (a^2 + -(ab)) + (ba – b^2) &&\text{[por def. de resta]} \\
&= a^2 + (-(ab) + (ba – b^2)) &&\text{[por la asociativa]} \\
&= a^2 + (-(ab) + (ba + -b^2)) &&\text{[por def. de resta]} \\
&= a^2 + ((-(ab) + ba) + -b^2) &&\text{[por la asociativa]} \\
&= a^2 + ((-(ab) + ab) + -b^2) &&\text{[por la conmutativa]} \\
&= a^2 + (0 + -b^2) &&\text{[por def. de opuesto]} \\
&= (a^2 + 0) + -b^2 &&\text{[por asociativa]} \\
&= a^2 + -b^2 &&\text{[por def. de cero]} \\
&= a^2 – b^2 &&\text{[por def. de resta]}
\end{align}
Demostraciones con Lean
|
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 66 67 68 69 70 71 72 73 74 75 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a b : ℝ) -- 1ª demostración -- =============== example : (a + b) * (a - b) = a^2 - b^2 := calc (a + b) * (a - b) = a * (a - b) + b * (a - b) := by rw [add_mul] _ = (a * a - a * b) + b * (a - b) := by rw [mul_sub] _ = (a^2 - a * b) + b * (a - b) := by rw [← pow_two] _ = (a^2 - a * b) + (b * a - b * b) := by rw [mul_sub] _ = (a^2 - a * b) + (b * a - b^2) := by rw [← pow_two] _ = (a^2 + -(a * b)) + (b * a - b^2) := by ring _ = a^2 + (-(a * b) + (b * a - b^2)) := by rw [add_assoc] _ = a^2 + (-(a * b) + (b * a + -b^2)) := by ring _ = a^2 + ((-(a * b) + b * a) + -b^2) := by rw [← add_assoc (-(a * b)) (b * a) (-b^2)] _ = a^2 + ((-(a * b) + a * b) + -b^2) := by rw [mul_comm] _ = a^2 + (0 + -b^2) := by rw [neg_add_self (a * b)] _ = (a^2 + 0) + -b^2 := by rw [← add_assoc] _ = a^2 + -b^2 := by rw [add_zero] _ = a^2 - b^2 := by linarith -- 2ª demostración -- =============== example : (a + b) * (a - b) = a^2 - b^2 := calc (a + b) * (a - b) = a * (a - b) + b * (a - b) := by ring _ = (a * a - a * b) + b * (a - b) := by ring _ = (a^2 - a * b) + b * (a - b) := by ring _ = (a^2 - a * b) + (b * a - b * b) := by ring _ = (a^2 - a * b) + (b * a - b^2) := by ring _ = (a^2 + -(a * b)) + (b * a - b^2) := by ring _ = a^2 + (-(a * b) + (b * a - b^2)) := by ring _ = a^2 + (-(a * b) + (b * a + -b^2)) := by ring _ = a^2 + ((-(a * b) + b * a) + -b^2) := by ring _ = a^2 + ((-(a * b) + a * b) + -b^2) := by ring _ = a^2 + (0 + -b^2) := by ring _ = (a^2 + 0) + -b^2 := by ring _ = a^2 + -b^2 := by ring _ = a^2 - b^2 := by ring -- 3ª demostración -- =============== example : (a + b) * (a - b) = a^2 - b^2 := by ring -- 4ª demostración (por reescritura usando el lema anterior) -- ========================================================= -- El lema anterior es lemma aux : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by ring -- La demostración es example : (a + b) * (a - b) = a^2 - b^2 := by rw [sub_eq_add_neg] rw [aux] rw [mul_neg] rw [add_assoc (a * a)] rw [mul_comm b a] rw [neg_add_self] rw [add_zero] rw [← pow_two] rw [mul_neg] rw [← pow_two] rw [← sub_eq_add_neg] |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 8.