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:
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} \newline &(∀ x, y ∈ ℝ)[x ≥ 0 → y ≥ 0 → x + y ≥ 0] \tag{L2} \newline &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} \newline &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
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
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