La semana en Calculemus (3 de febrero de 2024)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. La raíz cuadrada de 2 es irracional
- 2. Las funciones f(x,y) = (x + y)² y g(x,y) = x² + 2xy + y² son iguales
- 3. En ℝ, |a| = |a – b + b|
- 4. En ℝ, si 1 < a, entonces a < aa
- 5. La sucesión constante sₙ = c converge a c
A continuación se muestran las soluciones.
1. La raíz cuadrada de 2 es irracional
Demostrar con Lean4 que la raíz cuadrada de 2 es irracional; es decir, que no existen \(m, n ∈ ℕ\) tales que \(m\) y \(n\) son coprimos (es decir, que no tienen factores comunes distintos de uno) y \(m² = 2n²\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic import Mathlib.Data.Nat.Prime import Std.Data.Nat.Gcd open Nat variable {m n : ℕ} example : ¬∃ m n, coprime m n ∧ m ^ 2 = 2 * n ^ 2 := by sorry |
1. Demostración en lenguaje natural
Usaremos el lema del ejercicio anterior:
\[ (∀ n ∈ ℕ)[2 ∣ n² → 2 | n] \]
Supongamos que existen existen \(m, n ∈ ℕ\) tales que \(m\) y \(n\) son coprimos y \(m² = 2n²\) y tenemos que demostrar una contradicción. Puesto que 2 divide a 1, para tener la contradicción basta demostrar que 2 divide a 1 y (ya que \(m\) y \(n\) son coprimos); para ello es suficiente demostrar que 2 divide al máximo común divisor de \(m\) y \(n\). En definitiva, basta demostrar que 2 divide a \(m\) y a \(n\).
La demostración de que 2 divide a \(m\) es
\begin{align}
m² = 2n² &⟹ 2 | m² \\
&⟹ 2 | m &&\text{[por el lema]}
\end{align}
Para demostrar que 2 divide a \(n\), observamos que, puesto que 2 divide a \(m\), existe un \(k ∈ ℕ\) tal que \(m = 2k\). Sustituyendo en
\[ m² = 2n² \]
se tiene
\[ (2k)² = 2n² \]
Simplificando, queda
\[ 2k = n² \]
Por tanto, 2 divide a \(n²\) y, por el lema, 2 divide a \(n\).
2. 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 66 |
import Mathlib.Tactic import Mathlib.Data.Nat.Prime import Std.Data.Nat.Gcd open Nat variable {m n : ℕ} lemma par_si_cuadrado_par (h : 2 ∣ n ^ 2) : 2 ∣ n := by rw [pow_two] at h -- h : 2 ∣ n * n have h2 : 2 ∣ n ∨ 2 ∣ n := (Prime.dvd_mul prime_two).mp h tauto example : ¬∃ m n, coprime m n ∧ m ^ 2 = 2 * n ^ 2 := by rintro ⟨m, n, ⟨h1, h2⟩⟩ -- m n : ℕ -- h1 : coprime m n -- h2 : m ^ 2 = 2 * n ^ 2 -- ⊢ False have h3 : ¬(2 ∣ 1) := by norm_num have h4 : 2 ∣ 1 := by have h5 : Nat.gcd m n = 1 := h1 rw [← h5] -- ⊢ 2 ∣ Nat.gcd m n have h6 : 2 ∣ m := by apply par_si_cuadrado_par -- ⊢ 2 ∣ m ^ 2 rw [h2] -- ⊢ 2 ∣ 2 * n ^ 2 exact Nat.dvd_mul_right 2 (n ^ 2) have h7 : 2 ∣ n := by have h8 : ∃ k, m = 2 * k := h6 rcases h8 with ⟨k, h9⟩ -- k : ℕ -- h9 : m = 2 * k have h10 : 2 * k ^ 2 = n ^ 2 := by have h10a : 2 * (2 * k ^ 2) = 2 * n ^ 2 := calc 2 * (2 * k ^ 2) = (2 * k) ^ 2 := by nlinarith _ = m ^ 2 := by rw [← h9] _ = 2 * n ^ 2 := h2 show 2 * k ^ 2 = n ^ 2 exact (mul_right_inj' (by norm_num : 2 ≠ 0)).mp h10a have h11 : 2 ∣ n ^ 2 := by rw [← h10] -- ⊢ 2 ∣ 2 * k ^ 2 exact Nat.dvd_mul_right 2 (k ^ 2) show 2 ∣ n exact par_si_cuadrado_par h11 show 2 ∣ Nat.gcd m n exact Nat.dvd_gcd h6 h7 show False exact h3 h4 -- Lemas usados -- ============ -- variable (p k : ℕ) -- #check (pow_two n : n ^ 2 = n * n) -- #check (Prime.dvd_mul : Nat.Prime p → (p ∣ m * n ↔ p ∣ m ∨ p ∣ n)) -- #check (prime_two : Nat.Prime 2) -- #check (Nat.dvd_gcd : k ∣ m → k ∣ n → k ∣ Nat.gcd m n) -- #check (Nat.dvd_mul_right m n : m ∣ m * n) -- #check (mul_right_inj' : k ≠ 0 → (k * m = k * n ↔ m = n)) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
2. Las funciones f(x,y) = (x + y)² y g(x,y) = x² + 2xy + y² son iguales
Demostrar con Lean4 que las funciones \(f(x,y) = (x + y)²\) y \(g(x,y) = x² + 2xy + y\)² son iguales.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 |
import Mathlib.Data.Real.Basic example : (fun x y : ℝ ↦ (x + y)^2) = (fun x y : ℝ ↦ x^2 + 2*x*y + y^2) := by sorry |
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 |
import Mathlib.Data.Real.Basic -- 1ª demostración -- =============== example : (fun x y : ℝ ↦ (x + y)^2) = (fun x y : ℝ ↦ x^2 + 2*x*y + y^2) := by ext u v -- u v : ℝ -- ⊢ (u + v) ^ 2 = u ^ 2 + 2 * u * v + v ^ 2 ring -- Comentario: La táctica ext transforma las conclusiones de la forma -- (fun x ↦ f x) = (fun x ↦ g x) en f x = g x. -- 2ª demostración -- =============== example : (fun x y : ℝ ↦ (x + y)^2) = (fun x y : ℝ ↦ x^2 + 2*x*y + y^2) := by { ext ; ring } |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 41.
3. En ℝ, |a| = |a – b + b|
Demostrar con Lean4 que en \(ℝ\), \(|a| = |a – b + 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| = |a - b + b| := by sorry |
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 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) -- 1ª demostración -- =============== example : |a| = |a - b + b| := by congr -- a = a - b + b ring -- Comentario: La táctica congr sustituye una conclusión de la forma -- A = B por las igualdades de sus subtérminos que no no iguales por -- definición. Por ejemplo, sustituye la conclusión (x * f y = g w * f z) -- por las conclusiones (x = g w) y (y = z). -- 2ª demostración -- =============== example (a b : ℝ) : |a| = |a - b + b| := by { congr ; ring } -- 3ª demostración -- =============== example (a b : ℝ) : |a| = |a - b + b| := by ring_nf |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 41.
4. En ℝ, si 1 < a, entonces a < aa
Demostrar con Lean4 que en \(ℝ\), si \(1 < a\), entonces \(a < aa\)
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable {a : ℝ} example (h : 1 < a) : a < a * a := by sorry |
1. Demostración en lenguaje natural
Se usarán los siguientes lemas
\begin{align}
&0 < 1 \tag{L1} \\
&(∀ a ∈ ℝ[1a = a] \tag{L2} \\
&(∀ a, b, c ∈ ℝ)[0 < a → (ba < ca ↔ b < c)] \tag{L3}
\end{align}
En primer lugar, tenemos que
\[ 0 < a \tag{1} \]
ya que
\begin{align}
0 &< 1 &&\text{[por L1]} \\
&< a &&\text{[por la hipótesis]}
\end{align}
Entonces,
\begin{align}
a &= 1a &&\text{[por L2]} \\
&< aa &&\text{[por L3, (1) y la hipótesis]}
\end{align}
2. 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 variable {a : ℝ} -- 1ª demostración -- =============== example (h : 1 < a) : a < a * a := by have h1 : 0 < a := calc 0 < 1 := zero_lt_one _ < a := h show a < a * a calc a = 1 * a := (one_mul a).symm _ < a * a := (mul_lt_mul_right h1).mpr h -- Comentarios: La táctica (convert e) genera nuevos subojetivos cuya -- conclusiones son las diferencias entre el tipo de e y la conclusión. -- 2ª demostración -- =============== example (h : 1 < a) : a < a * a := by convert (mul_lt_mul_right _).2 h . -- ⊢ a = 1 * a rw [one_mul] . -- ⊢ 0 < a exact lt_trans zero_lt_one h -- Lemas usados -- ============ -- variables (a b c : ℝ) -- #check (mul_lt_mul_right : 0 < a → (b * a < c * a ↔ b < c)) -- #check (one_mul a : 1 * a = a) -- #check (lt_trans : a < b → b < c → a < c) -- #check (zero_lt_one : 0 < 1) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 41.
5. La sucesión constante sₙ = c converge a c
En Lean, una sucesión \(s₀, s₁, s₂, …\) se puede representar mediante una función \((s : ℕ → ℝ)\) de forma que \(s(n)\) es \(sₙ\).
Se define que a es el límite de la sucesión \(s\), por
|
1 2 |
def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε |
Demostrar que el límite de la sucesión constante \(sₙ = c\) es \(c\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε example : limite (fun _ : ℕ ↦ c) c := by sorry |
1. Demostración en lenguaje natural
Tenemos que demostrar que para cada \(ε ∈ ℝ\) tal que \(ε > 0\), existe un \(N ∈ ℕ\), tal que \((∀n ∈ ℕ)[n ≥ N → |s(n) – a| < ε]\). Basta tomar \(N\) como \(0\), ya que para todo \(n ≥ N\) se tiene
\begin{align}
|s(n) – a| &= |a – a| \\
&= |0| \\
&= 0 \\
&< ε \\
\end{align}
2. 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 66 67 68 69 70 71 72 73 74 75 76 77 |
import Mathlib.Data.Real.Basic def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε -- 1ª demostración -- =============== example : limite (fun _ : ℕ ↦ c) c := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun _ => c) n - c| < ε use 0 -- ⊢ ∀ (n : ℕ), n ≥ 0 → |(fun _ => c) n - c| < ε intros n _hn -- n : ℕ -- hn : n ≥ 0 -- ⊢ |(fun _ => c) n - c| < ε show |(fun _ => c) n - c| < ε calc |(fun _ => c) n - c| = |c - c| := by dsimp _ = |0| := by {congr ; exact sub_self c} _ = 0 := abs_zero _ < ε := hε -- 2ª demostración -- =============== example : limite (fun _ : ℕ ↦ c) c := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun _ => c) n - c| < ε use 0 -- ⊢ ∀ (n : ℕ), n ≥ 0 → |(fun _ => c) n - c| < ε intros n _hn -- n : ℕ -- hn : n ≥ 0 -- ⊢ |(fun _ => c) n - c| < ε show |(fun _ => c) n - c| < ε calc |(fun _ => c) n - c| = 0 := by simp _ < ε := hε -- 3ª demostración -- =============== example : limite (fun _ : ℕ ↦ c) c := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun _ => c) n - c| < ε aesop -- 4ª demostración -- =============== example : limite (fun _ : ℕ ↦ c) c := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun _ => c) n - c| < ε aesop -- 5ª demostración -- =============== example : limite (fun _ : ℕ ↦ c) c := fun ε hε ↦ by aesop -- Lemas usados -- ============ -- #check (sub_self a : a - a = 0) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3. Demostraciones con Isabelle/HOL
|
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 |
theory Limite_de_sucesiones_constantes imports Main HOL.Real begin definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)" (* 1ª demostración *) lemma "limite (λ n. c) c" proof (unfold limite_def) show "∀ε>0. ∃k::nat. ∀n≥k. ¦c - c¦ < ε" proof (intro allI impI) fix ε :: real assume "0 < ε" have "∀n≥0::nat. ¦c - c¦ < ε" proof (intro allI impI) fix n :: nat assume "0 ≤ n" have "c - c = 0" by (simp only: diff_self) then have "¦c - c¦ = 0" by (simp only: abs_eq_0_iff) also have "… < ε" by (simp only: ‹0 < ε›) finally show "¦c - c¦ < ε" by this qed then show "∃k::nat. ∀n≥k. ¦c - c¦ < ε" by (rule exI) qed qed (* 2ª demostración *) lemma "limite (λ n. c) c" proof (unfold limite_def) show "∀ε>0. ∃k::nat. ∀n≥k. ¦c - c¦ < ε" proof (intro allI impI) fix ε :: real assume "0 < ε" have "∀n≥0::nat. ¦c - c¦ < ε" by (simp add: ‹0 < ε›) then show "∃k::nat. ∀n≥k. ¦c - c¦ < ε" by (rule exI) qed qed (* 3ª demostración *) lemma "limite (λ n. c) c" unfolding limite_def by simp (* 4ª demostración *) lemma "limite (λ n. c) c" by (simp add: limite_def) end |
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 41.