finset.max for nonempty sets

Stream: maths

[Kevin Buzzard]

I've been trying to use finset.max and it's a bit annoying in all my use cases because it takes in an arbitrary finset X and returns an option X (to deal with the case where the finset is empty). It would be very easy to write a variant which takes a non-empty finset and returns its max, and I find myself wanting this variant. What should I call it?

[Kenny Lau]

you want to write a partial function? :shock:

[Kevin Buzzard]

And is there room for it in finset.lean?

[Kenny Lau]

I think finset.sup might be what you seek

[Kevin Buzzard]

It's not that either, because finset.sup wants the lattice to have a bot, and in my use case there is no bot.

[Kenny Lau]

so you really want a partial function :shock:

[Kevin Buzzard]

I simply want a function which takes in a non-empty finite set of reals and produces its max.

[Kevin Buzzard]

I am happy to supply the proof that it's non-empty.

[Kevin Buzzard]

Surely there will be more use cases. Kenny this is for proving that a convergent sequence of reals is bounded. Working with the option is a pain, because I simply want the answer rather than having to keep talking about elements of the option output.

[Kevin Buzzard]

Is finset.max' a crap name?

[Kevin Buzzard]

Ultimately it will be easier to use than the contortions I'm having to go through to prove the results I need about finset.max. Kenny, try proving that if f : nat -> real and B = max {f 0, f 1, f 2}` then for all i <= 2, f i <= B. I had to extract B from the option and then prove that it was in the option and it clutters up the local context -- both of these could be avoided because the fact that f 0 is in the set is easy to prove. I think my proposal makes it easier, but I might be wrong because it's only just occurred to me.

[Chris Hughes]

You can use option.get

[Johannes Hölzl]

No, Kevin wants option.iget. Or a max version which assumes inhabited.

[Johan Commelin]

So we should fix ourselves a finset.imax?

[Johan Commelin]

iget and imax sound like they were invented by Apple. :sad:

[Kevin Buzzard]

I don't want to keep applying iget, I know the set is nonempty and I just want the max :-) There seem to be more contortions using what is there already. I should try writing the code and see if it's actually better.

[Kevin Buzzard]

rofl I decided to call it finset.max' and then I discovered it was there already :-)

[Kevin Buzzard]

Johannes put it there in October!

[Patrick Massot]

One day I taught Simon what was convert. At some point in the history section of the explanation, I was forced to mention that Simon himself wrote that tactic.

[Kevin Buzzard]

I see, the point is that max' wants a proof that S ≠ ∅, perhaps Johannes could see that I wanted something a bit more convenient.

[Mario Carneiro]

I am 100% on board with having finset.imax defined and including the obvious lemmas. (Johan, I don't think you can patent single letter prefixes.) I agree you shouldn't deal with (finset.max s).iget, there should be a definition for this combination.

[Kevin Buzzard]

So I'm currently using finset.max' and it's fine