Equivalent of `nat.find` for positive integers?

Stream: Is there code for X?

[Stuart Presnell]

We have docs#nat.find that gives the smallest natural number satisfying some given satisfied predicate (and hence the smallest element of a given inhabited set ℕ). Is there a corresponding thing for positive integers? Or, if there's not something replicating that specific functionality, is there a nice way to prove that every set of positive integers has a minimal element?

example (S : set ℤ) (hS_pos : ∀ x : ℤ, x ∈ S → 0 < x) (hS : ∃ k : ℤ, k ∈ S) :
  ∃ m ∈ S, ∀ x ∈ S, m ≤ x := sorry

[Yaël Dillies]

We have docs#int.conditionally_complete_linear_order so you can use ⨆.

[Stuart Presnell]

I feel like I'm doing something in a laborious way that should be simple. Is there a trick I've missed here?

example (S : set ℤ) (hS_pos : ∀ x : ℤ, x ∈ S → 0 < x) (hS : ∃ k : ℤ, k ∈ S) :
  ∃ m ∈ S, ∀ x ∈ S, m ≤ x :=
begin
  have : bdd_below S, { rw bdd_below_iff_subset_Ici, use [0, λ x hx, le_of_lt (hS_pos x hx)] },
  use [Inf S, (int.cInf_mem hS this), (λ x hx, cInf_le this hx)],
end

[Yaël Dillies]

That sounds right, though.

[Eric Wieser]

Are you just trying to prove docs#bdd_below S there?

[Stuart Presnell]

Ok, thanks.

[Eric Wieser]

It golfs a little to:

begin
  have : bdd_below S := ⟨0, λ x hx, (hS_pos x hx).le⟩,
  exact ⟨Inf S, int.cInf_mem hS this, λ x, cInf_le this⟩,
end

[Eric Wieser]

Or even:

begin
  simp_rw exists_prop,
  exact int.exists_least_of_bdd ⟨0, λ x hx, (hS_pos x hx).le⟩ hS,
end

docs#int.exists_least_of_bdd and docs#int.least_of_bdd seem like exactly what you want.

[Stuart Presnell]

That's great, thank you!

[Eric Wieser]

I found that by spotting docs#int.cInf_eq_least_of_bdd which was in the same file as docs#int.conditionally_complete_linear_order

[Stuart Presnell]

Now, my first reaction is to want to PR (some version of) this, because the statement is a simple and obvious thing expressed in elementary language while the proof you've arrived at is rather less obvious. But from previous experience I know that my calibration on what's worth PRing is not quite dialled in yet :smile: What do you reckon to this?

[Stuart Presnell]

Part of my thinking on this is that a lot of newcomers to mathlib are likely to run into elementary stuff like this fairly quickly, and aren't going to find docs#int.conditionally_complete_linear_order or docs#int.least_of_bdd and aren't going to work out the neat concise proof that you landed on.

[Eric Wieser]

Well your version is just a special case of the general version with 0 < _ instead of x ≤ _.

[Eric Wieser]

I think if you had the general statement, you could then use library_search

[Eric Wieser]

The other problem is the difference between ∃ x ∈ S, p x (aka ∃ x, ∃ h : x ∈ S, p x) and ∃ x, x ∈ S ∧ p x, since it would be ridiculous to state every lemma in both versions

[Stuart Presnell]

I wrote hS_pos in that way because when I originally tried (hS_pos : ∀ x ∈ S, 0 ≤ x) I got failed to synthesize type class instance for ... has_mem ℕ (set ℤ) (because 0 was interpreted as 0 : ℕ).

[Stuart Presnell]

I've tried generalising to

example (S : set ℤ) {b : ℤ} (hS_pos : ∀ x ∈ S, b ≤ x) (hS : ∃ k : ℤ, k ∈ S) :
  ∃ m ∈ S, ∀ x ∈ S, m ≤ x

and still library_search can't find a solution. Was there a different version you were thinking of?

[Eric Wieser]

Yes, library search should be able to find:

example (S : set ℤ) {b : ℤ} (hS_pos : ∀ x ∈ S, b ≤ x) (hS : ∃ k : ℤ, k ∈ S) :
  ∃ m, m ∈ S ∧ ∀ x ∈ S, m ≤ x

[Eric Wieser]

Except it seems it can't...

[Eric Wieser]

Ah right, it can't because it takes two steps

[Eric Wieser]

I think ultimately the solution is to make it easier for someone who knows about docs#nat.find_x to find docs#int.least_of_bdd

[Eric Wieser]

The existential you have isn't a very good way to find definitions

[Eric Wieser]

Perhaps we should rename int.least_of_bdd and nat.find_x to be more similar; if nothing else, there's no equivalent of nat.find without the subtyping

[Stuart Presnell]

That would be a good solution. If the user knows about int.exists_least_of_bdd then from an exploratory have := int.exists_least_of_bdd _ _library search can close the goal, and from there it's obvious what needs to be filled in.

[Eric Wieser]

This is what the least_of_bdd API would look like if we rewrote it in the nat.find style:

namespace int

variables {P : ℤ → Prop} [decidable_pred P] (b : ℤ) (Hb : ∀ z : ℤ, P z → b ≤ z) (Hinh : ∃ z : ℤ, P z)

/-- Analog to `nat.find` -/
def least_of_bdd' : ℤ :=
have EX : ∃ n : ℕ, P (b + n), from
  let ⟨elt, Helt⟩ := Hinh in
  match elt, le.dest (Hb _ Helt), Helt with
  | ._, ⟨n, rfl⟩, Hn := ⟨n, Hn⟩
  end,
b + (nat.find EX : ℤ)

/-- Analog to `nat.find_spec` -/
lemma least_of_bdd_spec : P (least_of_bdd' b Hb Hinh) :=
nat.find_spec (_ : ∃ n : ℕ, P (b + n))

/-- Analog to `nat.find_min'` -/
lemma least_of_bdd_min' (z : ℤ) (hz : P z) : least_of_bdd' b Hb Hinh ≤ z :=
match z, le.dest (Hb _ hz), hz with
| ._, ⟨n, rfl⟩, h := add_le_add_left
  (int.coe_nat_le.2 $ nat.find_min' _ h) _
end

/-- Analog to `nat.find_x` -/
def least_of_bdd_x : {lb : ℤ // P lb ∧ (∀ z : ℤ, P z → lb ≤ z)} :=
⟨least_of_bdd' b Hb Hinh, least_of_bdd_spec _ _ _, least_of_bdd_min' _ _ _⟩

end int

(all I did was break the existing definition into four pieces)

[Eric Wieser]

@Mario Carneiro, it looks like you were involved in the least_of_bdd definitions; do you think the refactor above is sensible, or would you prefer that nat.find be changed to align with the current int.least_of_bdd?