## Stream: new members

### Topic: More on minimum naturals

#### Julian Gilbey (Nov 05 2021 at 07:23):

Hi! I'm still struggling with minimum natural number in a set and how to use nat.find and friends. Here's a (probably) minimal example (I wouldn't call it working though!). We define a simple predicate p2 (which appears to be undecidable), show the set of naturals satisfying it is nonempty, and then try to show its minimum is positive.

import data.nat.lattice

open_locale classical

def p2 := λ n : ℕ, n > 2

lemma hp2 : ∃ (m : ℕ), p2 m :=
begin
use 3,
have h32 : 3 > 2, by simp,
exact h32,
end

lemma hp2_not0 : ¬ p2 0 :=
begin
have h_not0 : ¬ 0 > 2, by simp,
exact h_not0,
end

noncomputable def min_p2 : ℕ := nat.find hp2

lemma min_p5_positive : min_p2 > 0 :=
begin
let min_p2_spec := nat.find_spec hp2,
simp at h,
-- we must now show that min_p2 = 0 leads to a contradiction
-- we know ¬ p2 0; how can we substitute this in?
-- in particular, the following rw line fails, as it cannot
-- unify(?) nat.find hp2 with min_p2, despite the latter
-- being defined as the former.
-- rw h at min_p2_spec,
sorry,
end


Any help filling in the sorry would be appreciated! Then I'll try to apply that to my bigger problem...

#### Johan Commelin (Nov 05 2021 at 07:27):

You've solved all the nat.find aspects of the problem already.

#### Johan Commelin (Nov 05 2021 at 07:28):

You are left with showing that \not (p2 0) and p2 x imply x > 0.

#### Johan Commelin (Nov 05 2021 at 07:31):

lemma min_p5_positive : min_p2 > 0 :=
begin
have min_p2_spec := nat.find_spec hp2,
apply nat.pos_of_ne_zero,
intro H,
apply hp2_not0,
rw ← H,
exact min_p2_spec,
end


#### Julian Gilbey (Nov 05 2021 at 08:48):

Oh, magic, thanks! One key error I made here was using let instead of have. I'll get there :wink:

#### Johan Commelin (Nov 05 2021 at 08:51):

No, I don't think that really mattered.

Last updated: Dec 20 2023 at 11:08 UTC