From 98d07d314aae5c8c745ae7582ac7863eb8eb23a6 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 18 Oct 2021 23:50:41 +0000 Subject: [PATCH] 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 --- src/algebra/order/group.lean | 93 +++++++++++----------- src/algebra/order/ring.lean | 148 ++++++++++++++--------------------- 2 files changed, 104 insertions(+), 137 deletions(-) diff --git a/src/algebra/order/group.lean b/src/algebra/order/group.lean index fdadeb97f224d..2bccb2931576c 100644 --- a/src/algebra/order/group.lean +++ b/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 diff --git a/src/algebra/order/ring.lean b/src/algebra/order/ring.lean index 9f46736d295c6..140acae0c1458 100644 --- a/src/algebra/order/ring.lean +++ b/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