refactor(algebra/order): replace typeclasses with constructors (#9725)

This RFC suggests removing some unused classes for the ordered algebra hierarchy, replacing them with constructors

We have `nonneg_add_comm_group extends add_comm_group`, and an instance from this to `ordered_add_comm_group`. The intention is to be able to construct an `ordered_add_comm_group` by specifying its positive cone, rather than directly its order.

There are then `nonneg_ring` and `linear_nonneg_ring`, similarly.

(None of these are actually used later in mathlib at this point.)




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

src/algebra/order/group.lean

@@ -1228,68 +1228,67 @@ instance with_top.linear_ordered_add_comm_group_with_top :
 
 end linear_ordered_add_comm_group
 
-/-- This is not so much a new structure as a construction mechanism
-  for ordered groups, by specifying only the "positive cone" of the group. -/
-class nonneg_add_comm_group (α : Type*) extends add_comm_group α :=
+namespace add_comm_group
+
+/-- A collection of elements in an `add_comm_group` designated as "non-negative".
+This is useful for constructing an `ordered_add_commm_group`
+by choosing a positive cone in an exisiting `add_comm_group`. -/
+@[nolint has_inhabited_instance]
+structure positive_cone (α : Type*) [add_comm_group α] :=
 (nonneg          : α → Prop)
-(pos             : α → Prop := λ a, nonneg a ∧ ¬ nonneg (neg a))
+(pos             : α → Prop := λ a, nonneg a ∧ ¬ nonneg (-a))
 (pos_iff         : ∀ a, pos a ↔ nonneg a ∧ ¬ nonneg (-a) . order_laws_tac)
 (zero_nonneg     : nonneg 0)
 (add_nonneg      : ∀ {a b}, nonneg a → nonneg b → nonneg (a + b))
 (nonneg_antisymm : ∀ {a}, nonneg a → nonneg (-a) → a = 0)
 
-namespace nonneg_add_comm_group
-variable [s : nonneg_add_comm_group α]
-include s
+/-- A positive cone in an `add_comm_group` induces a linear order if
+for every `a`, either `a` or `-a` is non-negative. -/
+@[nolint has_inhabited_instance]
+structure total_positive_cone (α : Type*) [add_comm_group α] extends positive_cone α :=
+(nonneg_decidable : decidable_pred nonneg)
+(nonneg_total : ∀ a : α, nonneg a ∨ nonneg (-a))
+
+/-- Forget that a `total_positive_cone` is total. -/
+add_decl_doc total_positive_cone.to_positive_cone
+
+end add_comm_group
+
+namespace ordered_add_comm_group
+
+open add_comm_group
 
-@[reducible, priority 100] -- see Note [lower instance priority]
-instance to_ordered_add_comm_group : ordered_add_comm_group α :=
-{ le               := λ a b, nonneg (b - a),
-  lt               := λ a b, pos (b - a),
-  lt_iff_le_not_le := λ a b, by simp; rw [pos_iff]; simp,
-  le_refl          := λ a, by simp [zero_nonneg],
+/-- Construct an `ordered_add_comm_group` by
+designating a positive cone in an existing `add_comm_group`. -/
+def mk_of_positive_cone {α : Type*} [add_comm_group α] (C : positive_cone α) :
+  ordered_add_comm_group α :=
+{ le               := λ a b, C.nonneg (b - a),
+  lt               := λ a b, C.pos (b - a),
+  lt_iff_le_not_le := λ a b, by simp; rw [C.pos_iff]; simp,
+  le_refl          := λ a, by simp [C.zero_nonneg],
   le_trans         := λ a b c nab nbc, by simp [-sub_eq_add_neg];
-    rw ← sub_add_sub_cancel; exact add_nonneg nbc nab,
+    rw ← sub_add_sub_cancel; exact C.add_nonneg nbc nab,
   le_antisymm      := λ a b nab nba, eq_of_sub_eq_zero $
-    nonneg_antisymm nba (by rw neg_sub; exact nab),
+    C.nonneg_antisymm nba (by rw neg_sub; exact nab),
   add_le_add_left  := λ a b nab c, by simpa [(≤), preorder.le] using nab,
-  ..s }
-
-theorem nonneg_def {a : α} : nonneg a ↔ 0 ≤ a :=
-show _ ↔ nonneg _, by simp
+  ..‹add_comm_group α› }
 
-theorem pos_def {a : α} : pos a ↔ 0 < a :=
-show _ ↔ pos _, by simp
+end ordered_add_comm_group
 
-theorem not_zero_pos : ¬ pos (0 : α) :=
-mt pos_def.1 (lt_irrefl _)
+namespace linear_ordered_add_comm_group
 
-theorem zero_lt_iff_nonneg_nonneg {a : α} :
-  0 < a ↔ nonneg a ∧ ¬ nonneg (-a) :=
-pos_def.symm.trans (pos_iff _)
+open add_comm_group
 
-theorem nonneg_total_iff :
-  (∀ a : α, nonneg a ∨ nonneg (-a)) ↔
-  (∀ a b : α, a ≤ b ∨ b ≤ a) :=
-⟨λ h a b, by have := h (b - a); rwa [neg_sub] at this,
- λ h a, by rw [nonneg_def, nonneg_def, neg_nonneg]; apply h⟩
+/-- Construct a `linear_ordered_add_comm_group` by
+designating a positive cone in an existing `add_comm_group`
+such that for every `a`, either `a` or `-a` is non-negative. -/
+def mk_of_positive_cone {α : Type*} [add_comm_group α] (C : total_positive_cone α) :
+  linear_ordered_add_comm_group α :=
+{ le_total := λ a b, by { convert C.nonneg_total (b - a), change C.nonneg _ = _, congr, simp, },
+  decidable_le := λ a b, C.nonneg_decidable _,
+  ..ordered_add_comm_group.mk_of_positive_cone C.to_positive_cone }
 
-/--
-A `nonneg_add_comm_group` is a `linear_ordered_add_comm_group`
-if `nonneg` is total and decidable.
--/
-def to_linear_ordered_add_comm_group
-  [decidable_pred (@nonneg α _)]
-  (nonneg_total : ∀ a : α, nonneg a ∨ nonneg (-a))
-  : linear_ordered_add_comm_group α :=
-{ le := (≤),
-  lt := (<),
-  le_total := nonneg_total_iff.1 nonneg_total,
-  decidable_le := by apply_instance,
-  decidable_lt := by apply_instance,
-  ..@nonneg_add_comm_group.to_ordered_add_comm_group _ s }
-
-end nonneg_add_comm_group
+end linear_ordered_add_comm_group
 
 namespace prod
 

src/algebra/order/ring.lean

@@ -1312,101 +1312,69 @@ def function.injective.linear_ordered_comm_ring {β : Type*}
 
 end linear_ordered_comm_ring
 
-/-- Extend `nonneg_add_comm_group` to support ordered rings
-  specified by their nonnegative elements -/
-class nonneg_ring (α : Type*) extends ring α, nonneg_add_comm_group α :=
+namespace ring
+
+/-- A positive cone in a ring consists of a positive cone in underlying `add_comm_group`,
+which contains `1` and such that the positive elements are closed under multiplication. -/
+@[nolint has_inhabited_instance]
+structure positive_cone (α : Type*) [ring α] extends add_comm_group.positive_cone α :=
 (one_nonneg : nonneg 1)
-(mul_nonneg : ∀ {a b}, nonneg a → nonneg b → nonneg (a * b))
-(mul_pos : ∀ {a b}, pos a → pos b → pos (a * b))
+(mul_pos : ∀ (a b), pos a → pos b → pos (a * b))
+
+/-- Forget that a positive cone in a ring respects the multiplicative structure. -/
+add_decl_doc positive_cone.to_positive_cone
 
-/-- Extend `nonneg_add_comm_group` to support linearly ordered rings
-  specified by their nonnegative elements -/
-class linear_nonneg_ring (α : Type*) extends domain α, nonneg_add_comm_group α :=
+/-- A positive cone in a ring induces a linear order if `1` is a positive element. -/
+@[nolint has_inhabited_instance]
+structure total_positive_cone (α : Type*) [ring α]
+  extends positive_cone α, add_comm_group.total_positive_cone α :=
 (one_pos : pos 1)
-(mul_nonneg : ∀ {a b}, nonneg a → nonneg b → nonneg (a * b))
-(nonneg_total : ∀ a, nonneg a ∨ nonneg (-a))
-[dec_nonneg : decidable_pred nonneg]
-
-namespace nonneg_ring
-open nonneg_add_comm_group
-variable [nonneg_ring α]
-
-/-- `to_linear_nonneg_ring` shows that a `nonneg_ring` with a linear order is a `domain`,
-hence a `linear_nonneg_ring`. -/
-def to_linear_nonneg_ring [nontrivial α] [decidable_pred (@nonneg α _)]
-  (nonneg_total : ∀ a : α, nonneg a ∨ nonneg (-a))
-  : linear_nonneg_ring α :=
-{ one_pos := (pos_iff 1).mpr ⟨one_nonneg, λ h, zero_ne_one (nonneg_antisymm one_nonneg h).symm⟩,
-  nonneg_total := nonneg_total,
-  eq_zero_or_eq_zero_of_mul_eq_zero :=
-    suffices ∀ {a} b : α, nonneg a → a * b = 0 → a = 0 ∨ b = 0,
-    from λ a b, (nonneg_total a).elim (this b)
-      (λ na, by simpa using this b na),
-    suffices ∀ {a b : α}, nonneg a → nonneg b → a * b = 0 → a = 0 ∨ b = 0,
-    from λ a b na, (nonneg_total b).elim (this na)
-      (λ nb, by simpa using this na nb),
-    λ a b na nb z, decidable.by_cases
-      (λ nna : nonneg (-a), or.inl (nonneg_antisymm na nna))
-      (λ pa, decidable.by_cases
-        (λ nnb : nonneg (-b), or.inr (nonneg_antisymm nb nnb))
-        (λ pb, absurd z $ ne_of_gt $ pos_def.1 $ mul_pos
-          ((pos_iff _).2 ⟨na, pa⟩)
-          ((pos_iff _).2 ⟨nb, pb⟩))),
-  ..‹nontrivial α›,
-  ..‹nonneg_ring α› }
-
-end nonneg_ring
-
-namespace linear_nonneg_ring
-open nonneg_add_comm_group
-variable [linear_nonneg_ring α]
 
-@[priority 100] -- see Note [lower instance priority]
-instance to_nonneg_ring : nonneg_ring α :=
-{ one_nonneg := ((pos_iff _).mp one_pos).1,
-  mul_pos := λ a b pa pb,
-  let ⟨a1, a2⟩ := (pos_iff a).1 pa,
-      ⟨b1, b2⟩ := (pos_iff b).1 pb in
-  have ab : nonneg (a * b), from mul_nonneg a1 b1,
-  (pos_iff _).2 ⟨ab, λ hn,
-    have a * b = 0, from nonneg_antisymm ab hn,
-    (eq_zero_or_eq_zero_of_mul_eq_zero _ _ this).elim
-      (ne_of_gt (pos_def.1 pa))
-      (ne_of_gt (pos_def.1 pb))⟩,
-  ..‹linear_nonneg_ring α› }
-
-/-- Construct `linear_order` from `linear_nonneg_ring`. This is not an instance
-because we don't use it in `mathlib`. -/
-local attribute [instance]
-def to_linear_order [decidable_pred (nonneg : α → Prop)] : linear_order α :=
-{ le_total := nonneg_total_iff.1 nonneg_total,
-  decidable_le := by apply_instance,
-  decidable_lt := by apply_instance,
-  ..‹linear_nonneg_ring α›, ..(infer_instance : ordered_add_comm_group α) }
-
-/-- Construct `linear_ordered_ring` from `linear_nonneg_ring`.
-This is not an instance because we don't use it in `mathlib`. -/
-local attribute [instance]
-def to_linear_ordered_ring [decidable_pred (nonneg : α → Prop)] : linear_ordered_ring α :=
-{ mul_pos := by simp [pos_def.symm]; exact @nonneg_ring.mul_pos _ _,
-  zero_le_one := le_of_lt $ lt_of_not_ge $ λ (h : nonneg (0 - 1)), begin
-    rw [zero_sub] at h,
-    have := mul_nonneg h h, simp at this,
-    exact zero_ne_one (nonneg_antisymm this h).symm
+/-- Forget that a `total_positive_cone` in a ring is total. -/
+add_decl_doc total_positive_cone.to_positive_cone
+
+/-- Forget that a `total_positive_cone` in a ring respects the multiplicative structure. -/
+add_decl_doc total_positive_cone.to_total_positive_cone
+
+end ring
+
+namespace ordered_ring
+
+open ring
+
+/-- Construct an `ordered_ring` by
+designating a positive cone in an existing `ring`. -/
+def mk_of_positive_cone {α : Type*} [ring α] (C : positive_cone α) :
+  ordered_ring α :=
+{ zero_le_one := by { change C.nonneg (1 - 0), convert C.one_nonneg, simp, },
+  mul_pos := λ x y xp yp, begin
+    change C.pos (x*y - 0),
+    convert C.mul_pos x y (by { convert xp, simp, }) (by { convert yp, simp, }),
+    simp,
   end,
-  ..‹linear_nonneg_ring α›, ..(infer_instance : ordered_add_comm_group α),
-  ..(infer_instance : linear_order α) }
-
-/-- Convert a `linear_nonneg_ring` with a commutative multiplication and
-decidable non-negativity into a `linear_ordered_comm_ring` -/
-def to_linear_ordered_comm_ring
-  [decidable_pred (@nonneg α _)]
-  [comm : @is_commutative α (*)]
-  : linear_ordered_comm_ring α :=
-{ mul_comm := is_commutative.comm,
-  ..@linear_nonneg_ring.to_linear_ordered_ring _ _ _ }
-
-end linear_nonneg_ring
+  ..‹ring α›,
+  ..ordered_add_comm_group.mk_of_positive_cone C.to_positive_cone }
+
+end ordered_ring
+
+namespace linear_ordered_ring
+
+open ring
+
+/-- Construct a `linear_ordered_ring` by
+designating a positive cone in an existing `ring`. -/
+def mk_of_positive_cone {α : Type*} [ring α] (C : total_positive_cone α) :
+  linear_ordered_ring α :=
+{ exists_pair_ne := ⟨0, 1, begin
+    intro h,
+    have one_pos := C.one_pos,
+    rw [←h, C.pos_iff] at one_pos,
+    simpa using one_pos,
+  end⟩,
+  ..ordered_ring.mk_of_positive_cone C.to_positive_cone,
+  ..linear_ordered_add_comm_group.mk_of_positive_cone C.to_total_positive_cone, }
+
+end linear_ordered_ring
 
 /-- A canonically ordered commutative semiring is an ordered, commutative semiring
 in which `a ≤ b` iff there exists `c` with `b = a + c`. This is satisfied by the