Los primos mayores que 2 son impares

Los números primos, los mayores que 2 y los impares se definen en Lean4 por

   def Primos      : Set ℕ := {n | Nat.Prime n}
   def MayoresQue2 : Set ℕ := {n | n > 2}
   def Impares     : Set ℕ := {n | ¬Even n}

def Primos : Set ℕ := {n | Nat.Prime n}

def MayoresQue2 : Set ℕ := {n | n > 2}

def Impares : Set ℕ := {n | ¬Even n}

Demostrar con Lean4 que

   Primos ∩ MayoresQue2 ⊆ Impares

1	Primos ∩ MayoresQue2 ⊆ Impares

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Nat.Parity
import Mathlib.Data.Nat.Prime
import Mathlib.Tactic

open Nat

def Primos      : Set ℕ := {n | Nat.Prime n}
def MayoresQue2 : Set ℕ := {n | n > 2}
def Impares     : Set ℕ := {n | ¬Even n}

example : Primos ∩ MayoresQue2 ⊆ Impares :=
by sorry

import Mathlib.Data.Nat.Parity

import Mathlib.Data.Nat.Prime

import Mathlib.Tactic

open Nat

def Primos : Set ℕ := {n | Nat.Prime n}

def MayoresQue2 : Set ℕ := {n | n > 2}

def Impares : Set ℕ := {n | ¬Even n}

example : Primos ∩ MayoresQue2 ⊆ Impares :=

by sorry

1. Demostraciones con Lean4

import Mathlib.Data.Nat.Parity
import Mathlib.Data.Nat.Prime
import Mathlib.Tactic

open Nat

def Primos      : Set ℕ := {n | Nat.Prime n}
def MayoresQue2 : Set ℕ := {n | n > 2}
def Impares     : Set ℕ := {n | ¬Even n}

-- 1ª demostración
-- ===============

example : Primos ∩ MayoresQue2 ⊆ Impares :=
by
  unfold Primos MayoresQue2 Impares
  -- ⊢ {n | Nat.Prime n} ∩ {n | n > 2} ⊆ {n | ¬Even n}
  intro n
  -- n : ℕ
  -- ⊢ n ∈ {n | Nat.Prime n} ∩ {n | n > 2} → n ∈ {n | ¬Even n}
  simp
  -- ⊢ Nat.Prime n → 2 < n → ¬Even n
  intro hn
  -- hn : Nat.Prime n
  -- ⊢ 2 < n → ¬Even n
  rcases Prime.eq_two_or_odd hn with (h | h)
  . -- h : n = 2
    rw [h]
    -- ⊢ 2 < 2 → ¬Even 2
    intro h1
    -- h1 : 2 < 2
    -- ⊢ ¬Even 2
    exfalso
    exact absurd h1 (lt_irrefl 2)
  . -- h : n % 2 = 1
    rw [even_iff]
    -- ⊢ 2 < n → ¬n % 2 = 0
    rw [h]
    -- ⊢ 2 < n → ¬1 = 0
    intro
    -- a : 2 < n
    -- ⊢ ¬1 = 0
    exact one_ne_zero

-- 2ª demostración
-- ===============

example : Primos ∩ MayoresQue2 ⊆ Impares :=
by
  unfold Primos MayoresQue2 Impares
  -- ⊢ {n | Nat.Prime n} ∩ {n | n > 2} ⊆ {n | ¬Even n}
  rintro n ⟨h1, h2⟩
  -- n : ℕ
  -- h1 : n ∈ {n | Nat.Prime n}
  -- h2 : n ∈ {n | n > 2}
  -- ⊢ n ∈ {n | ¬Even n}
  simp at *
  -- h1 : Nat.Prime n
  -- h2 : 2 < n
  -- ⊢ ¬Even n
  rcases Prime.eq_two_or_odd h1 with (h3 | h4)
  . -- h3 : n = 2
    rw [h3] at h2
    -- h2 : 2 < 2
    exfalso
    -- ⊢ False
    exact absurd h2 (lt_irrefl 2)
  . -- h4 : n % 2 = 1
    rw [even_iff]
    -- ⊢ ¬n % 2 = 0
    rw [h4]
    -- ⊢ ¬1 = 0
    exact one_ne_zero

-- 3ª demostración
-- ===============

example : Primos ∩ MayoresQue2 ⊆ Impares :=
by
  unfold Primos MayoresQue2 Impares
  -- ⊢ {n | Nat.Prime n} ∩ {n | n > 2} ⊆ {n | ¬Even n}
  rintro n ⟨h1, h2⟩
  -- n : ℕ
  -- h1 : n ∈ {n | Nat.Prime n}
  -- h2 : n ∈ {n | n > 2}
  -- ⊢ n ∈ {n | ¬Even n}
  simp at *
  -- h1 : Nat.Prime n
  -- h2 : 2 < n
  -- ⊢ ¬Even n
  rcases Prime.eq_two_or_odd h1 with (h3 | h4)
  . -- h3 : n = 2
    rw [h3] at h2
    -- h2 : 2 < 2
    linarith
  . -- h4 : n % 2 = 1
    rw [even_iff]
    -- ⊢ ¬n % 2 = 0
    linarith

-- Lemas usados
-- ============

-- variable (p n : ℕ)
-- variable (a b : Prop)
-- #check (Prime.eq_two_or_odd : Nat.Prime p → p = 2 ∨ p % 2 = 1)
-- #check (absurd : a → ¬a → b)
-- #check (even_iff : Even n ↔ n % 2 = 0)
-- #check (lt_irrefl n : ¬n < n)
-- #check (one_ne_zero : 1 ≠ 0)

100

101

102

103

104

105

106

107

108

109

110

import Mathlib.Data.Nat.Parity

import Mathlib.Data.Nat.Prime

import Mathlib.Tactic

open Nat

def Primos : Set ℕ := {n | Nat.Prime n}

def MayoresQue2 : Set ℕ := {n | n > 2}

def Impares : Set ℕ := {n | ¬Even n}

-- 1ª demostración

-- ===============

example : Primos ∩ MayoresQue2 ⊆ Impares :=

unfold Primos MayoresQue2 Impares

-- ⊢ {n | Nat.Prime n} ∩ {n | n > 2} ⊆ {n | ¬Even n}

intro n

-- n : ℕ

-- ⊢ n ∈ {n | Nat.Prime n} ∩ {n | n > 2} → n ∈ {n | ¬Even n}

simp

-- ⊢ Nat.Prime n → 2 < n → ¬Even n

intro hn

-- hn : Nat.Prime n

-- ⊢ 2 < n → ¬Even n

rcases Prime.eq_two_or_odd hn with (h | h)

. -- h : n = 2

rw [h]

-- ⊢ 2 < 2 → ¬Even 2

intro h1

-- h1 : 2 < 2

-- ⊢ ¬Even 2

exfalso

exact absurd h1 (lt_irrefl 2)

. -- h : n % 2 = 1

rw [even_iff]

-- ⊢ 2 < n → ¬n % 2 = 0

rw [h]

-- ⊢ 2 < n → ¬1 = 0

intro

-- a : 2 < n

-- ⊢ ¬1 = 0

exact one_ne_zero

-- 2ª demostración

-- ===============

example : Primos ∩ MayoresQue2 ⊆ Impares :=

unfold Primos MayoresQue2 Impares

-- ⊢ {n | Nat.Prime n} ∩ {n | n > 2} ⊆ {n | ¬Even n}

rintro n ⟨h1, h2⟩

-- n : ℕ

-- h1 : n ∈ {n | Nat.Prime n}

-- h2 : n ∈ {n | n > 2}

-- ⊢ n ∈ {n | ¬Even n}

simp at *

-- h1 : Nat.Prime n

-- h2 : 2 < n

-- ⊢ ¬Even n

rcases Prime.eq_two_or_odd h1 with (h3 | h4)

. -- h3 : n = 2

rw [h3] at h2

-- h2 : 2 < 2

exfalso

-- ⊢ False

exact absurd h2 (lt_irrefl 2)

. -- h4 : n % 2 = 1

rw [even_iff]

-- ⊢ ¬n % 2 = 0

rw [h4]

-- ⊢ ¬1 = 0

exact one_ne_zero

-- 3ª demostración

-- ===============

example : Primos ∩ MayoresQue2 ⊆ Impares :=

unfold Primos MayoresQue2 Impares

-- ⊢ {n | Nat.Prime n} ∩ {n | n > 2} ⊆ {n | ¬Even n}

rintro n ⟨h1, h2⟩

-- n : ℕ

-- h1 : n ∈ {n | Nat.Prime n}

-- h2 : n ∈ {n | n > 2}

-- ⊢ n ∈ {n | ¬Even n}

simp at *

-- h1 : Nat.Prime n

-- h2 : 2 < n

-- ⊢ ¬Even n

rcases Prime.eq_two_or_odd h1 with (h3 | h4)

. -- h3 : n = 2

rw [h3] at h2

-- h2 : 2 < 2

linarith

. -- h4 : n % 2 = 1

rw [even_iff]

-- ⊢ ¬n % 2 = 0

linarith

-- Lemas usados

-- ============

-- variable (p n : ℕ)

-- variable (a b : Prop)

-- #check (Prime.eq_two_or_odd : Nat.Prime p → p = 2 ∨ p % 2 = 1)

-- #check (absurd : a → ¬a → b)

-- #check (even_iff : Even n ↔ n % 2 = 0)

-- #check (lt_irrefl n : ¬n < n)

-- #check (one_ne_zero : 1 ≠ 0)

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3. Demostraciones con Isabelle/HOL

theory Interseccion_de_los_primos_y_los_mayores_que_dos
imports Main "HOL-Number_Theory.Number_Theory"
begin

definition primos :: "nat set" where
  "primos = {n ∈ ℕ . prime n}"

definition mayoresQue2 :: "nat set" where
  "mayoresQue2 = {n ∈ ℕ . n > 2}"

definition impares :: "nat set" where
  "impares = {n ∈ ℕ . ¬ even n}"

(* 1ª demostración *)
lemma "primos ∩ mayoresQue2 ⊆ impares"
proof
  fix x
  assume "x ∈ primos ∩ mayoresQue2"
  then have "x ∈ ℕ ∧ prime x ∧ 2 < x"
    by (simp add: primos_def mayoresQue2_def)
  then have "x ∈ ℕ ∧ odd x"
    by (simp add: prime_odd_nat)
  then show "x ∈ impares"
    by (simp add: impares_def)
qed

(* 2ª demostración *)
lemma "primos ∩ mayoresQue2 ⊆ impares"
  unfolding primos_def mayoresQue2_def impares_def
  by (simp add: Collect_mono_iff Int_def prime_odd_nat)

(* 3ª demostración *)
lemma "primos ∩ mayoresQue2 ⊆ impares"
  unfolding primos_def mayoresQue2_def impares_def
  by (auto simp add: prime_odd_nat)

end

theory Interseccion_de_los_primos_y_los_mayores_que_dos

imports Main "HOL-Number_Theory.Number_Theory"

begin

definition primos :: "nat set" where

"primos = {n ∈ ℕ . prime n}"

definition mayoresQue2 :: "nat set" where

"mayoresQue2 = {n ∈ ℕ . n > 2}"

definition impares :: "nat set" where

"impares = {n ∈ ℕ . ¬ even n}"

(* 1ª demostración *)

lemma "primos ∩ mayoresQue2 ⊆ impares"

proof

fix x

assume "x ∈ primos ∩ mayoresQue2"

then have "x ∈ ℕ ∧ prime x ∧ 2 < x"

by (simp add: primos_def mayoresQue2_def)

then have "x ∈ ℕ ∧ odd x"

by (simp add: prime_odd_nat)

then show "x ∈ impares"

by (simp add: impares_def)

qed

(* 2ª demostración *)

lemma "primos ∩ mayoresQue2 ⊆ impares"

unfolding primos_def mayoresQue2_def impares_def

by (simp add: Collect_mono_iff Int_def prime_odd_nat)

(* 3ª demostración *)

lemma "primos ∩ mayoresQue2 ⊆ impares"

unfolding primos_def mayoresQue2_def impares_def

by (auto simp add: prime_odd_nat)

end

1. Demostraciones con Lean4

3. Demostraciones con Isabelle/HOL

Share this:

Escribe un comentarioCancel reply