typeclasses for orders with neg and inv

Stream: general

[Joseph Myers]

In #15652 it was discussed how it's unfortunate that various lemmas about the interaction of order properties with neg and inv end up needing separate left and right versions because they're deduced from order properties for addition and multiplication that have separate left and right versions, and how it might make sense to have typeclasses for the neg and inv properties to avoid that duplication.

What should such typeclasses look like? For example, would it be appropriate to add variants of covariant_class and contravariant_class that (a) are for a unary rather than a binary operation and (b) are for operations that reverse the order of the relation? If so, can someone suggest better (shorter) names than e.g. covariant_unary_antitone_class?

Some of the lemmas also need neg_zero or inv_one. Should we have typeclasses for those as well, so that the lemmas can be applied more generally than subtraction_monoid / division_monoid (the current context in which neg_zero and inv_one are proved)?

Examples of types for which such order properties, and neg_zero or inv_one, are relevant, but that aren't covered by the typeclasses for existing lemmas (and thus sometimes have their own duplicate lemmas), include ereal, ennreal and sign_type. (We have a separate neg_zero' lemma in the mul_zero_class has_distrib_neg case to cover that property for sign_type.)

[Johan Commelin]

cc @Eric Wieser @Yaël Dillies

[Yaël Dillies]

I stand by my message on this PR: https://github.com/leanprover-community/mathlib/pull/15652#issuecomment-1193904087

[Yaël Dillies]

I will think of the details shortly.

[Johan Commelin]

Related PR

#16187 refactor(algebra/group/defs): inv_one_class, neg_zero_class

[Johan Commelin]

@Joseph Myers I'm somewhat worried about

These are Prop-valued classes, taking has_one and
has_inv or has_zero and has_neg arguments rather than extending
those classes, to allow them to be used together with other classes
such as div_inv_monoid in the typeclass requirements of lemmas
without needing to define extra classes for the combination of such a
class with these new classes.

I'm not an expert, but if I understand correctly then this might lead to performance problems. See also https://www.ralfj.de/blog/2019/05/15/typeclasses-exponential-blowup.html

Do we have data about how this PR affects mathlib compile time?

[Anne Baanen]

The current setup is probably OK since the inheritance depth is not so much. When you start writing division_monoid [monoid α] [has_inv α] [inv_one_class α] is when the blowup really starts...

[Anne Baanen]

Still I think bundled inheritance is the best way to go here.

[Joseph Myers]

With the way CI has been behaving lately with completely random timeouts and long delays lately unrelated to the content of PRs, getting meaningful compile time figures is hard.

[Joseph Myers]

Note that neg_zero_class is definitely relevant in cases such as sign_type that do not have addition or subtraction at all; I don't think a solution for the inequality lemmas that removes left/right duplication but keeps dependence on having add/sub/mul/div for lemmas that don't actually involve those operations would be a particularly good solution.

[Eric Wieser]

An argument for not bundling is that this matches the style of docs#covariant_class

[Yaël Dillies]

Actually I've always seen this as an argument against covariant_class!

[Sebastien Gouezel]

My two cents on this:

• Definitions should be bundled as far as it remains reasonable, to avoid exponential blowup when building products, for instance.
• But the bundled stuff should have instances to the most basic classes. For instance, ordered_comm_semiring or whatever should imply covariant_class ...
• Lemmas, on the other hand, are better stated with the most basic classes. Because in this way they will apply in the most possible general situations and still this will not create any blowup.

[Damiano Testa]

Since we are talking about covariant_class, I feel called in the discussion. I also agree that creating big bundles,while at the same time also proving stuff for "atomic" typeclasses is helpful. In particular, bundling a few of the covariant_class assumptions together in more comprehensive classes is certainly human friendly.

For instance, Yaël's recent PR with

• ordered_semiring renamed to ordered_cancel_semiring;
• ordered_semiring used for something more meaningful;

produces two typeclasses that bundle together a few covariant_classes into something that is way more meaningful.

[Damiano Testa]

The silly mul_left_of_le_of_lt_one_of_nonneg are then useful because they would apply smoothly to real, nat, ennreal and who knows what other "real-world" type you want!