n-ary maximum

Stream: new members

[Horatiu Cheval]

What's the recommended way of saying "the maximum of n numbers", for example in the form of a function list nat -> nat?
I thought about doing l.maximum.iget, where l : list nat, but does this have a good API like max does? Or is there a better way?

[Kevin Buzzard]

What happens when the list is empty?

[Kevin Buzzard]

There is Sup of course! But this is different to max because the sup might not be in the set (when the list is empty).

[Eric Wieser]

For finsets there's both docs#finset.max and docs#finset.sup

[Horatiu Cheval]

I know that the list is not empty, so I can provide a proof of this if needed. But I don't think it matters, with the iget function you will get the default inhabitant of the type and statements like forall x ∈ l, x ≤ l.maximum.iget should hold hold trivially by exfalso.

[Eric Wieser]

The sup version is Sup { x | x ∈ l }

[Horatiu Cheval]

But Sup is noncomputable, and finset.max has the same issue as list.maximum in that it returns an option.

[Horatiu Cheval]

Ah, but finset.sup is both computable and doesn't return option, that's what I was looking for

[Yakov Pechersky]

As a stopgap (I have an upcoming PR on this), you can use list.foldr max l 0

[Yakov Pechersky]

Or, over a multiset, multiset.fold max max_commutative m 0

[Yakov Pechersky]

Modulo argument order, which I don't remember currently

[Yakov Pechersky]

There's also docs#finset.max'