Trying to refactor `algebra/order/ring`

Stream: general

[FR]

I am trying to refactor algebra/order/ring. I tried to include every possible case, and I soon realized that there are too many cases. To alleviate this problem, is it possible to consider the ordered structure on the algebraic structure separately from the algebraic structure? For example, for an ordered ring R should we write [ring R] [ordered_semiring R]?

[Eric Rodriguez]

cc @Damiano Testa , who was leading the order refactor

[Yaël Dillies]

and @Yakov Pechersky

[Yaël Dillies]

We all know we need such a refactor in some form, but it's going to be massive.

[Damiano Testa]

The current approach (which is still ongoing) is to use the co(ntra)variant_classes to bypass changing the ordered_[...] hierarchy. This means that you make

• typeclass assumptions on the operations,
• typeclass assumptions on the order,
• some extra typeclass assumptions binding the two, using a combination of covariant_, contravariant_ add, mul \le, ...

[Damiano Testa]

You can look at the file with only one operations to see how this is taking place. The last file on which I worked is algebra.order.monoid_lemmas_zero_lt, but I have not yet lodged it at the bottom of the orderedhierarchy, since it is still incomplete.

I plan to continue with this when I have some time, but the term only just ended and I have not been able to work on this recently.

[Damiano Testa]

(This latest file finally starts the interaction between order and two operations.)

[Damiano Testa]

This is also explained in the module doc-string for algebra.covariant_and_contravariant.