From 49f5a1596bf25e56af7fc54d42305fdbb834dd67 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 10 Jun 2021 16:03:35 +0000
Subject: [PATCH] =?UTF-8?q?feat(algebra/ordered=5Fring):=20more=20granular?=
 =?UTF-8?q?=20typeclasses=20for=20`with=5Ftop=20=CE=B1`=20and=20`with=5Fbo?=
 =?UTF-8?q?t=20=CE=B1`=20(#7845)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`with_top α` and `with_bot α` now inherit the following typeclasses from `α` with suitable assumptions:

* `mul_zero_one_class`
* `semigroup_with_zero`
* `monoid_with_zero`
* `comm_monoid_with_zero`

These were all split out of the existing `canonically_ordered_comm_semiring`, with their proofs unchanged.
The same instances are added for `with_bot`.

It is not possible to split further, as `distrib'` requires `add_eq_zero_iff`, and `canonically_ordered_comm_semiring` is the smallest typeclass that provides both this lemma and `mul_zero_class`.

With these instances in place, we can now show `comm_monoid_with_zero ereal`.
---
 src/algebra/ordered_ring.lean  | 184 +++++++++++++++++++++++++--------
 src/data/real/ereal.lean       |  42 +++++++-
 src/order/bounded_lattice.lean |   5 +
 3 files changed, 184 insertions(+), 47 deletions(-)

diff --git a/src/algebra/ordered_ring.lean b/src/algebra/ordered_ring.lean
index 3a4acddbee89d..427851dd9e104 100644
--- a/src/algebra/ordered_ring.lean
+++ b/src/algebra/ordered_ring.lean
@@ -1346,6 +1346,12 @@ by simp only [pos_iff_ne_zero, ne.def, mul_eq_zero, not_or_distrib]
 
 end canonically_ordered_semiring
 
+/-! ### Structures involving `*` and `0` on `with_top` and `with_bot`
+
+The main results of this section are `with_top.canonically_ordered_comm_semiring` and
+`with_bot.comm_monoid_with_zero`.
+-/
+
 namespace with_top
 
 instance [nonempty α] : nontrivial (with_top α) :=
@@ -1402,27 +1408,67 @@ begin
   { simp [← coe_mul] }
 end
 
-end mul_zero_class
+lemma mul_lt_top [partial_order α] {a b : with_top α} (ha : a < ⊤) (hb : b < ⊤) : a * b < ⊤ :=
+begin
+  lift a to α using ne_top_of_lt ha,
+  lift b to α using ne_top_of_lt hb,
+  simp only [← coe_mul, coe_lt_top]
+end
 
-section no_zero_divisors
+end mul_zero_class
 
-variables [mul_zero_class α] [no_zero_divisors α]
+/-- `nontrivial α` is needed here as otherwise we have `1 * ⊤ = ⊤` but also `= 0 * ⊤ = 0`. -/
+instance [mul_zero_one_class α] [nontrivial α] : mul_zero_one_class (with_top α) :=
+{ mul := (*),
+  one := 1,
+  zero := 0,
+  one_mul := λ a, match a with
+  | none     := show ((1:α) : with_top α) * ⊤ = ⊤, by simp [-with_top.coe_one]
+  | (some a) := show ((1:α) : with_top α) * a = a, by simp [coe_mul.symm, -with_top.coe_one]
+  end,
+  mul_one := λ a, match a with
+  | none     := show ⊤ * ((1:α) : with_top α) = ⊤, by simp [-with_top.coe_one]
+  | (some a) := show ↑a * ((1:α) : with_top α) = a, by simp [coe_mul.symm, -with_top.coe_one]
+  end,
+  .. with_top.mul_zero_class }
 
-instance : no_zero_divisors (with_top α) :=
+instance [mul_zero_class α] [no_zero_divisors α] : no_zero_divisors (with_top α) :=
 ⟨λ a b, by cases a; cases b; dsimp [mul_def]; split_ifs;
   simp [*, none_eq_top, some_eq_coe, mul_eq_zero] at *⟩
 
-end no_zero_divisors
+instance [semigroup_with_zero α] [no_zero_divisors α] : semigroup_with_zero (with_top α) :=
+{ mul := (*),
+  zero := 0,
+  mul_assoc := λ a b c, begin
+    cases a,
+    { by_cases hb : b = 0; by_cases hc : c = 0;
+        simp [*, none_eq_top] },
+    cases b,
+    { by_cases ha : a = 0; by_cases hc : c = 0;
+        simp [*, none_eq_top, some_eq_coe] },
+    cases c,
+    { by_cases ha : a = 0; by_cases hb : b = 0;
+        simp [*, none_eq_top, some_eq_coe] },
+    simp [some_eq_coe, coe_mul.symm, mul_assoc]
+  end,
+  .. with_top.mul_zero_class }
+
+instance [monoid_with_zero α] [no_zero_divisors α] [nontrivial α] : monoid_with_zero (with_top α) :=
+{ .. with_top.mul_zero_one_class, .. with_top.semigroup_with_zero }
+
+instance [comm_monoid_with_zero α] [no_zero_divisors α] [nontrivial α] :
+  comm_monoid_with_zero (with_top α) :=
+{ mul := (*),
+  zero := 0,
+  mul_comm := λ a b, begin
+    by_cases ha : a = 0, { simp [ha] },
+    by_cases hb : b = 0, { simp [hb] },
+    simp [ha, hb, mul_def, option.bind_comm a b, mul_comm]
+  end,
+  .. with_top.monoid_with_zero }
 
 variables [canonically_ordered_comm_semiring α]
 
-private lemma comm (a b : with_top α) : a * b = b * a :=
-begin
-  by_cases ha : a = 0, { simp [ha] },
-  by_cases hb : b = 0, { simp [hb] },
-  simp [ha, hb, mul_def, option.bind_comm a b, mul_comm]
-end
-
 private lemma distrib' (a b c : with_top α) : (a + b) * c = a * c + b * c :=
 begin
   cases c,
@@ -1434,43 +1480,91 @@ begin
     repeat { refl <|> exact congr_arg some (add_mul _ _ _) } }
 end
 
-private lemma assoc (a b c : with_top α) : (a * b) * c = a * (b * c) :=
-begin
-  cases a,
-  { by_cases hb : b = 0; by_cases hc : c = 0;
-      simp [*, none_eq_top] },
-  cases b,
-  { by_cases ha : a = 0; by_cases hc : c = 0;
-      simp [*, none_eq_top, some_eq_coe] },
-  cases c,
-  { by_cases ha : a = 0; by_cases hb : b = 0;
-      simp [*, none_eq_top, some_eq_coe] },
-  simp [some_eq_coe, coe_mul.symm, mul_assoc]
-end
-
--- `nontrivial α` is needed here as otherwise
--- we have `1 * ⊤ = ⊤` but also `= 0 * ⊤ = 0`.
-private lemma one_mul' [nontrivial α] : ∀a : with_top α, 1 * a = a
-| none     := show ((1:α) : with_top α) * ⊤ = ⊤, by simp [-with_top.coe_one]
-| (some a) := show ((1:α) : with_top α) * a = a, by simp [coe_mul.symm, -with_top.coe_one]
+/-- This instance requires `canonically_ordered_comm_semiring` as it is the smallest class
+that derives from both `non_assoc_non_unital_semiring` and `canonically_ordered_add_monoid`, both
+of which are required for distributivity. -/
+instance [nontrivial α] : comm_semiring (with_top α) :=
+{ right_distrib   := distrib',
+  left_distrib    := assume a b c, by rw [mul_comm, distrib', mul_comm b, mul_comm c]; refl,
+  .. with_top.add_comm_monoid, .. with_top.comm_monoid_with_zero,}
 
 instance [nontrivial α] : canonically_ordered_comm_semiring (with_top α) :=
-{ one             := (1 : α),
-  right_distrib   := distrib',
-  left_distrib    := assume a b c, by rw [comm, distrib', comm b, comm c]; refl,
-  mul_assoc       := assoc,
-  mul_comm        := comm,
-  one_mul         := one_mul',
-  mul_one         := assume a, by rw [comm, one_mul'],
-  .. with_top.add_comm_monoid, .. with_top.mul_zero_class,
+{ .. with_top.comm_semiring,
   .. with_top.canonically_ordered_add_monoid,
-  .. with_top.no_zero_divisors, .. with_top.nontrivial }
+  .. with_top.no_zero_divisors, }
+
+end with_top
+
+namespace with_bot
+
+instance [nonempty α] : nontrivial (with_bot α) :=
+option.nontrivial
+
+variable [decidable_eq α]
+
+section has_mul
+
+variables [has_zero α] [has_mul α]
+
+instance : mul_zero_class (with_bot α) :=
+with_top.mul_zero_class
+
+lemma mul_def {a b : with_bot α} :
+  a * b = if a = 0 ∨ b = 0 then 0 else a.bind (λa, b.bind $ λb, ↑(a * b)) := rfl
+
+@[simp] lemma mul_bot {a : with_bot α} (h : a ≠ 0) : a * ⊥ = ⊥ :=
+with_top.mul_top h
+
+@[simp] lemma bot_mul {a : with_bot α} (h : a ≠ 0) : ⊥ * a = ⊥ :=
+with_top.top_mul h
+
+@[simp] lemma bot_mul_bot : (⊥ * ⊥ : with_bot α) = ⊥ :=
+with_top.top_mul_top
+
+end has_mul
+
+section mul_zero_class
+
+variables [mul_zero_class α]
 
-lemma mul_lt_top [nontrivial α] {a b : with_top α} (ha : a < ⊤) (hb : b < ⊤) : a * b < ⊤ :=
+@[norm_cast] lemma coe_mul {a b : α} : (↑(a * b) : with_bot α) = a * b :=
+decidable.by_cases (assume : a = 0, by simp [this]) $ assume ha,
+decidable.by_cases (assume : b = 0, by simp [this]) $ assume hb,
+by { simp [*, mul_def], refl }
+
+lemma mul_coe {b : α} (hb : b ≠ 0) {a : with_bot α} : a * b = a.bind (λa:α, ↑(a * b)) :=
+with_top.mul_coe hb
+
+@[simp] lemma mul_eq_bot_iff {a b : with_bot α} : a * b = ⊥ ↔ (a ≠ 0 ∧ b = ⊥) ∨ (a = ⊥ ∧ b ≠ 0) :=
+with_top.mul_eq_top_iff
+
+lemma bot_lt_mul [partial_order α] {a b : with_bot α} (ha : ⊥ < a) (hb : ⊥ < b) : ⊥ < a * b :=
 begin
-  lift a to α using ne_top_of_lt ha,
-  lift b to α using ne_top_of_lt hb,
-  simp only [← coe_mul, coe_lt_top]
+  lift a to α using ne_bot_of_gt ha,
+  lift b to α using ne_bot_of_gt hb,
+  simp only [← coe_mul, bot_lt_coe],
 end
 
-end with_top
+end mul_zero_class
+
+/-- `nontrivial α` is needed here as otherwise we have `1 * ⊥ = ⊥` but also `= 0 * ⊥ = 0`. -/
+instance [mul_zero_one_class α] [nontrivial α] : mul_zero_one_class (with_bot α) :=
+with_top.mul_zero_one_class
+
+instance [mul_zero_class α] [no_zero_divisors α] : no_zero_divisors (with_bot α) :=
+with_top.no_zero_divisors
+
+instance [semigroup_with_zero α] [no_zero_divisors α] : semigroup_with_zero (with_bot α) :=
+with_top.semigroup_with_zero
+
+instance [monoid_with_zero α] [no_zero_divisors α] [nontrivial α] : monoid_with_zero (with_bot α) :=
+with_top.monoid_with_zero
+
+instance [comm_monoid_with_zero α] [no_zero_divisors α] [nontrivial α] :
+  comm_monoid_with_zero (with_bot α) :=
+with_top.comm_monoid_with_zero
+
+instance [canonically_ordered_comm_semiring α] [nontrivial α] : comm_semiring (with_bot α) :=
+with_top.comm_semiring
+
+end with_bot
diff --git a/src/data/real/ereal.lean b/src/data/real/ereal.lean
index 79f4e363d74c0..6bf6b77d41281 100644
--- a/src/data/real/ereal.lean
+++ b/src/data/real/ereal.lean
@@ -23,6 +23,9 @@ to a group structure. Our choice is that `⊥ + ⊤ = ⊤ + ⊥ = ⊤`.
 An ad hoc subtraction is then defined by `x - y = x + (-y)`. It does not have nice properties,
 but it is sometimes convenient to have.
 
+An ad hoc multiplication is defined, for which `ereal` is a `comm_monoid_with_zero`.
+This does not distribute with addition, as `⊤ = ⊤ - ⊥ = 1*⊤ - 1*⊤ ≠ (1 - 1) * ⊤ = 0 * ⊤ = 0`.
+
 `ereal` is a `complete_linear_order`; this is deduced by type class inference from
 the fact that `with_top (with_bot L)` is a complete linear order if `L` is
 a conditionally complete linear order.
@@ -49,7 +52,7 @@ See https://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Extended_Real.html
 open_locale ennreal nnreal
 
 /-- ereal : The type `[-∞, ∞]` -/
-@[derive [order_bot, order_top,
+@[derive [order_bot, order_top, comm_monoid_with_zero,
   has_Sup, has_Inf, complete_linear_order, linear_ordered_add_comm_monoid_with_top]]
 def ereal := with_top (with_bot ℝ)
 
@@ -288,7 +291,7 @@ begin
   { simp [lt_top_iff_ne_top, with_top.add_eq_top, h1.ne, (h2.trans_le le_top).ne] }
 end
 
-@[simp] lemma ad_eq_top_iff {x y : ereal} : x + y = ⊤ ↔ x = ⊤ ∨ y = ⊤ :=
+@[simp] lemma add_eq_top_iff {x y : ereal} : x + y = ⊤ ↔ x = ⊤ ∨ y = ⊤ :=
 begin
   rcases x.cases with rfl|⟨x, rfl⟩|rfl; rcases y.cases with rfl|⟨x, rfl⟩|rfl;
   simp [← ereal.coe_add],
@@ -393,6 +396,13 @@ protected noncomputable def sub (x y : ereal) : ereal := x + (-y)
 
 noncomputable instance : has_sub ereal := ⟨ereal.sub⟩
 
+@[simp] lemma top_sub (x : ereal) : ⊤ - x = ⊤ := top_add x
+@[simp] lemma sub_bot (x : ereal) : x - ⊥ = ⊤ := add_top x
+
+@[simp] lemma bot_sub_top : (⊥ : ereal) - ⊤ = ⊥ := rfl
+@[simp] lemma bot_sub_coe (x : ℝ) : (⊥ : ereal) - x = ⊥ := rfl
+@[simp] lemma coe_sub_bot (x : ℝ) : (x : ereal) - ⊤ = ⊥ := rfl
+
 @[simp] lemma sub_zero (x : ereal) : x - 0 = x := by { change x + (-0) = x, simp }
 @[simp] lemma zero_sub (x : ereal) : 0 - x = - x := by { change 0 + (-x) = - x, simp }
 
@@ -430,4 +440,32 @@ begin
   { simpa using h'y }
 end
 
+/-! ### Multiplication -/
+
+@[simp] lemma coe_one : ((1 : ℝ) : ereal) = 1 := rfl
+
+@[simp, norm_cast] lemma coe_mul (x y : ℝ) : ((x * y : ℝ) : ereal) = (x : ereal) * (y : ereal) :=
+eq.trans (with_bot.coe_eq_coe.mpr with_bot.coe_mul) with_top.coe_mul
+
+@[simp] lemma mul_top (x : ereal) (h : x ≠ 0) : x * ⊤ = ⊤ := with_top.mul_top h
+@[simp] lemma top_mul (x : ereal) (h : x ≠ 0) : ⊤ * x = ⊤ := with_top.top_mul h
+
+@[simp] lemma bot_mul_bot : (⊥ : ereal) * ⊥ = ⊥ := rfl
+@[simp] lemma bot_mul_coe (x : ℝ) (h : x ≠ 0) : (⊥ : ereal) * x = ⊥ :=
+with_top.coe_mul.symm.trans $
+  with_bot.coe_eq_coe.mpr $ with_bot.bot_mul $ function.injective.ne (@option.some.inj _) h
+@[simp] lemma coe_mul_bot (x : ℝ) (h : x ≠ 0) : (x : ereal) * ⊥ = ⊥ :=
+with_top.coe_mul.symm.trans $
+  with_bot.coe_eq_coe.mpr $ with_bot.mul_bot $ function.injective.ne (@option.some.inj _) h
+
+@[simp] lemma to_real_one : to_real 1 = 1 := rfl
+
+lemma to_real_mul : ∀ {x y : ereal}, to_real (x * y) = to_real x * to_real y
+| ⊤ y := by by_cases hy : y = 0; simp [hy]
+| x ⊤ := by by_cases hx : x = 0; simp [hx]
+| (x : ℝ) (y : ℝ) := by simp [← ereal.coe_mul]
+| ⊥ (y : ℝ) := by by_cases hy : y = 0; simp [hy]
+| (x : ℝ) ⊥ := by by_cases hx : x = 0; simp [hx]
+| ⊥ ⊥ := by simp
+
 end ereal
diff --git a/src/order/bounded_lattice.lean b/src/order/bounded_lattice.lean
index 104ec4adabf9c..de12f9127eb7a 100644
--- a/src/order/bounded_lattice.lean
+++ b/src/order/bounded_lattice.lean
@@ -469,6 +469,11 @@ lemma bot_lt_some [has_lt α] (a : α) : (⊥ : with_bot α) < some a :=
 
 lemma bot_lt_coe [has_lt α] (a : α) : (⊥ : with_bot α) < a := bot_lt_some a
 
+instance : can_lift (with_bot α) α :=
+{ coe := coe,
+  cond := λ r, r ≠ ⊥,
+  prf := λ x hx, ⟨option.get $ option.ne_none_iff_is_some.1 hx, option.some_get _⟩ }
+
 instance [preorder α] : preorder (with_bot α) :=
 { le          := λ o₁ o₂ : option α, ∀ a ∈ o₁, ∃ b ∈ o₂, a ≤ b,
   lt          := (<),