La semana en Calculemus (10 de diciembre de 2023)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. P → ¬¬P
- 2. Si f no está acotada superiormente, entonces (∀a)(∃x)(f(x) > a)
- 3. Si ¬(∀a)(∃x)(f(x) > a), entonces f está acotada superiormente
- 4. Si f no es monótona, entonces ∃x∃y(x ≤ y ∧ f(y) < f(x))
- 5. Si 0 < 0, entonces a > 37 para cualquier número a
A continuación se muestran las soluciones.
1. P → ¬¬P
Demostrar con Lean4 que \(P → ¬¬P\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Tactic variable (P : Prop) example (h : P) : ¬¬P := by sorry |
Demostración en lenguaje natural
Supongamos \(¬P\). Entonces, tenemos una contradicción con la hipótesis (\(P\)).
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.Tactic variable (P : Prop) -- 1ª demostración -- =============== example (h : P) : ¬¬P := by intro h1 -- h1 : ¬P -- ⊢ False exact (h1 h) -- 2ª demostración -- =============== example (h : P) : ¬¬P := fun h1 ↦ h1 h -- 3ª demostración -- =============== example (h : P) : ¬¬P := not_not_intro h -- 4ª demostración -- =============== example (h : P) : ¬ ¬ P := by tauto -- Lemas usados -- ============ -- #check (not_not_intro : P → ¬¬P) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 33.
2. Si f no está acotada superiormente, entonces (∀a)(∃x)[f(x) > a]
Demostrar con Lean4 que si \(f\) no está acotada superiormente, entonces \((∀a)(∃x)[f(x) > a]\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import Mathlib.Data.Real.Basic def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def acotadaSup (f : ℝ → ℝ) := ∃ a, CotaSuperior f a variable (f : ℝ → ℝ) example (h : ¬acotadaSup f) : ∀ a, ∃ x, f x > a := by sorry |
Demostración en lenguaje natural
1ª demostración en LN
Usaremos los siguientes lemas
\begin{align}
&¬(∃x)P(x) → (∀x)¬P(x) \tag{L1} \\
&¬a > b → a ≤ b \tag{L2}
\end{align}
Sea \(a ∈ ℝ\). Tenemos que demostrar que
\[ (∃x)[f(x) > a] \]
Lo haremos por reducción al absurdo. Para ello, suponemos que
\[ ¬(∃x)[f(x) > a] \tag{1} \]
y tenemos que obtener una contradicción. Aplicando L1 a (1) se tiene
\[ (∀x)[¬ f(x) > a] \]
y, aplicando L2, se tiene
\[ (∀x)[f(x) ≤ a] \]
Lo que significa que \(a\) es una cota superior de \(f\) y, por tanto \(f\) está acotada superiormente, en cotradicción con la hipótesis.
2ª demostración en LN
Por la contrarecíproca, se supone que
\[ ¬(∀a)(∃x)[f(x) > a] \tag{1} \]
y tenemos que demostrar que \(f\) está acotada superiormente.
Interiorizando la negación en (1) y simplificando, se tiene que
\[ (∃a)(∀x)[f x ≤ a] \]
que es lo que teníamos que demostrar.
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 def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def acotadaSup (f : ℝ → ℝ) := ∃ a, CotaSuperior f a variable (f : ℝ → ℝ) -- 1ª demostración -- =============== example (h : ¬acotadaSup f) : ∀ a, ∃ x, f x > a := by intro a -- a : ℝ -- ⊢ ∃ x, f x > a by_contra h1 -- h1 : ¬∃ x, f x > a -- ⊢ False have h2 : ∀ x, ¬ f x > a := forall_not_of_not_exists h1 have h3 : ∀ x, f x ≤ a := by intro x have h3a : ¬ f x > a := h2 x show f x ≤ a exact le_of_not_gt h3a have h4 : CotaSuperior f a := h3 have h5 : ∃ b, CotaSuperior f b := ⟨a, h4⟩ have h6 : acotadaSup f := h5 show False exact h h6 -- 2ª demostración -- =============== example (h : ¬acotadaSup f) : ∀ a, ∃ x, f x > a := by intro a -- a : ℝ -- ⊢ ∃ x, f x > a by_contra h1 -- h1 : ¬∃ x, f x > a -- ⊢ False apply h -- ⊢ acotadaSup f use a -- ⊢ CotaSuperior f a intro x -- x : ℝ -- ⊢ f x ≤ a apply le_of_not_gt -- ⊢ ¬f x > a intro h2 -- h2 : f x > a -- ⊢ False apply h1 -- ⊢ ∃ x, f x > a use x -- ⊢ f x > a exact h2 -- 3ª demostración -- =============== example (h : ¬acotadaSup f) : ∀ a, ∃ x, f x > a := by unfold acotadaSup at h -- h : ¬∃ a, CotaSuperior f a unfold CotaSuperior at h -- h : ¬∃ a, ∀ (x : ℝ), f x ≤ a push_neg at h -- ∀ (a : ℝ), ∃ x, f x > a exact h -- 4ª demostración -- =============== example (h : ¬acotadaSup f) : ∀ a, ∃ x, f x > a := by simp only [acotadaSup, CotaSuperior] at h -- h : ¬∃ a, ∀ (x : ℝ), f x ≤ a push_neg at h -- ∀ (a : ℝ), ∃ x, f x > a exact h -- 5ª demostración -- =============== example (h : ¬acotadaSup f) : ∀ a, ∃ x, f x > a := by contrapose h -- h : ¬∀ (a : ℝ), ∃ x, f x > a -- ⊢ ¬¬acotadaSup f push_neg at * -- h : ∃ a, ∀ (x : ℝ), f x ≤ a -- ⊢ acotadaSup f exact h -- 6ª demostración -- =============== example (h : ¬acotadaSup f) : ∀ a, ∃ x, f x > a := by contrapose! h -- h : ∃ a, ∀ (x : ℝ), f x ≤ a -- ⊢ acotadaSup f exact h -- Lemas usados -- ============ -- variable {α : Type _} -- variable (P : α → Prop) -- #check (forall_not_of_not_exists : (¬∃ x, P x) → ∀ x, ¬P x) -- -- variable (a b : ℝ) -- #check (le_of_not_gt : ¬a > b → 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. 33.
3. Si ¬(∀a)(∃x)[f(x) > a], entonces f está acotada superiormente
Demostrar con Lean4 que si \(¬(∀a)(∃x)[f(x) > a]\), entonces \(f\) está acotada superiormente.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import Mathlib.Data.Real.Basic def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def acotadaSup (f : ℝ → ℝ) := ∃ a, CotaSuperior f a variable (f : ℝ → ℝ) example (h : ¬∀ a, ∃ x, f x > a) : acotadaSup f := by sorry |
Demostración en lenguaje natural
Tenemos que demostrar que \(f\) es acotada superiormente; es decir, que
\[ (∃a)(∀x)[f(x) ≤ a] \]
que es exactamente la fórmula obtenida interiorizando la negación en la hipótesis.
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 |
import Mathlib.Data.Real.Basic def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def acotadaSup (f : ℝ → ℝ) := ∃ a, CotaSuperior f a variable (f : ℝ → ℝ) -- 1ª demostración -- =============== example (h : ¬∀ a, ∃ x, f x > a) : acotadaSup f := by unfold acotadaSup -- ⊢ ∃ a, CotaSuperior f a unfold CotaSuperior -- ⊢ ∃ a, ∀ (x : ℝ), f x ≤ a push_neg at h -- h : ∃ a, ∀ (x : ℝ), f x ≤ a exact h -- 2ª demostración -- =============== example (h : ¬∀ a, ∃ x, f x > a) : acotadaSup f := by unfold acotadaSup CotaSuperior -- ⊢ ∃ a, ∀ (x : ℝ), f x ≤ a push_neg at h -- h : ∃ a, ∀ (x : ℝ), f x ≤ a exact h -- 3ª demostración -- =============== example (h : ¬∀ a, ∃ x, f x > a) : acotadaSup f := by push_neg at h -- h : ∃ a, ∀ (x : ℝ), f x ≤ a exact h |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 34.
4. Si f no es monótona, entonces ∃x∃y[x ≤ y ∧ f(y) < f(x)]
Demostrar con Lean4 que si \(f\) no es monótona, entonces \(∃x∃y[x ≤ y ∧ f(y) < f(x)]\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Tactic variable (f : ℝ → ℝ) example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by sorry |
Demostración en lenguaje natural
Usaremos los siguientes lemas:
\begin{align}
&¬(∀x)P(x) ↔ (∃ x)¬P(x) \tag{L1} \\
&¬(p → q) ↔ p ∧ ¬q \tag{L2} \\
&(∀a, b ∈ ℝ)[¬b ≤ a → a < b] \tag{L3}
\end{align}
Por la definición de función monótona,
\[ ¬(∀x)(∀y)[x ≤ y → f(x) ≤ f(y)] \]
Aplicando L1 se tiene
\[ (∃x)¬(∀y)[x ≤ y → f(x) ≤ f(y)] \]
Sea \(a\) tal que
\[ ¬(∀y)[a ≤ y → f(a) ≤ f(y)] \]
Aplicando L1 se tiene
\[ (∃y)¬[a ≤ y → f(a) ≤ f(y)] \]
Sea \(b\) tal que
\[ ¬[a ≤ b → f(a) ≤ f(b)] \]
Aplicando L2 se tiene que
\[ a ≤ b ∧ ¬(f(a) ≤ f(b)) \]
Aplicando L3 se tiene que
\[ a ≤ b ∧ f(b) < f(a) \]
Por tanto,
\[ (∃x,y)[x ≤ y ∧ f(y) < f(x)] \]
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 |
import Mathlib.Tactic variable (f : ℝ → ℝ) -- 1ª demostración -- =============== example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by have h1 : ¬∀ x y, x ≤ y → f x ≤ f y := h have h2 : ∃ x, ¬(∀ y, x ≤ y → f x ≤ f y) := not_forall.mp h1 rcases h2 with ⟨a, ha : ¬∀ y, a ≤ y → f a ≤ f y⟩ have h3 : ∃ y, ¬(a ≤ y → f a ≤ f y) := not_forall.mp ha rcases h3 with ⟨b, hb : ¬(a ≤ b → f a ≤ f b)⟩ have h4 : a ≤ b ∧ ¬(f a ≤ f b) := not_imp.mp hb have h5 : a ≤ b ∧ f b < f a := ⟨h4.1, lt_of_not_le h4.2⟩ use a, b -- ⊢ a ≤ b ∧ f b < f a exact h5 -- 2ª demostración -- =============== example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by simp only [Monotone] at h -- h : ¬∀ ⦃a b : ℝ⦄, a ≤ b → f a ≤ f b push_neg at h -- h : Exists fun ⦃a⦄ => Exists fun ⦃b⦄ => a ≤ b ∧ f b < f a exact h -- Lemas usados -- ============ -- variable {α : Type _} -- variable (P : α → Prop) -- variable (p q : Prop) -- variable (a b : ℝ) -- #check (not_forall : (¬∀ x, P x) ↔ ∃ x, ¬P x) -- #check (not_imp : ¬(p → q) ↔ p ∧ ¬q) -- #check (lt_of_not_le : ¬b ≤ a → 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. 34.
5. Si 0 < 0, entonces a > 37 para cualquier número a
Demostrar con Lean4 que si \(0 < 0\), entonces \(a > 37\) para cualquier número \(a\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic variable (a : ℕ) example (h : 0 < 0) : a > 37 := by sorry |
Demostración en lenguaje natural
Basta demostrar una contradicción, ya que de una contradicción se sigue cualquier cosa.
La hipótesis es una contradicción con la propiedad irreflexiva de la relación \(<\).
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.Tactic variable (a : ℕ) -- 1ª demostración -- =============== example (h : 0 < 0) : a > 37 := by exfalso -- ⊢ False show False exact lt_irrefl 0 h -- 2ª demostración -- =============== example (h : 0 < 0) : a > 37 := by exfalso -- ⊢ False apply lt_irrefl 0 h -- 3ª demostración -- =============== example (h : 0 < 0) : a > 37 := absurd h (lt_irrefl 0) -- 4ª demostración -- =============== example (h : 0 < 0) : a > 37 := by have : ¬ 0 < 0 := lt_irrefl 0 contradiction -- 5ª demostración -- =============== example (h : 0 < 0) : a > 37 := by linarith -- Lemas usados -- ============ -- variable (p q : Prop) -- #check (lt_irrefl a : ¬a < a) -- #check (absurd : p → ¬p → q) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 34.