More on minimum naturals

Stream: new members

[Julian Gilbey]

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,
  by_contradiction,
  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]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

No, I don't think that really mattered.