feat(algebra/ordered_sub): define truncated subtraction in general (#8503)

* Define and prove properties of truncated subtraction in general
* We currently only instantiate it for `nat`. The other types (`multiset`, `finsupp`, `nnreal`, `ennreal`, ...) will be in future PRs.

Todo in future PRs:
* Provide `has_ordered_sub` instances for all specific cases
* Remove the lemmas specific to each individual type



Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>

Author: fpvandoorn

src/algebra/covariant_and_contravariant.lean

@@ -235,6 +235,11 @@ instance contravariant_mul_lt_of_covariant_mul_le [has_mul N] [linear_order N]
   [covariant_class N N (*) (≤)] : contravariant_class N N (*) (<) :=
 { elim := (covariant_le_iff_contravariant_lt N N (*)).mp covariant_class.elim }
 
+@[to_additive]
+instance covariant_mul_lt_of_contravariant_mul_le [has_mul N] [linear_order N]
+  [contravariant_class N N (*) (≤)] : covariant_class N N (*) (<) :=
+{ elim := (covariant_lt_iff_contravariant_le N N (*)).mpr contravariant_class.elim }
+
 @[to_additive]
 instance covariant_swap_mul_le_of_covariant_mul_le [comm_semigroup N] [has_le N]
   [covariant_class N N (*) (≤)] : covariant_class N N (function.swap (*)) (≤) :=

src/algebra/ordered_monoid.lean

@@ -253,7 +253,7 @@ begin
     exact covariant_class.elim _ h }
 end
 
-lemma lt_of_mul_lt_mul_left  {α : Type u} [has_mul α] [partial_order α]
+lemma lt_of_mul_lt_mul_left {α : Type u} [has_mul α] [partial_order α]
   [contravariant_class α α (*) (<)] :
   ∀ (a b c : with_zero α), a * b < a * c → b < c :=
 begin
@@ -581,6 +581,17 @@ calc a = a * 1 : by simp
 @[to_additive] lemma le_self_mul : a ≤ a * c :=
 le_mul_right (le_refl a)
 
+@[to_additive]
+lemma lt_iff_exists_mul [covariant_class α α (*) (<)] : a < b ↔ ∃ c > 1, b = a * c :=
+begin
+  simp_rw [lt_iff_le_and_ne, and_comm, le_iff_exists_mul, ← exists_and_distrib_left, exists_prop],
+  apply exists_congr, intro c,
+  rw [and.congr_left_iff, gt_iff_lt], rintro rfl,
+  split,
+  { rw [one_lt_iff_ne_one], apply mt, rintro rfl, rw [mul_one] },
+  { rw [← (self_le_mul_right a c).lt_iff_ne], apply lt_mul_of_one_lt_right' }
+end
+
 local attribute [semireducible] with_zero
 
 -- This instance looks absurd: a monoid already has a zero
@@ -645,11 +656,10 @@ class canonically_linear_ordered_monoid (α : Type*)
       extends canonically_ordered_monoid α, linear_order α
 
 section canonically_linear_ordered_monoid
-variables
+variables [canonically_linear_ordered_monoid α]
 
 @[priority 100, to_additive]  -- see Note [lower instance priority]
-instance canonically_linear_ordered_monoid.semilattice_sup_bot
-  [canonically_linear_ordered_monoid α] : semilattice_sup_bot α :=
+instance canonically_linear_ordered_monoid.semilattice_sup_bot : semilattice_sup_bot α :=
 { ..lattice_of_linear_order, ..canonically_ordered_monoid.to_order_bot α }
 
 instance with_top.canonically_linear_ordered_add_monoid
@@ -658,8 +668,8 @@ instance with_top.canonically_linear_ordered_add_monoid
 { .. (infer_instance : canonically_ordered_add_monoid (with_top α)),
   .. (infer_instance : linear_order (with_top α)) }
 
-@[to_additive] lemma min_mul_distrib [canonically_linear_ordered_monoid α] (a b c : α) :
-  min a (b * c) = min a (min a b * min a c) :=
+@[to_additive]
+lemma min_mul_distrib (a b c : α) : min a (b * c) = min a (min a b * min a c) :=
 begin
   cases le_total a b with hb hb,
   { simp [hb, le_mul_right] },
@@ -668,10 +678,18 @@ begin
     { simp [hb, hc] } }
 end
 
-@[to_additive] lemma min_mul_distrib' [canonically_linear_ordered_monoid α] (a b c : α) :
-  min (a * b) c = min (min a c * min b c) c :=
+@[to_additive]
+lemma min_mul_distrib' (a b c : α) : min (a * b) c = min (min a c * min b c) c :=
 by simpa [min_comm _ c] using min_mul_distrib c a b
 
+@[simp, to_additive]
+lemma one_min (a : α) : min 1 a = 1 :=
+min_eq_left (one_le a)
+
+@[simp, to_additive]
+lemma min_one (a : α) : min a 1 = 1 :=
+min_eq_right (one_le a)
+
 end canonically_linear_ordered_monoid
 
 /-- An ordered cancellative additive commutative monoid

src/algebra/ordered_monoid_lemmas.lean

@@ -20,34 +20,23 @@ The reason is that we did not want to change existing names in the library.
 
 ## Remark
 
-No monoid is actually present in this file: all assumptions have been generalized to `has_mul` or
-`mul_one_class`.
+Almost no monoid is actually present in this file: most assumptions have been generalized to
+`has_mul` or `mul_one_class`.
 
 -/
 
 -- TODO: If possible, uniformize lemma names, taking special care of `'`,
 -- after the `ordered`-refactor is done.
 
+open function
+
 variables {α : Type*}
 section has_mul
 variables [has_mul α]
 
 section has_le
 variables [has_le α]
 
-@[simp, to_additive]
-lemma mul_le_mul_iff_left [covariant_class α α (*) (≤)] [contravariant_class α α (*) (≤)]
-  (a : α) {b c : α} :
-  a * b ≤ a * c ↔ b ≤ c :=
-rel_iff_cov α α (*) (≤) a
-
-@[simp, to_additive]
-lemma mul_le_mul_iff_right
-  [covariant_class α α (function.swap (*)) (≤)] [contravariant_class α α (function.swap (*)) (≤)]
-  (a : α) {b c : α} :
-  b * a ≤ c * a ↔ b ≤ c :=
-rel_iff_cov α α (function.swap (*)) (≤) a
-
 /- The prime on this lemma is present only on the multiplicative version.  The unprimed version
 is taken by the analogous lemma for semiring, with an extra non-negativity assumption. -/
 @[to_additive add_le_add_left]
@@ -75,6 +64,19 @@ lemma le_of_mul_le_mul_right' [contravariant_class α α (function.swap (*)) (
   b ≤ c :=
 contravariant_class.elim a bc
 
+@[simp, to_additive]
+lemma mul_le_mul_iff_left [covariant_class α α (*) (≤)] [contravariant_class α α (*) (≤)]
+  (a : α) {b c : α} :
+  a * b ≤ a * c ↔ b ≤ c :=
+rel_iff_cov α α (*) (≤) a
+
+@[simp, to_additive]
+lemma mul_le_mul_iff_right
+  [covariant_class α α (function.swap (*)) (≤)] [contravariant_class α α (function.swap (*)) (≤)]
+  (a : α) {b c : α} :
+  b * a ≤ c * a ↔ b ≤ c :=
+rel_iff_cov α α (function.swap (*)) (≤) a
+
 end has_le
 
 section has_lt
@@ -361,6 +363,17 @@ calc  a * b ≤ a * 1 : mul_le_mul_left' h a
 
 end mul_one_class
 
+@[to_additive]
+lemma mul_left_cancel'' [semigroup α] [partial_order α]
+  [contravariant_class α α (*) (≤)] {a b c : α} (h : a * b = a * c) : b = c :=
+(le_of_mul_le_mul_left' h.le).antisymm (le_of_mul_le_mul_left' h.ge)
+
+@[to_additive]
+lemma mul_right_cancel'' [semigroup α] [partial_order α]
+  [contravariant_class α α (function.swap (*)) (≤)] {a b c : α} (h : a * b = c * b) :
+  a = c :=
+le_antisymm (le_of_mul_le_mul_right' h.le) (le_of_mul_le_mul_right' h.ge)
+
 /- This is not instance, since we want to have an instance from `left_cancel_semigroup`s
 to the appropriate `covariant_class`. -/
 /--  A semigroup with a partial order and satisfying `left_cancel_semigroup`
@@ -369,10 +382,9 @@ to the appropriate `covariant_class`. -/
 "An additive semigroup with a partial order and satisfying `left_cancel_add_semigroup`
 (i.e. `c + a < c + b → a < b`) is a `left_cancel add_semigroup`."]
 def contravariant.to_left_cancel_semigroup [semigroup α] [partial_order α]
-  [contravariant_class α α ((*) : α → α → α) (≤)] :
+  [contravariant_class α α (*) (≤)] :
   left_cancel_semigroup α :=
-{ mul_left_cancel := λ a b c bc,
-    (le_of_mul_le_mul_left' bc.le).antisymm (le_of_mul_le_mul_left' bc.ge),
+{ mul_left_cancel := λ a b c, mul_left_cancel''
   ..‹semigroup α› }
 
 /- This is not instance, since we want to have an instance from `right_cancel_semigroup`s
@@ -383,10 +395,9 @@ to the appropriate `covariant_class`. -/
 "An additive semigroup with a partial order and satisfying `right_cancel_add_semigroup`
 (`a + c < b + c → a < b`) is a `right_cancel add_semigroup`."]
 def contravariant.to_right_cancel_semigroup [semigroup α] [partial_order α]
-  [contravariant_class α α (function.swap (*) : α → α → α) (≤)] :
+  [contravariant_class α α (function.swap (*)) (≤)] :
   right_cancel_semigroup α :=
-{ mul_right_cancel := λ a b c bc,
-    le_antisymm (le_of_mul_le_mul_right' bc.le) (le_of_mul_le_mul_right' bc.ge)
+{ mul_right_cancel := λ a b c, mul_right_cancel''
   ..‹semigroup α› }
 
 variables {a b c d : α}
@@ -740,3 +751,78 @@ lemma strict_mono.mul_monotone' (hf : strict_mono f) (hg : monotone g) :
 λ x y h, mul_lt_mul_of_lt_of_le (hf h) (hg h.le)
 
 end strict_mono
+
+/--
+An element `a : α` is `mul_le_cancellable` if `x ↦ a * x` is order-reflecting.
+We will make a separate version of many lemmas that require `[contravariant_class α α (*) (≤)]` with
+`mul_le_cancellable` assumptions instead. These lemmas can then be instantiated to specific types,
+like `ennreal`, where we can replace the assumption `add_le_cancellable x` by `x ≠ ∞`.
+-/
+@[to_additive /-" An element `a : α` is `add_le_cancellable` if `x ↦ a + x` is order-reflecting.
+We will make a separate version of many lemmas that require `[contravariant_class α α (+) (≤)]` with
+`mul_le_cancellable` assumptions instead. These lemmas can then be instantiated to specific types,
+like `ennreal`, where we can replace the assumption `add_le_cancellable x` by `x ≠ ∞`. "-/
+]
+def mul_le_cancellable [has_mul α] [has_le α] (a : α) : Prop :=
+∀ ⦃b c⦄, a * b ≤ a * c → b ≤ c
+
+@[to_additive]
+lemma contravariant.mul_le_cancellable [has_mul α] [has_le α] [contravariant_class α α (*) (≤)]
+  {a : α} : mul_le_cancellable a :=
+λ b c, le_of_mul_le_mul_left'
+
+namespace mul_le_cancellable
+
+@[to_additive]
+protected lemma injective [has_mul α] [partial_order α] {a : α} (ha : mul_le_cancellable a) :
+  injective ((*) a) :=
+λ b c h, le_antisymm (ha h.le) (ha h.ge)
+
+@[to_additive]
+protected lemma inj [has_mul α] [partial_order α] {a b c : α} (ha : mul_le_cancellable a) :
+  a * b = a * c ↔ b = c :=
+ha.injective.eq_iff
+
+@[to_additive]
+protected lemma injective_left [comm_semigroup α] [partial_order α] {a : α}
+  (ha : mul_le_cancellable a) : injective (* a) :=
+λ b c h, ha.injective $ by rwa [mul_comm a, mul_comm a]
+
+@[to_additive]
+protected lemma inj_left [comm_semigroup α] [partial_order α] {a b c : α}
+  (hc : mul_le_cancellable c) : a * c = b * c ↔ a = b :=
+hc.injective_left.eq_iff
+
+variable [has_le α]
+
+@[to_additive]
+protected lemma mul_le_mul_iff_left [has_mul α] [covariant_class α α (*) (≤)]
+  {a b c : α} (ha : mul_le_cancellable a) : a * b ≤ a * c ↔ b ≤ c :=
+⟨λ h, ha h, λ h, mul_le_mul_left' h a⟩
+
+@[to_additive]
+protected lemma mul_le_mul_iff_right [comm_semigroup α] [covariant_class α α (*) (≤)]
+  {a b c : α} (ha : mul_le_cancellable a) : b * a ≤ c * a ↔ b ≤ c :=
+by rw [mul_comm b, mul_comm c, ha.mul_le_mul_iff_left]
+
+@[to_additive]
+protected lemma le_mul_iff_one_le_right [mul_one_class α] [covariant_class α α (*) (≤)]
+  {a b : α} (ha : mul_le_cancellable a) : a ≤ a * b ↔ 1 ≤ b :=
+iff.trans (by rw [mul_one]) ha.mul_le_mul_iff_left
+
+@[to_additive]
+protected lemma mul_le_iff_le_one_right [mul_one_class α] [covariant_class α α (*) (≤)]
+  {a b : α} (ha : mul_le_cancellable a) : a * b ≤ a ↔ b ≤ 1 :=
+iff.trans (by rw [mul_one]) ha.mul_le_mul_iff_left
+
+@[to_additive]
+protected lemma le_mul_iff_one_le_left [comm_monoid α] [covariant_class α α (*) (≤)]
+  {a b : α} (ha : mul_le_cancellable a) : a ≤ b * a ↔ 1 ≤ b :=
+by rw [mul_comm, ha.le_mul_iff_one_le_right]
+
+@[to_additive]
+protected lemma mul_le_iff_le_one_left [comm_monoid α] [covariant_class α α (*) (≤)]
+  {a b : α} (ha : mul_le_cancellable a) : b * a ≤ a ↔ b ≤ 1 :=
+by rw [mul_comm, ha.mul_le_iff_le_one_right]
+
+end mul_le_cancellable