Zulip Chat Archive

Stream: new members

Topic: Find min of a set of natural numbers


view this post on Zulip Ryan Lahfa (Apr 04 2020 at 21:50):

I'm trying to understand the nat.find_xxx API and as far as I understand it, it looks like rather some helpers which prove the induction over natural numbers.

I have some set of natural numbers which is infinite, nonempty and I'd like to take the smallest element, I could reuse the Inf/is_least machinery but I think there must be more elementary things to do?

Namely, I'm interested in this (mis-formulated?) lemma:

import data.set

lemma smallest_element (S: set ): S.nonempty   n : ,  m < n, m \notin S := sorry

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 21:50):

(I cannot use finset.min because of the infinite condition.)

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 21:53):

And I answer myself…

lemma smallest_element (S: set ): S.nonempty   n : ,  m < n, m  S := begin
  intro H,
  use (nat.find H),
  intro m,
  apply nat.find_min H,
end

seems to work just fine.

But I wonder if there is a more canonical way.

view this post on Zulip Daniel Keys (Apr 04 2020 at 23:00):

Well-ordered principle: every non-empty subset of the natural numbers has a least element.

view this post on Zulip Daniel Keys (Apr 04 2020 at 23:02):

Mathematical induction is true if and only if ℕ is well-ordered.

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 23:12):

Daniel Keys said:

Well-ordered principle: every non-empty subset of the natural numbers has a least element.

Is there a direct theorem using is_least?

view this post on Zulip Daniel Keys (Apr 04 2020 at 23:42):

Not sure what you mean here, but it seems to me that your smallest_element lemma restates an axiom:

axiom well_ordered (S : set ) : S.nonempty   m  S,  n  S, m  n

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 23:43):

That's not an axiom in Lean

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 23:43):

that's a theorem

view this post on Zulip Daniel Keys (Apr 04 2020 at 23:44):

Good point. I didn't mean it was in Lean.

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 23:45):

The question is how to do all of this stuff in Lean.

view this post on Zulip Daniel Keys (Apr 04 2020 at 23:46):

Isn't this hidden somewhere in Lean - i.e. by the definition of the naturals as an inductive type?

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 23:46):

Sure

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 23:46):

The question is where is it hidden and what is the canonical way to get it out.

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 23:47):

< is not some predicate which is canonically associated to nat; < has a definition which probably uses +

view this post on Zulip Daniel Keys (Apr 04 2020 at 23:49):

(deleted)

view this post on Zulip Logan Murphy (Nov 26 2020 at 15:26):

I hope it's okay to revive an old thread, but I wanted to write a proof of the well-ordering principle for positive naturals and so was searching through old Zulip threads mentioning WOP, of which there are a few. I ended up figuring out this (not particularly graceful) tactic proof, so I thought I'd stick it here in case anyone else tries looking up "well-ordering principle" and finds it useful.

import tactic
open classical

local attribute [instance] prop_decidable

lemma pnat_wf : well_founded (preorder.to_has_lt +).1 :=
measure_wf coe

lemma well_ordering_principle (A : set pnat) : A.nonempty 
     m  A, ( x  A, m  x) :=
begin
  intro H,
  have := well_founded.has_min pnat_wf A H,
  rcases this with m, H1,H2⟩,
  use m, split,{exact H1},
  intros x H3, replace H2 := H2 x H3,
  exact not_lt.mp H2,
end

view this post on Zulip Mario Carneiro (Nov 26 2020 at 15:31):

FYI, "well ordering principle" is another way to spell "induction"


Last updated: May 16 2021 at 21:11 UTC