La semana en Calculemus (27 de enero de 2024)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. En ℝ, x² = y² → x = y ∨ x = -y
- 2. ¬¬P → P
- 3. (P → Q) ↔ ¬P ∨ Q
- 4. Existen infinitos números primos
- 5. Si n² es par, entonces n es par
A continuación se muestran las soluciones.
1. En ℝ, x² = y² → x = y ∨ x = -y
Demostrar con Lean4 que en \(ℝ\),
\[x² = y² → x = y ∨ x = -y\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable (x y : ℝ) example (h : x^2 = y^2) : x = y ∨ x = -y := by sorry |
1. Demostración en lenguaje natural
Usaremos los siguientes lemas
\begin{align}
&(∀ x ∈ ℝ)[x – x = 0] \tag{L1} \\
&(∀ x, y ∈ ℝ)[xy = 0 → x = 0 ∨ y = 0] \tag{L2} \\
&(∀ x, y ∈ ℝ)[x – y = 0 ↔ x = y] \tag{L3} \\
&(∀ x, y ∈ ℝ)[x + y = 0 → x = -y] \tag{L4}
\end{align}
Se tiene que
\begin{align}
(x – y)(x + y) &= x² – y² \\
&= y² – y² &&\text{[por la hipótesis]} \\
&= 0 &&\text{[por L1]}
\end{align}
y, por el lema L2, se tiene que
\[ x – y = 0 ∨ x + y = 0 \]
Acabaremos la demostración por casos.
Primer caso:
\begin{align}
x – y = 0 &⟹ x = y &&\text{[por L3]} \\
&⟹ x = y ∨ x = -y
\end{align}
Segundo caso:
\begin{align}
x + y = 0 &⟹ x = -y &&\text{[por L4]} \\
&⟹ x = y ∨ x = -y
\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 |
import Mathlib.Data.Real.Basic variable (x y : ℝ) -- 1ª demostración -- =============== example (h : x^2 = y^2) : x = y ∨ x = -y := by have h1 : (x - y) * (x + y) = 0 := by calc (x - y) * (x + y) = x^2 - y^2 := by ring _ = y^2 - y^2 := by rw [h] _ = 0 := sub_self (y ^ 2) have h2 : x - y = 0 ∨ x + y = 0 := by apply eq_zero_or_eq_zero_of_mul_eq_zero h1 rcases h2 with h3 | h4 . -- h3 : x - y = 0 left -- ⊢ x = y exact sub_eq_zero.mp h3 . -- h4 : x + y = 0 right -- ⊢ x = -y exact eq_neg_of_add_eq_zero_left h4 -- 2ª demostración -- =============== example (h : x^2 = y^2) : x = y ∨ x = -y := by have h1 : (x - y) * (x + y) = 0 := by nlinarith have h2 : x - y = 0 ∨ x + y = 0 := by aesop rcases h2 with h3 | h4 . -- h3 : x - y = 0 left -- ⊢ x = y linarith . -- h4 : x + y = 0 right -- ⊢ x = -y linarith -- 2ª demostración -- =============== example (h : x^2 = y^2) : x = y ∨ x = -y := sq_eq_sq_iff_eq_or_eq_neg.mp h -- Lemas usados -- ============ -- #check (eq_neg_of_add_eq_zero_left : x + y = 0 → x = -y) -- #check (eq_zero_or_eq_zero_of_mul_eq_zero : x * y = 0 → x = 0 ∨ y = 0) -- #check (sq_eq_sq_iff_eq_or_eq_neg : x ^ 2 = y ^ 2 ↔ x = y ∨ x = -y) -- #check (sub_eq_zero : x - y = 0 ↔ x = y) -- #check (sub_self x : x - x = 0) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 39.
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 59 60 61 62 63 64 65 66 |
theory Cuadrado_igual_a_uno imports Main HOL.Real begin (* 1ª demostración *) lemma fixes x :: real assumes "x^2 = 1" shows "x = 1 ∨ x = -1" proof - have "(x - 1) * (x + 1) = x^2 - 1" by algebra also have "... = 0" using assms by simp finally have "(x - 1) * (x + 1) = 0" . moreover { assume "(x - 1) = 0" then have "x = 1" by simp } moreover { assume "(x + 1) = 0" then have "x = -1" by simp } ultimately show "x = 1 ∨ x = -1" by auto qed (* 2ª demostración *) lemma fixes x :: real assumes "x^2 = 1" shows "x = 1 ∨ x = -1" proof - have "(x - 1) * (x + 1) = x^2 - 1" by algebra also have "... = 0" using assms by simp finally have "(x - 1) * (x + 1) = 0" . then show "x = 1 ∨ x = -1" by auto qed (* 3ª demostración *) lemma fixes x :: real assumes "x^2 = 1" shows "x = 1 ∨ x = -1" proof - have "(x - 1) * (x + 1) = 0" proof - have "(x - 1) * (x + 1) = x^2 - 1" by algebra also have "… = 0" by (simp add: assms) finally show ?thesis . qed then show "x = 1 ∨ x = -1" by auto qed (* 4ª demostración *) lemma fixes x :: real assumes "x^2 = 1" shows "x = 1 ∨ x = -1" using assms power2_eq_1_iff by blast end |
2. ¬¬P → P
Demostrar con Lean4 que
\[ ¬¬P → P \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Tactic variable (P : Prop) example : ¬¬P → P := by sorry |
1. Demostración en lenguaje natural
Supongamos que
\[ ¬¬P \tag{1} \]
Por el principio del tercio excluso, se tiene
\[ P ∨ ¬P \]
lo que da lugar a dos casos.
En el primer caso, se supone \(P\) que es lo que hay que demostrar.
En el primer caso, se supone \(¬P\) que es una contradicción con (1).
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 |
import Mathlib.Tactic variable (P : Prop) -- 1ª demostración -- =============== example : ¬¬P → P := by intro h1 -- h1 : ¬¬P -- ⊢ P have h2 : P ∨ ¬ P := em P rcases h2 with h3 | h4 . -- h3 : P exact h3 . -- h4 : ¬P exfalso -- ⊢ False exact h1 h4 -- 2ª demostración -- =============== example : ¬¬P → P := by intro h1 -- h1 : ¬¬P -- ⊢ P rcases em P with h2 | h3 . -- h2 : P exact h2 . -- h3 : ¬P exact absurd h3 h1 -- 3ª demostración -- =============== example : ¬¬P → P := by intro h1 -- h1 : ¬¬P -- ⊢ P cases em P . -- h2 : P assumption . -- h3 : ¬P contradiction -- 4ª demostración -- =============== example : ¬¬P → P := by intro h by_cases P . assumption . contradiction -- 4ª demostración -- =============== example : ¬¬P → P := by intro h1 -- h1 : ¬¬P -- ⊢ P by_contra h -- h : ¬P -- ⊢ False exact h1 h -- 5ª demostración -- =============== example : ¬¬P → P := by tauto |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 40.
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 |
theory Eliminacion_de_la_doble_negacion imports Main begin (* 1ª demostración *) lemma "¬¬P ⟶ P" proof assume h1 : "¬¬P" have "¬P ∨ P" by (rule excluded_middle) then show "P" proof assume "¬P" then show "P" using h1 by (simp only: notE) next assume "P" then show "P" . qed qed (* 2ª demostración *) lemma "¬¬P ⟶ P" proof assume h1 : "¬¬P" show "P" proof (rule ccontr) assume "¬P" then show False using h1 by simp qed qed (* 3ª demostración *) lemma "¬¬P ⟶ P" by simp end |
3. (P → Q) ↔ ¬P ∨ Q
Demostrar con Lean4 que
\[ (P → Q) ↔ ¬P ∨ Q \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Tactic variable (P Q : Prop) example : (P → Q) ↔ ¬P ∨ Q := by sorry |
1. Demostración en lenguaje natural
Demostraremos cada una de las implicaciones.
(==>) Supongamos que \(P → Q\). Distinguimos dos subcasos según el valor de \(P\).
Primer subcaso: suponemos \(P\). Entonces, tenemos \(Q\) (porque \(P → Q\)) y. por tanto, \(¬P ∨ Q\).
Segundo subcaso: suponemos \(¬P\). Entonces. tenemos \(¬P ∨ Q\).
(<==) Supongamos que \(¬P ∨ Q\) y \(P\) y tenemos que demostrar \(Q\). Distinguimos dos subcasos según \(¬P ∨ Q\).
Primer subcaso: Suponemos \(¬P\). Entonces tenemos una contradicción con \(P\).
Segundo subcaso: Suponemos \(Q\), que es lo que tenemos que demostrar.
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 78 79 80 81 82 83 84 |
import Mathlib.Tactic variable (P Q : Prop) -- 1ª demostración -- =============== example : (P → Q) ↔ ¬P ∨ Q := by constructor . -- ⊢ (P → Q) → ¬P ∨ Q intro h1 -- h1 : P → Q -- ⊢ ¬P ∨ Q by_cases h2 : P . -- h2 : P right -- ⊢ Q apply h1 -- ⊢ P exact h2 . -- h2 : ¬P left -- ⊢ ¬P exact h2 . -- ⊢ ¬P ∨ Q → P → Q intros h3 h4 -- h3 : ¬P ∨ Q -- h4 : P -- ⊢ Q rcases h3 with h3a | h3b . -- h : ¬P exact absurd h4 h3a . -- h : Q exact h3b done -- 2ª demostración -- =============== example : (P → Q) ↔ ¬P ∨ Q := by constructor . -- ⊢ (P → Q) → ¬P ∨ Q intro h1 -- h1 : P → Q -- ⊢ ¬P ∨ Q by_cases h2: P . -- h2 : P right -- ⊢ Q exact h1 h2 . -- h2 : ¬P left -- ⊢ ¬P exact h2 . -- ⊢ ¬P ∨ Q → P → Q intros h3 h4 -- h3 : ¬P ∨ Q -- h4 : P -- ⊢ Q cases h3 . -- h : ¬P contradiction . -- h : Q assumption done -- 3ª demostración -- =============== example (P Q : Prop) : (P → Q) ↔ ¬P ∨ Q := imp_iff_not_or -- 4ª demostración -- =============== example (P Q : Prop) : (P → Q) ↔ ¬P ∨ Q := by tauto |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 40.
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 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 |
theory Implicacion_mediante_disyuncion_y_negacion imports Main begin (* 1ª demostración *) lemma "(P ⟶ Q) ⟷ (¬P ∨ Q)" proof assume "P ⟶ Q" show "¬P ∨ Q" proof - have "¬P ∨ P" by (rule excluded_middle) then show "¬P ∨ Q" proof (rule disjE) assume "¬P" then show "¬P ∨ Q" by (rule disjI1) next assume 2: "P" with `P ⟶ Q` have "Q" by (rule mp) then show "¬P ∨ Q" by (rule disjI2) qed qed next assume "¬P ∨ Q" show "P ⟶ Q" proof assume "P" note `¬P ∨ Q` then show "Q" proof (rule disjE) assume "¬P" then show Q using `P` by (rule notE) next assume "Q" then show "Q" by this qed qed qed (* 2ª demostración *) lemma "(P ⟶ Q) ⟷ (¬P ∨ Q)" proof assume "P ⟶ Q" show "¬P ∨ Q" proof - have "¬P ∨ P" by (rule excluded_middle) then show "¬P ∨ Q" proof assume "¬P" then show "¬P ∨ Q" .. next assume 2: "P" with `P ⟶ Q` have "Q" .. then show "¬P ∨ Q" .. qed qed next assume "¬P ∨ Q" show "P ⟶ Q" proof assume "P" note `¬P ∨ Q` then show "Q" proof assume "¬P" then show Q using `P` .. next assume "Q" then show "Q" . qed qed qed (* 3ª demostración *) lemma "(P ⟶ Q) ⟷ (¬P ∨ Q)" by simp end |
4. Existen infinitos números primos
Demostrar con Lean4 que existen infinitos números primos.
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 open Nat example (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by sorry |
1. Demostración en lenguaje natural
Se usarán los siguientes lemas de los números naturales, donde \(\text{Primo}(n)\) se verifica si \(n\) es primo y \(\text{minFac}(n)\) es el menor factor primo de \(n\).
\begin{align}
&n ≠ 1 → \text{Primo}(\text{minFac}(n)) \tag{L1} \\
&n! > 0 \tag{L2} \\
&0 < k → n < k + n \tag{L3} \\
&k < n → n ≠ k \tag{L4} \\
&k ≱ n → k ≤ n \tag{L5} \\
&0 < k → k ≤ n → k ∣ n! \tag{L6} \\
&0 < \text{minFac}(n) \tag{L7} \\
&k ∣ m → (k ∣ n ↔ k ∣ m + n) \tag{L8} \\
&\text{minFac}(n) ∣ n \tag{L9} \\
&\text{Primo}(n) → ¬n ∣ 1 \tag{L10}
\end{align}
Sea \(p\) el menor factor primo de \(n! + 1\). Tenemos que demostrar que \(n ≤ p\) y que \(p\) es primo.
Para demostrar que \(p\) es primo, por el lema L1, basta demostrar que
\[ n! + 1 ≠ 1 \]
Su demostración es
\begin{align}
&n ! > 0 &&\text{[por L2]} \\
&⟹ n ! + 1 > 1 &&\text{[por L3]} \\
&⟹ n ! + 1 ≠ 1 &&\text{[por L4]}
\end{align}
Para demostrar \(n ≤ p\), por el lema L5, basta demostrar que \(n ≱ p\). Su demostración es
\begin{align}
&n ≥ p \\
&⟹ p ∣ n! &&\text{[por L6 y L7]} \\
&⟹ p | 1 &&\text{[por L8 y L9]} \\
&⟹ Falso &&\text{[por L10 y \(p\) es primo]}
\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 |
import Mathlib.Tactic import Mathlib.Data.Nat.Prime open Nat -- 1ª demostración -- =============== example (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by let p := minFac (n ! + 1) have h1 : Nat.Prime p := by apply minFac_prime -- ⊢ n ! + 1 ≠ 1 have h3 : n ! > 0 := factorial_pos n have h4 : n ! + 1 > 1 := Nat.lt_add_of_pos_left h3 show n ! + 1 ≠ 1 exact Nat.ne_of_gt h4 use p constructor . -- ⊢ n ≤ p apply le_of_not_ge -- ⊢ ¬n ≥ p intro h5 -- h5 : n ≥ p -- ⊢ False have h6 : p ∣ n ! := dvd_factorial (minFac_pos _) h5 have h7 : p ∣ 1 := (Nat.dvd_add_iff_right h6).mpr (minFac_dvd _) show False exact (Nat.Prime.not_dvd_one h1) h7 . -- ⊢ Nat.Prime p exact h1 done -- 2ª demostración -- =============== example (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := exists_infinite_primes n -- Lemas usados -- ============ -- variable (k m n : ℕ) -- #check (Nat.Prime.not_dvd_one : Nat.Prime n → ¬n ∣ 1) -- #check (Nat.dvd_add_iff_right : k ∣ m → (k ∣ n ↔ k ∣ m + n)) -- #check (Nat.dvd_one : n ∣ 1 ↔ n = 1) -- #check (Nat.lt_add_of_pos_left : 0 < k → n < k + n) -- #check (Nat.ne_of_gt : k < n → n ≠ k) -- #check (dvd_factorial : 0 < k → k ≤ n → k ∣ n !) -- #check (factorial_pos n: n ! > 0) -- #check (le_of_not_ge : ¬k ≥ n → k ≤ n) -- #check (minFac_dvd n : minFac n ∣ n) -- #check (minFac_pos n : 0 < minFac n) -- #check (minFac_prime : n ≠ 1 → Nat.Prime (minFac n)) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
5. Si n² es par, entonces n es par
Demostrar con Lean4 que si \(n²\) es par, entonces \(n\) es par.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic open Nat variable (n : ℕ) example (h : 2 ∣ n ^ 2) : 2 ∣ n := by sorry |
1. Demostración en lenguaje natural
Se usará el siguiente lema: Si \(p\) es primo, entonces
\[ (∀ a, b ∈ ℕ)[p ∣ ab ↔ p ∣ a ∨ p ∣ b] \]
Si \(n²\) es par, entonces \(2\) divide a \(n.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 |
import Mathlib.Tactic open Nat variable (n : ℕ) -- 1ª demostración -- =============== example (h : 2 ∣ n ^ 2) : 2 ∣ n := by rw [pow_two] at h -- h : 2 ∣ n * n have h1 : Nat.Prime 2 := prime_two have h2 : 2 ∣ n ∨ 2 ∣ n := (Prime.dvd_mul h1).mp h rcases h2 with h3 | h4 · -- h3 : 2 ∣ n exact h3 · -- h4 : 2 ∣ n exact h4 done -- 2ª demostración -- =============== example (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 rcases h2 with h3 | h4 · exact h3 · exact h4 done -- 3ª demostración -- =============== example (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 done -- Lemas usados -- ============ -- variable (p a b : ℕ) -- #check (prime_two : Nat.Prime 2) -- #check (Prime.dvd_mul : Nat.Prime p → (p ∣ a * b ↔ p ∣ a ∨ p ∣ b)) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.