CODEWITHSUNDEEP
prooflean
pop123_123
pop123_123

Reputation: 1

lean4 prove that the set of prime numbers has at least two distinct elements

my example: seems to throw an error. am i doing something wrong? is my syntax the error? if so, how do i fix it? or how do i change me logic if i'm making a logical error?

/- 
## Problem 2 
-/

/- 
1. Define in Lean what it means for a subset of natural numbers to have at least two elements. 

2. Define in Lean what it means for a subset of any type `X` to have exactly two elements.

3. Define in Lean what it means for a subset of natural numbers to have infinitely many elements.

**In 1-3 above you should not borrow any definition from Mathlib.** There are possibly many ways to define these concepts. You should do it your own way, and what feels most natural to you.

Then verify that your definitions are correct according to the specification above by proving the followings test cases. 

1. Prove that the set of prime number has at least two elements.
2. Prove that the closed interval `Icc (0 : ℕ) 1` has exactly two elements. 
3. Prove that the set of injective functions `Bool → Bool` has exactly two elements.
4. Prove that the set of odd natural numbers has infinitely many elements.
-/ 

noncomputable section
open Classical 
open Set 

-- Definition for a set of natural numbers to have at least two distinct elements
def at_least_two_elems (A : Set ℕ) : Prop :=
  ∃ a b, a ∈ A ∧ b ∈ A ∧ a ≠ b 

-- Definition for a subset of any type `X` to have exactly two distinct elements
def exactly_two_elems {X : Type} (A : Set X) : Prop :=
  ∃ a b, a ∈ A ∧ b ∈ A ∧ a ≠ b ∧ ∀ c, c ∈ A → (c = a ∨ c = b)

-- Definition for a subset of natural numbers to have infinitely many elements
def inf_elems (A : Set ℕ) : Prop :=
  ∀ n : ℕ, ∃ m, m ∈ A ∧ m > n

-- Prove that the set of prime numbers has at least two distinct elements
example : at_least_two_elems {p : ℕ | Nat.Prime p} :=
  ⟨2, 3, Nat.Prime.two, Nat.Prime.three, ne_of_gt (by decide)⟩

Upvotes: -1

Views: 411

Answers (1)

Adomas Baliuka
Adomas Baliuka

Reputation: 1602

How about a tactics-based proof? Or do you explicitly not want that for some reason? By the way, your lemmas Nat.Prime.two (or three) do not seem to exist in the current version of Mathlib4.

import Mathlib  -- I added this. Using Mathlib4
noncomputable section
open Classical 
open Set 

-- Definition for a set of natural numbers to have at least two distinct elements
def at_least_two_elems (A : Set ℕ) : Prop :=
  ∃ a b, a ∈ A ∧ b ∈ A ∧ a ≠ b 

-- Definition for a subset of any type `X` to have exactly two distinct elements
def exactly_two_elems {X : Type} (A : Set X) : Prop :=
  ∃ a b, a ∈ A ∧ b ∈ A ∧ a ≠ b ∧ ∀ c, c ∈ A → (c = a ∨ c = b)

-- Definition for a subset of natural numbers to have infinitely many elements
def inf_elems (A : Set ℕ) : Prop :=
  ∀ n : ℕ, ∃ m, m ∈ A ∧ m > n


-- Prove that the set of prime numbers has at least two distinct elements
example : at_least_two_elems {p : ℕ | Nat.Prime p} := by
  rw [at_least_two_elems]
  use 2, 3
  decide

If you insist on doing it by constructor call,

-- Prove that the set of prime numbers has at least two distinct elements
example : at_least_two_elems {p : ℕ | Nat.Prime p} :=
  ⟨2, 3, (Nat.fact_prime_two).out, (Nat.fact_prime_three).out, (by decide)⟩

due to Nat.fact_prime_two being Facts now, not simply Props, in order to make typeclass inference easier. Not sure if there's a nicer notation (yes I am: the nicer notation uses tactics!)

Upvotes: 2

Related Questions