La semana en Calculemus (16 de septiembre de 2023)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. En ℝ, |a| – |b| ≤ |a – b|
- 2. Si x, y, z ∈ ℕ, entonces x divide a yxz
- 3. Si x divide a w, entonces también divide a y(xz)+x²+w²
- 4. Conmutatividad del máximo común divisor
- 5. En los retículos, x ⊓ y = y ⊓ x
A continuación se muestran las soluciones.
1. En ℝ, |a| – |b| ≤ |a – b|
Demostrar con Lean4 que si \(a\) y \(b\) números reales, entonces
\[|a| – |b| \leq |a – b|\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) example : |a| - |b| ≤ |a - b| := by sorry |
Demostraciones en lenguaje natural (LN)
1ª demostración en LN
Por la siguiente cadena de desigualdades
\begin{align}
|a| – |b| &= |a – b + b| – |b| \\
&\leq (|a – b| + |b|) – |b| &&\text{[por la desigualdad triangular]}\\
&= |a – b|
\end{align}
2ª demostración en LN
Por la desigualdad triangular
\[ |a – b + b| \leq |a – b| + |b| \]
simplificando en la izquierda
\[ |a| \leq |a – b| + |b| \]
y, pasando \(|b|\) a la izquierda
\[ |a| – |b| ≤ |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 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) -- 1ª demostración (basada en la 1ª en LN) example : |a| - |b| ≤ |a - b| := calc |a| - |b| = |a - b + b| - |b| := congrArg (fun x => |x| - |b|) (sub_add_cancel a b).symm _ ≤ (|a - b| + |b|) - |b| := sub_le_sub_right (abs_add (a - b) b) (|b|) _ = |a - b| := add_sub_cancel (|a - b|) (|b|) -- 2ª demostración (basada en la 1ª en LN) example : |a| - |b| ≤ |a - b| := calc |a| - |b| = |a - b + b| - |b| := by rw [sub_add_cancel] _ ≤ (|a - b| + |b|) - |b| := by apply sub_le_sub_right apply abs_add _ = |a - b| := by rw [add_sub_cancel] -- 3ª demostración (basada en la 2ª en LN) example : |a| - |b| ≤ |a - b| := by have h1 : |a - b + b| ≤ |a - b| + |b| := abs_add (a - b) b rw [sub_add_cancel] at h1 exact abs_sub_abs_le_abs_sub a b -- 4ª demostración example : |a| - |b| ≤ |a - b| := abs_sub_abs_le_abs_sub 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. 18.
2. Si x, y, z ∈ ℕ, entonces x divide a yxz
Demostrar con Lean4 que si \(x,y,z \in \mathbb{N}\), entonces \(x \mid yxz\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable (x y z : ℕ) example : x ∣ y * x * z := by sorry |
Demostración en lenguaje natural
Por la transitividad de la divisibilidad aplicada a las relaciones
\begin{align}
x &\mid yx \\
yx &\mid yxz
\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.Data.Real.Basic variable (x y z : ℕ) -- 1ª demostración -- =============== example : x ∣ y * x * z := by have h1 : x ∣ y * x := dvd_mul_left x y have h2 : (y * x) ∣ (y * x * z) := dvd_mul_right (y * x) z show x ∣ y * x * z exact dvd_trans h1 h2 -- 2ª demostración -- =============== example : x ∣ y * x * z := dvd_trans (dvd_mul_left x y) (dvd_mul_right (y * x) z) -- 3ª demostración -- =============== example : x ∣ y * x * z := by apply dvd_mul_of_dvd_left apply dvd_mul_left -- Los lemas utilizados son: #check (dvd_mul_left x y : x ∣ y * x) #check (dvd_mul_right x y : x ∣ x * y) #check (dvd_trans : x ∣ y → y ∣ z → x ∣ z) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 19.
3. Si x divide a w, entonces también divide a y(xz)+x²+w²
Demostrar con Lean4 que si \(x\) divide a \(w\), entonces también divide a \(y(xz)+x^2+w^2\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable (w x y z : ℕ) example (h : x ∣ w) : x ∣ y * (x * z) + x^2 + w^2 := by sorry |
Demostración en lenguaje natural
Por la divisibilidad de la suma basta probar que
\begin{align}
x &\mid yxz \tag{1} \\
x &\mid x^2 \tag{2} \\
x &\mid w^2 \tag{3}
\end{align}
Para demostrar (1), por la divisibilidad del producto se tiene
\[ x \mid xz\]
y, de nuevo por la divisibilidad del producto,
\[ x \mid y(xz)\]
La propiedad (2) se tiene por la definición de cuadrado y la divisibilidad del producto.
La propiedad (3) se tiene por la definición de cuadrado, la hipótesis y la divisibilidad del producto.
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.Data.Real.Basic variable (w x y z : ℕ) -- 1ª demostración example (h : x ∣ w) : x ∣ y * (x * z) + x^2 + w^2 := by have h1 : x ∣ x * z := dvd_mul_right x z have h2 : x ∣ y * (x * z) := dvd_mul_of_dvd_right h1 y have h3 : x ∣ x^2 := by apply dvd_mul_left have h4 : x ∣ w * w := dvd_mul_of_dvd_left h w have h5 : x ∣ w^2 := by rwa [← pow_two w] at h4 have h6 : x ∣ y * (x * z) + x^2 := dvd_add h2 h3 show x ∣ y * (x * z) + x^2 + w^2 exact dvd_add h6 h5 -- 2ª demostración example (h : x ∣ w) : x ∣ y * (x * z) + x^2 + w^2 := by apply dvd_add { apply dvd_add { apply dvd_mul_of_dvd_right apply dvd_mul_right } { rw [pow_two] apply dvd_mul_right }} { rw [pow_two] apply dvd_mul_of_dvd_left h } -- 3ª demostración example (h : x ∣ w) : x ∣ y * (x * z) + x^2 + w^2 := by repeat' apply dvd_add { apply dvd_mul_of_dvd_right apply dvd_mul_right } { rw [pow_two] apply dvd_mul_right } { rw [pow_two] apply dvd_mul_of_dvd_left h } -- Lemas usados -- ============ -- #check (dvd_add : x ∣ y → x ∣ z → x ∣ y + z) -- #check (dvd_mul_left x y : x ∣ y * x) -- #check (dvd_mul_right x y : x ∣ x * y) -- #check (dvd_mul_of_dvd_left : x ∣ y → ∀ (c : ℕ), x ∣ y * c) -- #check (dvd_mul_of_dvd_right : x ∣ y → ∀ (c : ℕ), x ∣ c * y) -- #check (pow_two x : x ^ 2 = x * x) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 19.
4. Conmutatividad del máximo común divisor
Demostrar con Lean4 que si \(m, n \in \mathbb{N}\) son números naturales, entonces
\[\gcd(m, n) = \gcd(n, m)\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable (k m n : ℕ) open Nat example : gcd m n = gcd n m := by sorry |
Demostración en lenguaje natural
Es consecuencia del siguiente lema auxiliar
\[ (\forall x, y \in \mathbb{N})[\gcd(x,y) \mid \gcd(y,x)] \tag{1} \]
En efecto, sustituyendo en (1) \(x\) por \(m\) e \(y\) por \(n\), se tiene
\[ \gcd(m, n) \mid \gcd(n, m) \tag{2}\]
y, sustituyendo en (1) \(x\) por \(n\) e \(y\) por \(m\), se tiene
\[ \gcd(n, m) \mid \gcd(m, n) \tag{3} \]
Finalmente, aplicando la propiedad antisimétrica de la divisibilidad a (2) y (3), se tiene
\[ \gcd(m, n) = \gcd(n, m) \]
Para demostrar (1), por la definición del máximo común divisor, basta demostrar las siguientes relaciones
\begin{align}
\gcd(m, n) &\mid n \\
\gcd(m, n) &\mid m
\end{align}
y ambas se tienen por la definición del máximo común divisor.
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 |
import Mathlib.Data.Real.Basic variable (k m n : ℕ) open Nat -- 1ª demostración del lema auxiliar lemma aux : gcd m n ∣ gcd n m := by have h1 : gcd m n ∣ n := gcd_dvd_right m n have h2 : gcd m n ∣ m := gcd_dvd_left m n show gcd m n ∣ gcd n m exact dvd_gcd h1 h2 -- 2ª demostración del lema auxiliar example : gcd m n ∣ gcd n m := dvd_gcd (gcd_dvd_right m n) (gcd_dvd_left m n) -- 1ª demostración example : gcd m n = gcd n m := by have h1 : gcd m n ∣ gcd n m := aux m n have h2 : gcd n m ∣ gcd m n := aux n m show gcd m n = gcd n m exact _root_.dvd_antisymm h1 h2 -- 2ª demostración example : gcd m n = gcd n m := by apply _root_.dvd_antisymm { exact aux m n } { exact aux n m } -- 3ª demostración example : gcd m n = gcd n m := _root_.dvd_antisymm (aux m n) (aux n m) -- 4ª demostración example : gcd m n = gcd n m := -- by apply? gcd_comm m n -- Lemas usados -- ============ -- #check (_root_.dvd_antisymm : m ∣ n → n ∣ m → m = n) -- #check (dvd_gcd : k ∣ m → k ∣ n → k ∣ gcd m n) -- #check (gcd_comm m n : gcd m n = gcd n m) -- #check (gcd_dvd_left m n: gcd m n ∣ m) -- #check (gcd_dvd_right m n : gcd m n ∣ n) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 19.
5. En los retículos, x ⊓ y = y ⊓ x
Demostrar con Lean4 que en los retículos se verifica que
\[x ⊓ y = y ⊓ x\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (x y z : α) example : x ⊓ y = y ⊓ x := by sorry |
Demostración en lenguaje natural
Es consecuencia del siguiente lema auxiliar
\[ (∀ a, b)[a ⊓ b ≤ b ⊓ a] \tag{1} \]
En efecto, sustituyendo en (1) \(a\) por \(x\) y \(b\) por \(y\), se tiene
\[ x ⊓ y ≤ y ⊓ x \tag{2} \]
y sustituyendo en (1) \(a\) por \(y\) y \(b\) por \(x\), se tiene
\[ y ⊓ x ≤ x ⊓ y \tag{3} \]
Finalmente, aplicando la propiedad antisimétrica de la divisibilidad a (2) y (3), se tiene
\[ x ⊓ y = y ⊓ x \]
Para demostrar (1), por la definición del ínfimo, basta demostrar las siguientes relaciones
\begin{align}
y ⊓ x &≤ x \\
y ⊓ x &≤ y
\end{align}
y ambas se tienen por la definición del ínfimo.
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 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (x y z : α) -- 1ª demostración del lema auxiliar lemma aux : x ⊓ y ≤ y ⊓ x := by have h1 : x ⊓ y ≤ y := inf_le_right have h2 : x ⊓ y ≤ x := inf_le_left show x ⊓ y ≤ y ⊓ x exact le_inf h1 h2 -- 2ª demostración del lema auxiliar example : x ⊓ y ≤ y ⊓ x := by apply le_inf { apply inf_le_right } { apply inf_le_left } -- 3ª demostración del lema auxiliar example : x ⊓ y ≤ y ⊓ x := le_inf inf_le_right inf_le_left -- 1ª demostración example : x ⊓ y = y ⊓ x := by have h1 : x ⊓ y ≤ y ⊓ x := aux x y have h2 : y ⊓ x ≤ x ⊓ y := aux y x show x ⊓ y = y ⊓ x exact le_antisymm h1 h2 -- 2ª demostración example : x ⊓ y = y ⊓ x := by apply le_antisymm { apply aux } { apply aux } -- 3ª demostración example : x ⊓ y = y ⊓ x := le_antisymm (aux x y) (aux y x) -- 4ª demostración example : x ⊓ y = y ⊓ x := by apply le_antisymm; simp ; simp -- 5ª demostración example : x ⊓ y = y ⊓ x := -- by apply? inf_comm -- Lemas usados -- ============ -- #check (inf_comm : x ⊓ y = y ⊓ x) -- #check (inf_le_left : x ⊓ y ≤ x) -- #check (inf_le_right : x ⊓ y ≤ y) -- #check (le_antisymm : x ≤ y → y ≤ x → x = y) -- #check (le_inf : z ≤ x → z ≤ y → z ≤ x ⊓ y) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 20.