Zulip Chat Archive

Stream: general

Topic: typeclasses for orders with neg and inv

Joseph Myers (Aug 18 2022 at 22:55):

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 (Aug 24 2022 at 09:56):

cc @Eric Wieser @Yaël Dillies

Yaël Dillies (Aug 24 2022 at 09:56):

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

Yaël Dillies (Aug 24 2022 at 09:56):

I will think of the details shortly.

Johan Commelin (Aug 24 2022 at 09:57):

Related PR

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

Johan Commelin (Aug 24 2022 at 09:59):

@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 (Aug 24 2022 at 10:37):

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 (Aug 24 2022 at 10:37):

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

Joseph Myers (Aug 24 2022 at 11:00):

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 (Aug 24 2022 at 11:04):

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 (Aug 24 2022 at 12:20):

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

Yaël Dillies (Aug 24 2022 at 12:37):

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

Sebastien Gouezel (Aug 24 2022 at 15:01):

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 (Aug 24 2022 at 15:08):

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 (Aug 24 2022 at 15:11):

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!

Last updated: Aug 03 2023 at 10:10 UTC