Commit 2021-05-15 16:28 172195bb

feat(algebra/{ordered_monoid, ordered_monoid_lemmas}): split the ordered_[...] typeclasses (#7371) This PR tries to split the ordering assumptions from the algebraic assumptions on the operations in the ordered_[...] hierarchy. The strategy is to introduce two more flexible typeclasses, covariant_class and contravariant_class.

• covariant_class models the implication a ≤ b → c * a ≤ c * b (multiplication is monotone),
• contravariant_class models the implication a * b < a * c → b < c. Since co(ntra)variant_class takes as input the operation (typically (+) or (*)) and the order relation (typically (≤) or (<)), these are the only two typeclasses that I have used. The general approach is to formulate the lemma that you are interested in and prove it, with the ordered_[...] typeclass of your liking. After that, you convert the single typeclass, say [ordered_cancel_monoid M], to three typeclasses, e.g. [partial_order M] [left_cancel_semigroup M] [covariant_class M M (function.swap (*)) (≤)] and have a go at seeing if the proof still works! Note that it is possible (or even expected) to combine several co(ntra)variant_class assumptions together. Indeed, the usual ordered typeclasses arise from assuming the pair [covariant_class M M (*) (≤)] [contravariant_class M M (*) (<)] on top of order/algebraic assumptions. A formal remark is that normally covariant_class uses the (≤)-relation, while contravariant_class uses the (<)-relation. This need not be the case in general, but seems to be the most common usage. In the opposite direction, the implication [semigroup α] [partial_order α] [contravariant_class α α (*) (≤)] => left_cancel_semigroup α holds (note the co*ntra* assumption and the (≤)-relation). Zulip: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/ordered.20stuff