Find min of a set of natural numbers

Stream: new members

[Ryan Lahfa]

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

[Ryan Lahfa]

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

[Ryan Lahfa]

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.

[Daniel Keys]

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

[Daniel Keys]

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

[Ryan Lahfa]

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?

[Daniel Keys]

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

[Kevin Buzzard]

That's not an axiom in Lean

[Kevin Buzzard]

that's a theorem

[Daniel Keys]

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

[Kevin Buzzard]

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

[Daniel Keys]

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

[Kevin Buzzard]

Sure

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Daniel Keys]

(deleted)

[Logan Murphy]

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

[Mario Carneiro]

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