Zulip Chat Archive

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 :=
  use 3,
  have h32 : 3 > 2, by simp,
  exact h32,

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

noncomputable def min_p2 :  := nat.find hp2

lemma min_p5_positive : min_p2 > 0 :=
  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,

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 :=
  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,

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