Zulip Chat Archive

Stream: maths

Topic: Return type of `finset.sup`


view this post on Zulip Chris Hughes (Jun 28 2019 at 12:46):

Currently the type of finset.sup is

finset.sup :
  Π {α : Type u_1} {β : Type u_2} [_inst_1 : lattice.semilattice_sup_bot α], finset β  (β  α)  α

I think it would make more sense to return a β. There's no function that does this at the moment, and it would be useful.

view this post on Zulip Chris Hughes (Jun 28 2019 at 12:49):

I guess the β is not unique though. In my application the function is injective.

view this post on Zulip Reid Barton (Jun 28 2019 at 12:51):

The ordering on \a might not be total, in which there is no "corresponding" value of \b to return, if I understand what you want to do

view this post on Zulip Mario Carneiro (Jun 28 2019 at 12:51):

You could write a trunc of a value that maps to the sup

view this post on Zulip Mario Carneiro (Jun 28 2019 at 12:52):

and in the case where the function is injective you can get the value out

view this post on Zulip Reid Barton (Jun 28 2019 at 12:52):

What you're looking for is usually called "argmax"

view this post on Zulip Chris Hughes (Jun 28 2019 at 13:03):

Okay, so I'm going to have to write this argmax function. We're kind of inconsistent at the moment with how we handle empty lists on the variants of max list.maximum, finset.sup, finset.max. What should argmax do?

view this post on Zulip Mario Carneiro (Jun 28 2019 at 13:05):

If it has a complex type like I suggested, then it's basically a proof procedure, so I think it should be fine to assume the input is nonempty

view this post on Zulip Mario Carneiro (Jun 28 2019 at 13:07):

We could also have a more weakly typed version that has some default behavior in that case

view this post on Zulip Mario Carneiro (Jun 28 2019 at 13:08):

just so you can write argmax_(x \in S) f x as a term in reasonable conditions


Last updated: May 18 2021 at 07:19 UTC