Pares ∪ Impares = Naturales
Los conjuntos de los números naturales, de los pares y de los impares se definen en Lean4 por
|
1 2 3 |
def Naturales : Set ℕ := {n | True} def Pares : Set ℕ := {n | Even n} def Impares : Set ℕ := {n | ¬Even n} |
Demostrar con Lean4 que
|
1 |
Pares ∪ Impares = Naturales |
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Nat.Parity open Set def Naturales : Set ℕ := {n | True} def Pares : Set ℕ := {n | Even n} def Impares : Set ℕ := {n | ¬Even n} example : Pares ∪ Impares = Naturales := by sorry |
1. Demostración en lenguaje natural
Tenemos que demostrar que
\[ \{n | \text{Even}(n)\} ∪ \{n | ¬\text{Even}(n)\} = \{n | \text{True}\} \]
es decir,
\[ n ∈ \{n | \text{Even}(n)\} ∪ \{n | ¬\text{Even}(n)\} ↔ n ∈ \{n | \text{True}\} \]
que se reduce a
\[ ⊢ \text{Even}(n) ∨ ¬\text{Even}(n) \]
que es una tautología.
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 |
import Mathlib.Data.Nat.Parity open Set def Naturales : Set ℕ := {n | True} def Pares : Set ℕ := {n | Even n} def Impares : Set ℕ := {n | ¬Even n} -- 1ª demostración -- =============== example : Pares ∪ Impares = Naturales := by unfold Pares Impares Naturales -- ⊢ {n | Even n} ∪ {n | ¬Even n} = {n | True} ext n -- ⊢ n ∈ {n | Even n} ∪ {n | ¬Even n} ↔ n ∈ {n | True} simp -- ⊢ Even n ∨ ¬Even n exact em (Even n) -- 2ª demostración -- =============== example : Pares ∪ Impares = Naturales := by unfold Pares Impares Naturales -- ⊢ {n | Even n} ∪ {n | ¬Even n} = {n | True} ext n -- ⊢ n ∈ {n | Even n} ∪ {n | ¬Even n} ↔ n ∈ {n | True} tauto |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
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 |
theory Union_de_pares_e_impares imports Main begin definition naturales :: "nat set" where "naturales = {n∈ℕ . True}" definition pares :: "nat set" where "pares = {n∈ℕ . even n}" definition impares :: "nat set" where "impares = {n∈ℕ . ¬ even n}" (* 1ª demostración *) lemma "pares ∪ impares = naturales" proof - have "∀ n ∈ ℕ . even n ∨ ¬ even n ⟷ True" by simp then have "{n ∈ ℕ. even n} ∪ {n ∈ ℕ. ¬ even n} = {n ∈ ℕ. True}" by auto then show "pares ∪ impares = naturales" by (simp add: naturales_def pares_def impares_def) qed (* 2ª demostración *) lemma "pares ∪ impares = naturales" unfolding naturales_def pares_def impares_def by auto end |
