Finset.max

Stream: mathlib4

[Violeta Hernández]

Just ran into some annoyances with missing API with docs#Finset.max, only to realize that this is actually just a thin wrapper around docs#Finset.sup, which does have the API I want.

[Violeta Hernández]

I could go ahead and add said API, but I think it's worth asking, why have both definitions?

[Violeta Hernández]

I get the logic behind having both max and sup, it being that Lean also caters to programmers. But does this logic go all the way up to Finset?

[Violeta Hernández]

(Also, why does Finset.sup take an extra function argument, while Finset.max doesn't?)

[Yakov Pechersky]

Because sup is like sum.

[Yakov Pechersky]

And max withBots for the user. There are also sup' and max'

[Yakov Pechersky]

Max is specialized for linear orders. And there is docs#Finset.max_eq_sup_coe

[Yakov Pechersky]

I think both are worth having. What api would you like to add?

[Violeta Hernández]

Yakov Pechersky said:

And max withBots for the user. There are also sup' and max'

I don't really understand the asymmetry here. Why can't sup do the same? Why can't max take in an extra function argument? What is the benefit of specializing to linear orders?

[Violeta Hernández]

Yakov Pechersky said:

I think both are worth having. What api would you like to add?

I noticed we don't have a max analog of docs#Finset.sup'_eq_sup

[Jakub Nowak]

Violeta Hernández said:

What is the benefit of specializing to linear orders?

E.g. docs#Finset.mem_of_max is not true for sup.

[Jakub Nowak]

Although, I've noticed that there's instance of docs#Max docs#SemilatticeSup.toMax, which is defined in terms of SemilatticeSup.sup. The documentation of docs#Max says "Returns the greater of its two arguments.", which is not true for docs#SemilatticeSup.toMax (because, it can return neither of its two arguments). There seems to be inconsistency with max vs sup terminology in mathlib.

[Violeta Hernández]

MrQubo said:

Violeta Hernández said:

What is the benefit of specializing to linear orders?

E.g. docs#Finset.mem_of_max is not true for sup.

What do you mean? It is true, if you take a LinearOrder assumption.

[Jakub Nowak]

Ah, you're right.
Isn't putting more assumption than necessary at the definition an anti-pattern in lean? Even if there is a reason to have both max and sup, there is no need for LinearOrder assumption at the definition of max. Though, sup also doesn't need SemilatticeSup at the definition. Just Max. Although, as I've stated previously, SemilatticeSup shouldn't implement Max in the first place.

[Aaron Liu]

MrQubo said:

Ah, you're right.
Isn't putting more assumption than necessary at the definition an anti-pattern in lean? Even if there is a reason to have both max and sup, there is no need for LinearOrder assumption at the definition of max. Though, sup also doesn't need SemilatticeSup at the definition. Just Max. Although, as I've stated previously, SemilatticeSup shouldn't implement Max in the first place.

it works with any commutative associative operation

[Jakub Nowak]

Well, yes, it's just sum. But you might want to have multiple different operations on your type, like addition, multiplication etc, so we have different classes for those. We need to refer to one of these classes, Max/Sup in this case.

[Aaron Liu]

so do we just put [m : Max α] [Std.Commutative m.max] [Std.Associative m.max]

[Jakub Nowak]

You don't need Commutative and Associative in the definition I think? Only Max and OrderBot.

[Aaron Liu]

Max means an arbitrary binary operation which is called "max"

[Jakub Nowak]

Yes.

[Aaron Liu]

and I think commutativity and associativity are necessary

[Jakub Nowak]

Anyway, it doesn't matter, because I doubt there are any interesting properties without assuming relation between max and partial order.

Back to main topic, I think there are use cases to have max. It's I think similar to like we have e.g. Monoid and Semigroup. Like, Monoid is just Semigroup with additional properties, but we still have it, duplicating some of the API of Semigroup with it. We should probably just mirror the api from sup to max, all the proofs should be trivial as LinearOrder implements SemilatticeSup.

[Aaron Liu]

I think we already do that?

[Jakub Nowak]

Probably yes, just not the whole api apparently.