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

Author: adomani

src/algebra/linear_ordered_comm_group_with_zero.lean

@@ -182,7 +182,8 @@ have hb : b ≠ 0 := ne_zero_of_lt hab,
 have hd : d ≠ 0 := ne_zero_of_lt hcd,
 if ha : a = 0 then by { rw [ha, zero_mul, zero_lt_iff], exact mul_ne_zero hb hd } else
 if hc : c = 0 then by { rw [hc, mul_zero, zero_lt_iff], exact mul_ne_zero hb hd } else
-@mul_lt_mul''' _ _ (units.mk0 a ha) (units.mk0 b hb) (units.mk0 c hc) (units.mk0 d hd) hab hcd
+@mul_lt_mul''' _
+  (units.mk0 a ha) (units.mk0 b hb) (units.mk0 c hc) (units.mk0 d hd) _ _ _ _ _ _ hab hcd
 
 lemma mul_inv_lt_of_lt_mul' (h : x < y * z) : x * z⁻¹ < y :=
 have hz : z ≠ 0 := (mul_ne_zero_iff.1 $ ne_zero_of_lt h).2,

src/algebra/ordered_group.lean

@@ -36,6 +36,17 @@ class ordered_comm_group (α : Type u) extends comm_group α, partial_order α :
 
 attribute [to_additive] ordered_comm_group
 
+@[to_additive]
+instance units.covariant_class [ordered_comm_monoid α] :
+  covariant_class (units α) (units α) (*) (≤) :=
+{ covc := λ a b c bc, by {
+  rcases le_iff_eq_or_lt.mp bc with ⟨rfl, h⟩,
+  { exact rfl.le },
+  refine le_iff_eq_or_lt.mpr (or.inr _),
+  refine units.coe_lt_coe.mp _,
+  cases lt_iff_le_and_ne.mp (units.coe_lt_coe.mpr h) with lef rig,
+  exact lt_of_le_of_ne (mul_le_mul_left' lef ↑a) (λ hg, rig ((units.mul_right_inj a).mp hg)) } }
+
 /--The units of an ordered commutative monoid form an ordered commutative group. -/
 @[to_additive]
 instance units.ordered_comm_group [ordered_comm_monoid α] : ordered_comm_group (units α) :=
@@ -962,7 +973,7 @@ instance [ordered_add_comm_group α] : ordered_add_comm_group (order_dual α) :=
 
 instance [linear_ordered_add_comm_group α] :
   linear_ordered_add_comm_group (order_dual α) :=
-{ add_le_add_left := λ a b h c, @add_le_add_left α _ b a h _,
+{ add_le_add_left := λ a b h c, by exact add_le_add_left h _,
   ..order_dual.linear_order α,
   ..show add_comm_group α, by apply_instance }