Demostrar con Lean4 que en ℝ, si x²=1 entonces x=1 ó x=−1.
Para ello, completar la siguiente teoría de Lean4:
|
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
(∀x∈ℝ)[x–x=0](∀x,y∈ℝ)[xy=0→x=0∨y=0](∀x,y∈ℝ)[x–y=0↔x=y](∀x,y∈ℝ)[x+y=0→x=−y]
Se tiene que
(x–1)(x+1)=x²–1=1–1[por la hipótesis]=0[por L1]
y, por el lema L2, se tiene que
x–1=0∨x+1=0
Acabaremos la demostración por casos.
Primer caso:
x–1=0⟹x=1[por L3]⟹x=1∨x=−1
Segundo caso:
x+1=0⟹x=−1[por L4]⟹x=1∨x=−1
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
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 |