La semana en Calculemus (20 de enero de 2024)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. En ℝ, |x + y| ≤ |x| + |y|
- 2. En ℝ, si x ≠ 0 entonces x < 0 ó x > 0
- 3. Si m divide a n o a k, entonces m divide a nk
- 4. Si (∃ x, y ∈ ℝ)(z = x² + y² ∨ z = x² + y² + 1), entonces z ≥ 0
- 5. En ℝ, si x² = 1 entonces x = 1 ó x = -1
A continuación se muestran las soluciones.
1. En ℝ, |x + y| ≤ |x| + |y|
Demostrar con Lean4 que en \(ℝ\),
\[ |x + y| ≤ |x| + |y|\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example : |x + y| ≤ |x| + |y| := by sorry |
Demostración en lenguaje natural
Se usarán los siguientes lemas
\begin{align}
&(∀ x ∈ ℝ)[0 ≤ x → |x| = x) \tag{L1} \\
&(∀ a, b, c, d ∈ ℝ)[a ≤ b ∧ c ≤ d → a + c ≤ b + d] \tag{L2} \\
&(∀ x ∈ ℝ)[x ≤ |x|] \tag{L3} \\
&(∀ x ∈ ℝ)[x < 0 → |x| = -x] \tag{L4} \\
&(∀ x, y ∈ ℝ)[-(x + y) = -x + -y] \tag{L5} \\
&(∀ x ∈ ℝ)[-x ≤ |x|] \tag{L6}
\end{align}
Se demostrará por casos según \(x + y ≥ 0\):
Primer caso: Supongamos que \(x + y ≥ 0\). Entonces,
\begin{align}
|x + y| &= x + y &&\text{[por L1]} \\
&≤ |x| + |y| &&\text{[por L2 y L3]}
\end{align}
Segundo caso: Supongamos que \(x + y < 0\). Entonces,
\begin{align}
|x + y| &= -(x + y) &&\text{[por L4]} \\
&= -x + -y &&\text{[por L5]} \\
&≤ |x| + |y| &&\text{[por L2 y L6]}
\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 66 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} -- 1ª demostración -- =============== example : |x + y| ≤ |x| + |y| := by rcases le_or_gt 0 (x + y) with h1 | h2 · -- h1 : 0 ≤ x + y show |x + y| ≤ |x| + |y| calc |x + y| = x + y := by exact abs_of_nonneg h1 _ ≤ |x| + |y| := add_le_add (le_abs_self x) (le_abs_self y) . -- h2 : 0 > x + y show |x + y| ≤ |x| + |y| calc |x + y| = -(x + y) := by exact abs_of_neg h2 _ = -x + -y := by exact neg_add x y _ ≤ |x| + |y| := add_le_add (neg_le_abs_self x) (neg_le_abs_self y) -- 2ª demostración -- =============== example : |x + y| ≤ |x| + |y| := by rcases le_or_gt 0 (x + y) with h1 | h2 · -- h1 : 0 ≤ x + y rw [abs_of_nonneg h1] -- ⊢ x + y ≤ |x| + |y| exact add_le_add (le_abs_self x) (le_abs_self y) . -- h2 : 0 > x + y rw [abs_of_neg h2] -- ⊢ -(x + y) ≤ |x| + |y| calc -(x + y) = -x + -y := by exact neg_add x y _ ≤ |x| + |y| := add_le_add (neg_le_abs_self x) (neg_le_abs_self y) -- 2ª demostración -- =============== example : |x + y| ≤ |x| + |y| := by rcases le_or_gt 0 (x + y) with h1 | h2 · -- h1 : 0 ≤ x + y rw [abs_of_nonneg h1] -- ⊢ x + y ≤ |x| + |y| linarith [le_abs_self x, le_abs_self y] . -- h2 : 0 > x + y rw [abs_of_neg h2] -- ⊢ -(x + y) ≤ |x| + |y| linarith [neg_le_abs_self x, neg_le_abs_self y] -- 3ª demostración -- =============== example : |x + y| ≤ |x| + |y| := abs_add x y -- Lemas usados -- ============ -- variable (a b c d : ℝ) -- #check (abs_add x y : |x + y| ≤ |x| + |y|) -- #check (abs_of_neg : x < 0 → |x| = -x) -- #check (abs_of_nonneg : 0 ≤ x → |x| = x) -- #check (add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d) -- #check (le_abs_self a : a ≤ |a|) -- #check (le_or_gt x y : x ≤ y ∨ x > y) -- #check (neg_add x y : -(x + y) = -x + -y) -- #check (neg_le_abs_self x : -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. 38.
2. En ℝ, si x ≠ 0 entonces x < 0 ó x > 0
Demostrar con Lean4 que en ℝ, si \(x ≠ 0\) entonces \(x < 0\) ó \(x > 0\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable {x : ℝ} example (h : x ≠ 0) : x < 0 ∨ x > 0 := by sorry |
Demostración en lenguaje natural
Usando el siguiente lema
\[ (∀ x y ∈ ℝ)[x < y ∨ x = y ∨ y < x] \]
se demuestra distinguiendo tres casos.
Caso 1: Supongamos que \(x < 0\). Entonces, se verifica la disyunción ya
que se verifica su primera parte.
Caso 2: Supongamos que \(x = 0\). Entonces, se tiene una contradicción
con la hipótesis.
Caso 3: Supongamos que \(x > 0\). Entonces, se verifica la disyunción ya
que se verifica su segunda parte.
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 |
import Mathlib.Data.Real.Basic variable {x : ℝ} -- 1ª demostración -- =============== example (h : x ≠ 0) : x < 0 ∨ x > 0 := by rcases lt_trichotomy x 0 with hx1 | hx2 | hx3 . -- hx1 : x < 0 left -- ⊢ x < 0 exact hx1 . -- hx2 : x = 0 contradiction . -- hx3 : 0 < x right -- ⊢ x > 0 exact hx3 -- 2ª demostración -- =============== example (h : x ≠ 0) : x < 0 ∨ x > 0 := Ne.lt_or_lt h -- 3ª demostración -- =============== example (h : x ≠ 0) : x < 0 ∨ x > 0 := by aesop -- Lemas usados -- ============ -- variable (y : ℝ) -- #check (lt_trichotomy x y : x < y ∨ x = y ∨ y < x) |
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. Si m divide a n o a k, entonces m divide a nk
Demostrar con Lean4 que si \(m\) divide a \(n\) o a \(k\), entonces \(m\) divide a \(nk\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Tactic variable {m n k : ℕ} example (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by sorry |
Demostración en lenguaje natural
Se demuestra por casos.
Caso 1: Supongamos que \(m ∣ n\). Entonces, existe un \(a ∈ ℕ\) tal que
\[ n = ma \]
Por tanto,
\begin{align}
nk &= (ma)k \\
&= m(ak)
\end{align}
que es divisible por \(m\).
Caso 2: Supongamos que \(m ∣ k). Entonces, existe un \(b ∈ ℕ\) tal que
\[ k = mb \]
Por tanto,
\begin{align}
nk &= n(mb) \\
&= m(nb)
\end{align}
que es divisible por \(m\).
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 85 86 87 88 89 90 91 92 93 94 |
import Mathlib.Tactic variable {m n k : ℕ} -- 1ª demostración -- =============== example (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by rcases h with h1 | h2 . -- h1 : m ∣ n rcases h1 with ⟨a, ha⟩ -- a : ℕ -- ha : n = m * a rw [ha] -- ⊢ m ∣ (m * a) * k rw [mul_assoc] -- ⊢ m ∣ m * (a * k) exact dvd_mul_right m (a * k) . -- h2 : m ∣ k rcases h2 with ⟨b, hb⟩ -- b : ℕ -- hb : k = m * b rw [hb] -- ⊢ m ∣ n * (m * b) rw [mul_comm] -- ⊢ m ∣ (m * b) * n rw [mul_assoc] -- ⊢ m ∣ m * (b * n) exact dvd_mul_right m (b * n) -- 2ª demostración -- =============== example (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by rcases h with h1 | h2 . -- h1 : m ∣ n rcases h1 with ⟨a, ha⟩ -- a : ℕ -- ha : n = m * a rw [ha, mul_assoc] -- ⊢ m ∣ m * (a * k) exact dvd_mul_right m (a * k) . -- h2 : m ∣ k rcases h2 with ⟨b, hb⟩ -- b : ℕ -- hb : k = m * b rw [hb, mul_comm, mul_assoc] -- ⊢ m ∣ m * (b * n) exact dvd_mul_right m (b * n) -- 3ª demostración -- =============== example (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by rcases h with ⟨a, rfl⟩ | ⟨b, rfl⟩ . -- a : ℕ -- ⊢ m ∣ (m * a) * k rw [mul_assoc] -- ⊢ m ∣ m * (a * k) exact dvd_mul_right m (a * k) . -- ⊢ m ∣ n * (m * b) rw [mul_comm, mul_assoc] -- ⊢ m ∣ m * (b * n) exact dvd_mul_right m (b * n) -- 4ª demostración -- =============== example (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by rcases h with h1 | h2 . -- h1 : m ∣ n exact dvd_mul_of_dvd_left h1 k . -- h2 : m ∣ k exact dvd_mul_of_dvd_right h2 n -- Lemas usados -- ============ -- #check (dvd_mul_of_dvd_left : m ∣ n → ∀ (c : ℕ), m ∣ n * c) -- #check (dvd_mul_of_dvd_right : m ∣ n → ∀ (c : ℕ), m ∣ c * n) -- #check (dvd_mul_right m n : m ∣ m * n) -- #check (mul_assoc m n k : m * n * k = m * (n * k)) -- #check (mul_comm m n : m * n = n * m) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 39.
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 |
theory CS_de_divisibilidad_del_producto imports Main begin (* 1ª demostración *) lemma fixes n m k :: nat assumes "m dvd n ∨ m dvd k" shows "m dvd (n * k)" using assms proof assume "m dvd n" then obtain a where "n = m * a" by auto then have "n * k = m * (a * k)" by simp then show ?thesis by auto next assume "m dvd k" then obtain b where "k = m * b" by auto then have "n * k = m * (n * b)" by simp then show ?thesis by auto qed (* 2ª demostración *) lemma fixes n m k :: nat assumes "m dvd n ∨ m dvd k" shows "m dvd (n * k)" using assms by auto end |
4. Si (∃ x, y ∈ ℝ)[z = x² + y² ∨ z = x² + y² + 1], entonces z ≥ 0
Demostrar con Lean4 que si \((∃ x, y ∈ ℝ)[z = x² + y² ∨ z = x² + y² + 1]\), entonces \(z ≥ 0\).
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 {z : ℝ} example (h : ∃ x y, z = x^2 + y^2 ∨ z = x^2 + y^2 + 1) : z ≥ 0 := by sorry |
Demostración en lenguaje natural
Usaremos los siguientes lemas
\begin{align}
&(∀ x ∈ ℝ)[x² ≥ 0] \tag{L1} \\
&(∀ x, y ∈ ℝ)[x ≥ 0 → y ≥ 0 → x + y ≥ 0] \tag{L2} \\
&1 ≥ 0 \tag{L3}
\end{align}
Sean \(a\) y \(b\) tales que
\[ z = a² + b² ∨ z = a² + b² + 1 \]
Entonces, por L1, se tiene que
\begin{align}
&a² ≥ 0 \tag{1} \\
&b² ≥ 0 \tag{2}
\end{align}
En el primer caso, \(z = a² + b²\) y se tiene que \(z ≥ 0\) por el lema L2 aplicado a (1) y (2).
En el segundo caso, \(z = a² + b² + 1\) y se tiene que \(z ≥ 0\) por el lema L2 aplicado a (1), (2) y L3.
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 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {z : ℝ} -- 1ª demostración -- =============== example (h : ∃ x y, z = x^2 + y^2 ∨ z = x^2 + y^2 + 1) : z ≥ 0 := by rcases h with ⟨a, b, h1⟩ -- a b : ℝ -- h1 : z = a ^ 2 + b ^ 2 ∨ z = a ^ 2 + b ^ 2 + 1 have h2 : a ^ 2 ≥ 0 := pow_two_nonneg a have h3 : b ^ 2 ≥ 0 := pow_two_nonneg b have h4 : a ^ 2 + b ^ 2 ≥ 0 := add_nonneg h2 h3 rcases h1 with h5 | h6 . -- h5 : z = a ^ 2 + b ^ 2 show z ≥ 0 calc z = a ^ 2 + b ^ 2 := h5 _ ≥ 0 := add_nonneg h2 h3 . -- h6 : z = a ^ 2 + b ^ 2 + 1 show z ≥ 0 calc z = (a ^ 2 + b ^ 2) + 1 := h6 _ ≥ 0 := add_nonneg h4 zero_le_one -- 2ª demostración -- =============== example (h : ∃ x y, z = x^2 + y^2 ∨ z = x^2 + y^2 + 1) : z ≥ 0 := by rcases h with ⟨a, b, h1 | h2⟩ . -- h1 : z = a ^ 2 + b ^ 2 have h1a : a ^ 2 ≥ 0 := pow_two_nonneg a have h1b : b ^ 2 ≥ 0 := pow_two_nonneg b show z ≥ 0 calc z = a ^ 2 + b ^ 2 := h1 _ ≥ 0 := add_nonneg h1a h1b . -- h2 : z = a ^ 2 + b ^ 2 + 1 have h2a : a ^ 2 ≥ 0 := pow_two_nonneg a have h2b : b ^ 2 ≥ 0 := pow_two_nonneg b have h2c : a ^ 2 + b ^ 2 ≥ 0 := add_nonneg h2a h2b show z ≥ 0 calc z = (a ^ 2 + b ^ 2) + 1 := h2 _ ≥ 0 := add_nonneg h2c zero_le_one -- 3ª demostración -- =============== example (h : ∃ x y, z = x^2 + y^2 ∨ z = x^2 + y^2 + 1) : z ≥ 0 := by rcases h with ⟨a, b, h1 | h2⟩ . -- h1 : z = a ^ 2 + b ^ 2 rw [h1] -- ⊢ a ^ 2 + b ^ 2 ≥ 0 apply add_nonneg . -- ⊢ 0 ≤ a ^ 2 apply pow_two_nonneg . -- ⊢ 0 ≤ b ^ 2 apply pow_two_nonneg . -- h2 : z = a ^ 2 + b ^ 2 + 1 rw [h2] -- ⊢ a ^ 2 + b ^ 2 + 1 ≥ 0 apply add_nonneg . -- ⊢ 0 ≤ a ^ 2 + b ^ 2 apply add_nonneg . -- ⊢ 0 ≤ a ^ 2 apply pow_two_nonneg . -- ⊢ 0 ≤ b ^ 2 apply pow_two_nonneg . -- ⊢ 0 ≤ 1 exact zero_le_one -- 4ª demostración -- =============== example (h : ∃ x y, z = x^2 + y^2 ∨ z = x^2 + y^2 + 1) : z ≥ 0 := by rcases h with ⟨a, b, rfl | rfl⟩ . -- ⊢ a ^ 2 + b ^ 2 ≥ 0 apply add_nonneg . -- ⊢ 0 ≤ a ^ 2 apply pow_two_nonneg . -- ⊢ 0 ≤ b ^ 2 apply pow_two_nonneg . -- ⊢ a ^ 2 + b ^ 2 + 1 ≥ 0 apply add_nonneg . -- ⊢ 0 ≤ a ^ 2 + b ^ 2 apply add_nonneg . -- ⊢ 0 ≤ a ^ 2 apply pow_two_nonneg . -- ⊢ 0 ≤ b ^ 2 apply pow_two_nonneg . -- ⊢ 0 ≤ 1 exact zero_le_one -- 5ª demostración -- =============== example (h : ∃ x y, z = x^2 + y^2 ∨ z = x^2 + y^2 + 1) : z ≥ 0 := by rcases h with ⟨a, b, rfl | rfl⟩ . -- ⊢ a ^ 2 + b ^ 2 ≥ 0 nlinarith . -- ⊢ a ^ 2 + b ^ 2 + 1 ≥ 0 nlinarith -- 6ª demostración -- =============== example (h : ∃ x y, z = x^2 + y^2 ∨ z = x^2 + y^2 + 1) : z ≥ 0 := by rcases h with ⟨a, b, rfl | rfl⟩ <;> nlinarith -- Lemas usados -- ============ -- variable (x y : ℝ) -- #check (add_nonneg : 0 ≤ x → 0 ≤ y → 0 ≤ x + y) -- #check (pow_two_nonneg x : 0 ≤ x ^ 2) -- #check (zero_le_one : 0 ≤ 1) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 39.
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 |
theory Desigualdad_con_rcases imports Main "HOL.Real" begin (* 1ª demostración *) lemma assumes "∃x y :: real. (z = x^2 + y^2 ∨ z = x^2 + y^2 + 1)" shows "z ≥ 0" proof - obtain x y where hxy: "z = x^2 + y^2 ∨ z = x^2 + y^2 + 1" using assms by auto { assume "z = x^2 + y^2" have "x^2 + y^2 ≥ 0" by simp then have "z ≥ 0" using `z = x^2 + y^2` by simp } { assume "z = x^2 + y^2 + 1" have "x^2 + y^2 ≥ 0" by simp then have "z ≥ 1" using `z = x^2 + y^2 + 1` by simp } with hxy show "z ≥ 0" by auto qed (* 2ª demostración *) lemma assumes "∃x y :: real. (z = x^2 + y^2 ∨ z = x^2 + y^2 + 1)" shows "z ≥ 0" proof - obtain x y where hxy: "z = x^2 + y^2 ∨ z = x^2 + y^2 + 1" using assms by auto with hxy show "z ≥ 0" by auto qed (* 3ª demostración *) lemma assumes "∃x y :: real. (z = x^2 + y^2 ∨ z = x^2 + y^2 + 1)" shows "z ≥ 0" using assms by fastforce end |
5. En ℝ, si x² = 1 entonces x = 1 ó x = -1
Demostrar con Lean4 que en \(ℝ\), si \(x² = 1\) entonces \(x = 1\) ó \(x = -1\).
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 = 1) : x = 1 ∨ x = -1 := by sorry |
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 – 1)(x + 1) &= x² – 1 \\
&= 1 – 1 &&\text{[por la hipótesis]} \\
&= 0 &&\text{[por L1]}
\end{align}
y, por el lema L2, se tiene que
\[ x – 1 = 0 ∨ x + 1 = 0 \]
Acabaremos la demostración por casos.
Primer caso:
\begin{align}
x – 1 = 0 &⟹ x = 1 &&\text{[por L3]} \\
&⟹ x = 1 ∨ x = -1
\end{align}
Segundo caso:
\begin{align}
x + 1 = 0 &⟹ x = -1 &&\text{[por L4]} \\
&⟹ x = 1 ∨ x = -1
\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 66 67 68 69 |
import Mathlib.Data.Real.Basic variable (x y : ℝ) -- 1ª demostración -- =============== example (h : x^2 = 1) : x = 1 ∨ x = -1 := by have h1 : (x - 1) * (x + 1) = 0 := by calc (x - 1) * (x + 1) = x^2 - 1 := by ring _ = 1 - 1 := by rw [h] _ = 0 := sub_self 1 have h2 : x - 1 = 0 ∨ x + 1 = 0 := by apply eq_zero_or_eq_zero_of_mul_eq_zero h1 rcases h2 with h3 | h4 . -- h3 : x - 1 = 0 left -- ⊢ x = 1 exact sub_eq_zero.mp h3 . -- h4 : x + 1 = 0 right -- ⊢ x = -1 exact eq_neg_of_add_eq_zero_left h4 -- 2ª demostración -- =============== example (h : x^2 = 1) : x = 1 ∨ x = -1 := by have h1 : (x - 1) * (x + 1) = 0 := by nlinarith have h2 : x - 1 = 0 ∨ x + 1 = 0 := by aesop rcases h2 with h3 | h4 . -- h3 : x - 1 = 0 left -- ⊢ x = 1 linarith . -- h4 : x + 1 = 0 right -- ⊢ x = -1 linarith -- 3ª demostración -- =============== example (h : x^2 = 1) : x = 1 ∨ x = -1 := sq_eq_one_iff.mp h -- 3ª demostración -- =============== example (h : x^2 = 1) : x = 1 ∨ x = -1 := by aesop -- 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_one_iff : x ^ 2 = 1 ↔ x = 1 ∨ x = -1) -- #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.
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 |