feat(algebra/ordered_monoid): correct definition (#8877)

Our definition of `ordered_monoid` is not the usual one, and this PR corrects that.

The standard definition just says
```
(mul_le_mul_left       : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b)
```
while we currently have an extra axiom
```
(lt_of_add_lt_add_left : ∀ a b c : α, a + b < a + c → b < c)
```
(This was introduced in ancient times, 7d8e3f3, with no indication of where the definition came from. I couldn't find it in other sources.)

As @urkud pointed out a while ago [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/ordered_comm_monoid), these really are different.

The second axiom *does* automatically hold for cancellative ordered monoids, however.

This PR simply drops the axiom. In practice this causes no harm, because all the interesting examples are cancellative. There's a little bit of cleanup to do. In `src/algebra/ordered_sub.lean` four lemmas break, so I just added the necessary `[contravariant_class _ _ (+) (<)]` hypothesis. These lemmas aren't currently used in mathlib, but presumably where they are needed this typeclass will be available.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

counterexamples/canonically_ordered_comm_semiring_two_mul.lean

@@ -222,9 +222,6 @@ instance order_bot : order_bot L :=
   bot_le := bot_le,
   ..(infer_instance : partial_order L) }
 
-lemma lt_of_add_lt_add_left : ∀ (a b c : L), a + b < a + c → b < c :=
-λ (a : L) {b c : L}, (add_lt_add_iff_left a).mp
-
 lemma le_iff_exists_add : ∀ (a b : L), a ≤ b ↔ ∃ (c : L), b = a + c :=
 begin
   rintros ⟨⟨an, a2⟩, ha⟩ ⟨⟨bn, b2⟩, hb⟩,
@@ -271,8 +268,7 @@ begin
 end
 
 instance can : canonically_ordered_comm_semiring L :=
-{ lt_of_add_lt_add_left := lt_of_add_lt_add_left,
-  le_iff_exists_add := le_iff_exists_add,
+{ le_iff_exists_add := le_iff_exists_add,
   eq_zero_or_eq_zero_of_mul_eq_zero := eq_zero_or_eq_zero_of_mul_eq_zero,
   ..(infer_instance : order_bot L),
   ..(infer_instance : ordered_comm_semiring L) }

counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean

@@ -1,8 +1,8 @@
 /-
-Copyright (c) 2021 Johan Commelin (inspired by Kevin Buzzard, copied by Damiano Testa).
+Copyright (c) 2021 Johan Commelin.
 All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johan Commelin (inspired by Kevin Buzzard, copied by Damiano Testa)
+Authors: Johan Commelin, Damiano Testa, Kevin Buzzard
 -/
 import algebra.ordered_monoid
 
@@ -68,7 +68,6 @@ instance : linear_ordered_comm_monoid_with_zero foo :=
   zero_mul := by boom,
   mul_zero := by boom,
   mul_le_mul_left := by { rintro ⟨⟩ ⟨⟩ h ⟨⟩; revert h; dec_trivial },
-  lt_of_mul_lt_mul_left := by { rintro ⟨⟩ ⟨⟩ ⟨⟩; dec_trivial },
   zero_le_one := dec_trivial,
   .. foo.linear_order,
   .. foo.comm_monoid }

src/algebra/ordered_monoid.lean

@@ -28,24 +28,18 @@ universe u
 variable {α : Type u}
 
 /-- An ordered commutative monoid is a commutative monoid
-with a partial order such that
-  * `a ≤ b → c * a ≤ c * b` (multiplication is monotone)
-  * `a * b < a * c → b < c`.
+with a partial order such that `a ≤ b → c * a ≤ c * b` (multiplication is monotone)
 -/
 @[protect_proj, ancestor comm_monoid partial_order]
 class ordered_comm_monoid (α : Type*) extends comm_monoid α, partial_order α :=
 (mul_le_mul_left       : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b)
-(lt_of_mul_lt_mul_left : ∀ a b c : α, a * b < a * c → b < c)
 
 /-- An ordered (additive) commutative monoid is a commutative monoid
-  with a partial order such that
-  * `a ≤ b → c + a ≤ c + b` (addition is monotone)
-  * `a + b < a + c → b < c`.
+  with a partial order such that `a ≤ b → c + a ≤ c + b` (addition is monotone)
 -/
 @[protect_proj, ancestor add_comm_monoid partial_order]
 class ordered_add_comm_monoid (α : Type*) extends add_comm_monoid α, partial_order α :=
 (add_le_add_left       : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
-(lt_of_add_lt_add_left : ∀ a b c : α, a + b < a + c → b < c)
 
 attribute [to_additive] ordered_comm_monoid
 
@@ -56,27 +50,13 @@ instance ordered_comm_monoid.to_covariant_class_left (M : Type*) [ordered_comm_m
   covariant_class M M (*) (≤) :=
 { elim := λ a b c bc, ordered_comm_monoid.mul_le_mul_left _ _ bc a }
 
-@[to_additive]
-instance ordered_comm_monoid.to_contravariant_class_left (M : Type*) [ordered_comm_monoid M] :
-  contravariant_class M M (*) (<) :=
-{ elim := λ a b c, ordered_comm_monoid.lt_of_mul_lt_mul_left _ _ _ }
-
 /- This instance can be proven with `by apply_instance`.  However, `with_bot ℕ` does not
 pick up a `covariant_class M M (function.swap (*)) (≤)` instance without it (see PR #7940). -/
 @[to_additive]
 instance ordered_comm_monoid.to_covariant_class_right (M : Type*) [ordered_comm_monoid M] :
   covariant_class M M (swap (*)) (≤) :=
 covariant_swap_mul_le_of_covariant_mul_le M
 
-/- This instance can be proven with `by apply_instance`.  However, by analogy with the
-instance `ordered_comm_monoid.to_covariant_class_right` above, I imagine that without
-this instance, some Type would not have a `contravariant_class M M (function.swap (*)) (≤)`
-instance. -/
-@[to_additive]
-instance ordered_comm_monoid.to_contravariant_class_right (M : Type*) [ordered_comm_monoid M] :
-  contravariant_class M M (swap (*)) (<) :=
-contravariant_swap_mul_lt_of_contravariant_mul_lt M
-
 end ordered_instances
 
 /-- An `ordered_comm_monoid` with one-sided 'division' in the sense that
@@ -100,24 +80,12 @@ export has_exists_add_of_le (exists_add_of_le)
 /-- A linearly ordered additive commutative monoid. -/
 @[protect_proj, ancestor linear_order ordered_add_comm_monoid]
 class linear_ordered_add_comm_monoid (α : Type*)
-  extends linear_order α, ordered_add_comm_monoid α :=
-(lt_of_add_lt_add_left := λ x y z, by {
-  -- type-class inference uses `a : linear_order α` which it can't unfold, unless we provide this!
-  -- `lt_iff_le_not_le` gets filled incorrectly with `autoparam` if we don't provide that field.
-  letI : linear_order α := by refine { le := le, lt := lt, lt_iff_le_not_le := _, .. }; assumption,
-  apply lt_imp_lt_of_le_imp_le,
-  exact λ h, add_le_add_left _ _ h _ })
+  extends linear_order α, ordered_add_comm_monoid α.
 
 /-- A linearly ordered commutative monoid. -/
 @[protect_proj, ancestor linear_order ordered_comm_monoid, to_additive]
 class linear_ordered_comm_monoid (α : Type*)
-  extends linear_order α, ordered_comm_monoid α :=
-(lt_of_mul_lt_mul_left := λ x y z, by {
-  -- type-class inference uses `a : linear_order α` which it can't unfold, unless we provide this!
-  -- `lt_iff_le_not_le` gets filled incorrectly with `autoparam` if we don't provide that field.
-  letI : linear_order α := by refine { le := le, lt := lt, lt_iff_le_not_le := _, .. }; assumption,
-  apply lt_imp_lt_of_le_imp_le,
-  exact λ h, mul_le_mul_left _ _ h _ })
+  extends linear_order α, ordered_comm_monoid α.
 
 /-- A linearly ordered commutative monoid with a zero element. -/
 class linear_ordered_comm_monoid_with_zero (α : Type*)
@@ -158,8 +126,6 @@ def function.injective.ordered_comm_monoid [ordered_comm_monoid α] {β : Type*}
   ordered_comm_monoid β :=
 { mul_le_mul_left := λ a b ab c, show f (c * a) ≤ f (c * b), by
   { rw [mul, mul], apply mul_le_mul_left', exact ab },
-  lt_of_mul_lt_mul_left :=
-    λ a b c bc, show f b < f c, from lt_of_mul_lt_mul_left' (by rwa [← mul, ← mul] : (f a) * _ < _),
   ..partial_order.lift f hf,
   ..hf.comm_monoid f one mul }
 
@@ -273,7 +239,6 @@ end
 
 instance [ordered_comm_monoid α] : ordered_comm_monoid (with_zero α) :=
 { mul_le_mul_left := with_zero.mul_le_mul_left,
-  lt_of_mul_lt_mul_left := with_zero.lt_of_mul_lt_mul_left,
   ..with_zero.comm_monoid_with_zero,
   ..with_zero.partial_order }
 
@@ -295,17 +260,6 @@ begin
     add_le_add_left := this,
     ..with_zero.partial_order,
     ..with_zero.add_comm_monoid, .. },
-  { intros a b c h,
-    have h' := lt_iff_le_not_le.1 h,
-    rw lt_iff_le_not_le at ⊢,
-    refine ⟨λ b h₂, _, λ h₂, h'.2 $ this _ _ h₂ _⟩,
-    cases h₂, cases c with c,
-    { cases h'.2 (this _ _ bot_le a) },
-    { refine ⟨_, rfl, _⟩,
-      cases a with a,
-      { exact with_bot.some_le_some.1 h'.1 },
-      { exact le_of_lt (lt_of_add_lt_add_left $
-          with_bot.some_lt_some.1 h), } } },
   { intros a b h c ca h₂,
     cases b with b,
     { rw le_antisymm h bot_le at h₂,
@@ -420,15 +374,6 @@ instance [ordered_add_comm_monoid α] : ordered_add_comm_monoid (with_top α) :=
       simp only [some_eq_coe, ← coe_add, coe_le_coe] at h ⊢,
       exact add_le_add_left h c
     end,
-  lt_of_add_lt_add_left :=
-    begin
-      intros a b c h,
-      rcases lt_iff_exists_coe.1 h with ⟨ab, hab, hlt⟩,
-      rcases add_eq_coe.1 hab with ⟨a, b, rfl, rfl, rfl⟩,
-      rw coe_lt_iff,
-      rintro c rfl,
-      exact lt_of_add_lt_add_left (coe_lt_coe.1 hlt)
-    end,
   ..with_top.partial_order, ..with_top.add_comm_monoid }
 
 instance [linear_ordered_add_comm_monoid α] :
@@ -469,16 +414,6 @@ begin
     add_le_add_left := this,
     ..with_bot.partial_order,
     ..with_bot.add_comm_monoid, ..},
-  { intros a b c h,
-    have h' := h,
-    rw lt_iff_le_not_le at h' ⊢,
-    refine ⟨λ b h₂, _, λ h₂, h'.2 $ this _ _ h₂ _⟩,
-    cases h₂, cases a with a,
-    { exact (not_le_of_lt h).elim bot_le },
-    cases c with c,
-    { exact (not_le_of_lt h).elim bot_le },
-    { exact ⟨_, rfl, le_of_lt (lt_of_add_lt_add_left $
-        with_bot.some_lt_some.1 h)⟩ } },
   { intros a b h c ca h₂,
     cases c with c, {cases h₂},
     cases a with a; cases h₂,
@@ -733,12 +668,31 @@ class ordered_cancel_comm_monoid (α : Type u)
 section ordered_cancel_comm_monoid
 variables [ordered_cancel_comm_monoid α] {a b c d : α}
 
+@[to_additive]
+lemma ordered_cancel_comm_monoid.lt_of_mul_lt_mul_left : ∀ a b c : α, a * b < a * c → b < c :=
+λ a b c h, lt_of_le_not_le
+  (ordered_cancel_comm_monoid.le_of_mul_le_mul_left a b c h.le) $
+  mt (λ h, ordered_cancel_comm_monoid.mul_le_mul_left _ _ h _) (not_le_of_gt h)
+
+@[to_additive]
+instance ordered_cancel_comm_monoid.to_contravariant_class_left
+  (M : Type*) [ordered_cancel_comm_monoid M] :
+  contravariant_class M M (*) (<) :=
+{ elim := λ a b c, ordered_cancel_comm_monoid.lt_of_mul_lt_mul_left _ _ _ }
+
+/- This instance can be proven with `by apply_instance`.  However, by analogy with the
+instance `ordered_cancel_comm_monoid.to_covariant_class_right` above, I imagine that without
+this instance, some Type would not have a `contravariant_class M M (function.swap (*)) (<)`
+instance. -/
+@[to_additive]
+instance ordered_cancel_comm_monoid.to_contravariant_class_right
+  (M : Type*) [ordered_cancel_comm_monoid M] :
+  contravariant_class M M (swap (*)) (<) :=
+contravariant_swap_mul_lt_of_contravariant_mul_lt M
+
 @[priority 100, to_additive]    -- see Note [lower instance priority]
 instance ordered_cancel_comm_monoid.to_ordered_comm_monoid : ordered_comm_monoid α :=
-{ lt_of_mul_lt_mul_left := λ a b c h, lt_of_le_not_le
-      (ordered_cancel_comm_monoid.le_of_mul_le_mul_left a b c h.le) $
-      mt (λ h, ordered_cancel_comm_monoid.mul_le_mul_left _ _ h _) (not_le_of_gt h),
-  ..‹ordered_cancel_comm_monoid α› }
+{ ..‹ordered_cancel_comm_monoid α› }
 
 /-- Pullback an `ordered_cancel_comm_monoid` under an injective map.
 See note [reducible non-instances]. -/
@@ -943,7 +897,6 @@ instance covariant_class_swap_mul_lt [has_lt α] [has_mul α]
 @[to_additive]
 instance [ordered_comm_monoid α] : ordered_comm_monoid (order_dual α) :=
 { mul_le_mul_left := λ a b h c, mul_le_mul_left' h c,
-  lt_of_mul_lt_mul_left := λ a b c, lt_of_mul_lt_mul_left',
   .. order_dual.partial_order α,
   .. order_dual.comm_monoid }
 
@@ -995,13 +948,11 @@ instance : Π [linear_order α], linear_order (additive α) := id
 
 instance [ordered_add_comm_monoid α] : ordered_comm_monoid (multiplicative α) :=
 { mul_le_mul_left := @ordered_add_comm_monoid.add_le_add_left α _,
-  lt_of_mul_lt_mul_left := @ordered_add_comm_monoid.lt_of_add_lt_add_left α _,
   ..multiplicative.partial_order,
   ..multiplicative.comm_monoid }
 
 instance [ordered_comm_monoid α] : ordered_add_comm_monoid (additive α) :=
 { add_le_add_left := @ordered_comm_monoid.mul_le_mul_left α _,
-  lt_of_add_lt_add_left := @ordered_comm_monoid.lt_of_mul_lt_mul_left α _,
   ..additive.partial_order,
   ..additive.add_comm_monoid }
 

src/algebra/ordered_sub.lean

@@ -413,8 +413,8 @@ protected lemma lt_sub_iff_left_of_le (hc : add_le_cancellable c) (h : c ≤ b)
   a < b - c ↔ c + a < b :=
 by { rw [add_comm], exact hc.lt_sub_iff_right_of_le h }
 
-protected lemma lt_of_sub_lt_sub_left_of_le (hb : add_le_cancellable b) (hca : c ≤ a)
-  (h : a - b < a - c) : c < b :=
+protected lemma lt_of_sub_lt_sub_left_of_le [contravariant_class α α (+) (<)]
+  (hb : add_le_cancellable b) (hca : c ≤ a) (h : a - b < a - c) : c < b :=
 begin
   conv_lhs at h { rw [← sub_add_cancel_of_le hca] },
   exact lt_of_add_lt_add_left (hb.lt_add_of_sub_lt_right h),
@@ -441,8 +441,9 @@ protected lemma sub_inj_right (hab : add_le_cancellable (a - b)) (h₁ : b ≤ a
   (h₃ : a - b = a - c) : b = c :=
 by { rw ← hab.inj, rw [sub_add_cancel_of_le h₁, h₃, sub_add_cancel_of_le h₂] }
 
-protected lemma sub_lt_sub_iff_left_of_le_of_le (hb : add_le_cancellable b)
-  (hab : add_le_cancellable (a - b)) (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < a - c ↔ c < b :=
+protected lemma sub_lt_sub_iff_left_of_le_of_le [contravariant_class α α (+) (<)]
+  (hb : add_le_cancellable b) (hab : add_le_cancellable (a - b)) (h₁ : b ≤ a) (h₂ : c ≤ a) :
+  a - b < a - c ↔ c < b :=
 begin
   refine ⟨hb.lt_of_sub_lt_sub_left_of_le h₂, _⟩,
   intro h, refine (sub_le_sub_left' h.le _).lt_of_ne _,
@@ -516,7 +517,8 @@ lemma lt_sub_iff_left_of_le (h : c ≤ b) : a < b - c ↔ c + a < b :=
 contravariant.add_le_cancellable.lt_sub_iff_left_of_le h
 
 /-- See `lt_of_sub_lt_sub_left` for a stronger statement in a linear order. -/
-lemma lt_of_sub_lt_sub_left_of_le (hca : c ≤ a) (h : a - b < a - c) : c < b :=
+lemma lt_of_sub_lt_sub_left_of_le  [contravariant_class α α (+) (<)]
+  (hca : c ≤ a) (h : a - b < a - c) : c < b :=
 contravariant.add_le_cancellable.lt_of_sub_lt_sub_left_of_le hca h
 
 lemma sub_le_sub_iff_left' (h : c ≤ a) : a - b ≤ a - c ↔ c ≤ b :=
@@ -533,7 +535,8 @@ lemma sub_inj_right (h₁ : b ≤ a) (h₂ : c ≤ a) (h₃ : a - b = a - c) : b
 contravariant.add_le_cancellable.sub_inj_right h₁ h₂ h₃
 
 /-- See `sub_lt_sub_iff_left_of_le` for a stronger statement in a linear order. -/
-lemma sub_lt_sub_iff_left_of_le_of_le (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < a - c ↔ c < b :=
+lemma sub_lt_sub_iff_left_of_le_of_le  [contravariant_class α α (+) (<)]
+  (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < a - c ↔ c < b :=
 contravariant.add_le_cancellable.sub_lt_sub_iff_left_of_le_of_le
   contravariant.add_le_cancellable h₁ h₂
 

src/algebra/punit_instances.lean

@@ -56,8 +56,7 @@ intros; trivial <|> simp only [eq_iff_true_of_subsingleton]
 
 instance : canonically_ordered_add_monoid punit :=
 by refine
-{ lt_of_add_lt_add_left := λ _ _ _, id,
-  le_iff_exists_add := λ _ _, iff_of_true _ ⟨star, subsingleton.elim _ _⟩,
+{ le_iff_exists_add := λ _ _, iff_of_true _ ⟨star, subsingleton.elim _ _⟩,
   .. punit.comm_ring, .. punit.complete_boolean_algebra, .. };
 intros; trivial
 

src/data/multiset/basic.lean

@@ -410,8 +410,7 @@ theorem le_iff_exists_add {s t : multiset α} : s ≤ t ↔ ∃ u, t = s + u :=
  λ ⟨u, e⟩, e.symm ▸ le_add_right _ _⟩
 
 instance : canonically_ordered_add_monoid (multiset α) :=
-{ lt_of_add_lt_add_left := λ a b c, (add_lt_add_iff_left a).mp,
-  le_iff_exists_add     := @le_iff_exists_add _,
+{ le_iff_exists_add     := @le_iff_exists_add _,
   bot                   := 0,
   bot_le                := multiset.zero_le,
   ..multiset.ordered_cancel_add_comm_monoid }

src/data/nat/enat.lean

@@ -259,14 +259,6 @@ instance : ordered_add_comm_monoid enat :=
     enat.cases_on c (by simp)
       (λ c, ⟨λ h, and.intro trivial (h₁ h.2),
         λ _, add_le_add_left (h₂ _) c⟩),
-  lt_of_add_lt_add_left := λ a b c, enat.cases_on a
-    (λ h, by simpa [lt_irrefl] using h)
-    (λ a, enat.cases_on b
-      (λ h, absurd h (not_lt_of_ge (by rw add_top; exact le_top)))
-      (λ b, enat.cases_on c
-        (λ _, coe_lt_top _)
-        (λ c h,  coe_lt_coe.2 (by rw [← coe_add, ← coe_add, coe_lt_coe] at h;
-            exact lt_of_add_lt_add_left h)))),
   ..enat.linear_order,
   ..enat.add_comm_monoid }
 

src/data/real/nnreal.lean

@@ -267,8 +267,6 @@ instance : order_bot ℝ≥0 :=
 instance : canonically_linear_ordered_add_monoid ℝ≥0 :=
 { add_le_add_left       := assume a b h c,
     nnreal.coe_le_coe.mp $ (add_le_add_left (nnreal.coe_le_coe.mpr h) c),
-  lt_of_add_lt_add_left := assume a b c bc,
-    nnreal.coe_lt_coe.mp $ lt_of_add_lt_add_left (nnreal.coe_lt_coe.mpr bc),
   le_iff_exists_add     := assume ⟨a, ha⟩ ⟨b, hb⟩,
     iff.intro
       (assume h : a ≤ b,

src/set_theory/cardinal.lean

@@ -306,7 +306,6 @@ instance : order_bot cardinal.{u} :=
 
 instance : canonically_ordered_comm_semiring cardinal.{u} :=
 { add_le_add_left       := λ a b h c, cardinal.add_le_add_left _ h,
-  lt_of_add_lt_add_left := λ a b c, lt_imp_lt_of_le_imp_le (cardinal.add_le_add_left _),
   le_iff_exists_add     := @cardinal.le_iff_exists_add,
   eq_zero_or_eq_zero_of_mul_eq_zero := @cardinal.eq_zero_or_eq_zero_of_mul_eq_zero,
   ..cardinal.order_bot,