least element principle

Stream: Is there code for X?

[Jeremy Avigad]

I would have expected the least element principle for the natural numbers to be somewhere in the library (without any decidable_eq hypothesis), but I can't find it. Am I missing something?

import data.nat.basic
open_locale classical

theorem nat.exists_least {p : ℕ → Prop} (h : ∃ x, p x) :
  ∃ x, p x ∧ ∀ y < x, ¬ p y :=
subtype.exists_of_subtype (nat.find_x h)

[Mario Carneiro]

That's nat.strong_induction in contrapositive, I guess

[Yakov Pechersky]

Or the nat.find and nat.find_x related decls.

[Yakov Pechersky]

Unless there the constructiveness of it is what is undesired

[Junyan Xu]

Basically the same as docs#well_founded.has_min:

import order.well_founded
open_locale classical

theorem nat.exists_least {p : ℕ → Prop} (h : ∃ x, p x) :
  ∃ x, p x ∧ ∀ y < x, ¬ p y :=
let ⟨x, hx, hm⟩ := nat.well_founded_lt.1.has_min p h in ⟨x, hx, λ y hl hy, hm y hy hl⟩

[Jeremy Avigad]

It's nice that works without open_locale classical, though it's a lot to have to remember.

[Junyan Xu]

docs#nat.strong_induction_on doesn't depend on any axioms, but docs#well_founded.has_min depends on all three, as it should be: your nat.exists_least implies LEM.

import order.well_founded

axiom nat.exists_least {p : ℕ → Prop} (h : ∃ x, p x) : ∃ x, p x ∧ ∀ y < x, ¬ p y

def pred (p : Prop) : ℕ → Prop | 0 := p | 1 := ¬p | _ := true

theorem lem {p : Prop} : p ∨ ¬ p :=
begin
  obtain ⟨x, hx, hm⟩ := @nat.exists_least (pred p) ⟨2, trivial⟩,
  cases x, { exact or.inl hx },
  cases x, { exact or.inr hx },
  refine (hm 1 _ $ hm 0 _).elim; dec_trivial,
end

#print axioms lem /- nat.exists_least -/

[Mario Carneiro]

Oh, that's a neat proof. Golfed:

axiom nat.exists_least {p : ℕ → Prop} (h : ∃ x, p x) : ∃ x, p x ∧ ∀ y < x, ¬ p y

theorem lem {p : Prop} : p ∨ ¬ p :=
match @nat.exists_least (λ n, nat.cases_on n p (λ _, true)) ⟨1, trivial⟩ with
| ⟨0, hx, _⟩ := or.inl hx
| ⟨_+1, _, hm⟩ := or.inr (hm 0 dec_trivial)
end