Zulip Chat Archive

Stream: new members

Topic: Canonical way to get minimum element of set of naturals

Julian Gilbey (Nov 03 2021 at 09:10):

I have a property defined for natural numbers: p : N -> Prop and I have a subtype { x : N // p x }. I can produce a natural n : N with p n, so this set/subtype is non-empty. Since N is well-ordered, this non-empty subtype/set has a minimum element. But I cannot figure out what Lean incantation I should use to find/refer to this minimum element of this set/subtype.

Any suggestions would be much welcomed, thanks!

Kevin Buzzard (Nov 03 2021 at 09:13):

You want nat.find -- right click on it and look at the functions defined just after it to see the API available to you

Julian Gilbey (Nov 03 2021 at 09:13):

Thanks @Kevin Buzzard !

Julian Gilbey (Nov 03 2021 at 11:55):

Oh, groan, I thought I was getting the hang of this. But now I realise I don't know how to define a lambda expression inside a begin/end argument. I've written:

  have p := λ k : , x < (k : ) * (1 / (n : )),

but then the goals just list: p : N -> Prop, and when I get a target of p n0 and I have a term h of exactly the right form (namely, x < (n0 : R) * (1 / (n : R))), Lean refuses to match the two when I say exact h. I guess I should be using something other than have, but I don't know what.

My second problem, once I've resolved this, is that because my predicate uses the reals, I'm guessing it's not decidable. So nat.find presumably won't work. Is there a non-decidable version of nat.find which just asserts the existence of such an element but without attempting to compute it?

Reid Barton (Nov 03 2021 at 11:59):

Use let not have

Julian Gilbey (Nov 03 2021 at 12:01):

Ah, magic, thanks! :grinning:

Reid Barton (Nov 03 2021 at 12:05):

For the second question you could use tactic#classical, or open_locale classical at the top level of your file if this is something you will generally need

Floris van Doorn (Nov 03 2021 at 13:56):

You can also use Inf {n | p n}, and use the instance docs#nat.conditionally_complete_linear_order_bot and the API about docs#conditionally_complete_linear_order. This does not require the predicate to be decidable.

Floris van Doorn (Nov 03 2021 at 13:57):

plus some lemmas specific to nat, like docs#nat.Inf_mem

Yury G. Kudryashov (Nov 04 2021 at 06:25):

Inf doesn't require decidable and is not computable.

Last updated: Dec 20 2023 at 11:08 UTC