From 1c2d71f1833b5d5d4b2fe26e2d805047508e23b6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Sat, 27 Aug 2022 21:53:53 +0000
Subject: [PATCH] feat(algebra/order/field): Canonically linear ordered
 semifields (#15677)

Define `canonically_linear_ordered_semifield`. The target is `nnreal` and the future `nnrat`.
---
 src/algebra/order/field.lean      |  8 ++++
 src/algebra/order/field_defs.lean | 15 +++++-
 src/algebra/order/nonneg.lean     | 78 ++++++++++++++++++-------------
 3 files changed, 67 insertions(+), 34 deletions(-)

diff --git a/src/algebra/order/field.lean b/src/algebra/order/field.lean
index 927c23a3f67fa..8840c4a17cd63 100644
--- a/src/algebra/order/field.lean
+++ b/src/algebra/order/field.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn
 -/
 import algebra.order.field_defs
+import algebra.order.with_zero
 
 /-!
 # Linear ordered (semi)fields
@@ -852,3 +853,10 @@ theorem nat.cast_le_pow_div_sub (H : 1 < a) (n : ℕ) : (n : α) ≤ a ^ n / (a
   (sub_le_self _ zero_le_one)
 
 end
+
+section canonically_linear_ordered_semifield
+variables [canonically_linear_ordered_semifield α] [has_sub α] [has_ordered_sub α]
+
+lemma tsub_div (a b c : α) : (a - b) / c = a / c - b / c := by simp_rw [div_eq_mul_inv, tsub_mul]
+
+end canonically_linear_ordered_semifield
diff --git a/src/algebra/order/field_defs.lean b/src/algebra/order/field_defs.lean
index a345e440e108c..c734f15d942f3 100644
--- a/src/algebra/order/field_defs.lean
+++ b/src/algebra/order/field_defs.lean
@@ -32,6 +32,8 @@ The lemmata are instead located there.
 
 set_option old_structure_cmd true
 
+variables {α : Type*}
+
 /-- A linear ordered semifield is a field with a linear order respecting the operations. -/
 @[protect_proj] class linear_ordered_semifield (α : Type*)
   extends linear_ordered_semiring α, semifield α
@@ -39,7 +41,18 @@ set_option old_structure_cmd true
 /-- A linear ordered field is a field with a linear order respecting the operations. -/
 @[protect_proj] class linear_ordered_field (α : Type*) extends linear_ordered_comm_ring α, field α
 
+/-- A canonically linear ordered field is a linear ordered field in which `a ≤ b` iff there exists
+`c` with `b = a + c`. -/
+@[protect_proj] class canonically_linear_ordered_semifield (α : Type*)
+  extends canonically_ordered_comm_semiring α, linear_ordered_semifield α
+
 @[priority 100] -- See note [lower instance priority]
-instance linear_ordered_field.to_linear_ordered_semifield {α} [linear_ordered_field α] :
+instance linear_ordered_field.to_linear_ordered_semifield [linear_ordered_field α] :
   linear_ordered_semifield α :=
 { ..linear_ordered_ring.to_linear_ordered_semiring, ..‹linear_ordered_field α› }
+
+@[priority 100] -- See note [lower instance priority]
+instance canonically_linear_ordered_semifield.to_linear_ordered_comm_group_with_zero
+  [canonically_linear_ordered_semifield α] : linear_ordered_comm_group_with_zero α :=
+{ mul_le_mul_left := λ a b h c, mul_le_mul_of_nonneg_left h $ zero_le _,
+  ..‹canonically_linear_ordered_semifield α› }
diff --git a/src/algebra/order/nonneg.lean b/src/algebra/order/nonneg.lean
index aeb62e116e86c..1fe76aca8d83f 100644
--- a/src/algebra/order/nonneg.lean
+++ b/src/algebra/order/nonneg.lean
@@ -4,9 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 import algebra.order.archimedean
-import algebra.order.floor
-import algebra.order.sub
-import algebra.order.with_zero
 import order.lattice_intervals
 import order.complete_lattice_intervals
 
@@ -227,36 +224,6 @@ def coe_ring_hom [ordered_semiring α] : {x : α // 0 ≤ x} →+* α :=
 protected lemma coe_nat_cast [ordered_semiring α] (n : ℕ) : ((↑n : {x : α // 0 ≤ x}) : α) = n :=
 map_nat_cast (coe_ring_hom : {x : α // 0 ≤ x} →+* α) n
 
-instance has_inv [linear_ordered_field α] : has_inv {x : α // 0 ≤ x} :=
-{ inv := λ x, ⟨x⁻¹, inv_nonneg.mpr x.2⟩ }
-
-@[simp, norm_cast]
-protected lemma coe_inv [linear_ordered_field α] (a : {x : α // 0 ≤ x}) :
-  ((a⁻¹ : {x : α // 0 ≤ x}) : α) = a⁻¹ := rfl
-
-@[simp] lemma inv_mk [linear_ordered_field α] {x : α} (hx : 0 ≤ x) :
-  (⟨x, hx⟩ : {x : α // 0 ≤ x})⁻¹ = ⟨x⁻¹, inv_nonneg.mpr hx⟩ :=
-rfl
-
-instance linear_ordered_comm_group_with_zero [linear_ordered_field α] :
-  linear_ordered_comm_group_with_zero {x : α // 0 ≤ x} :=
-{ inv_zero := by { ext, exact inv_zero },
-  mul_inv_cancel := by { intros a ha, ext, refine mul_inv_cancel (mt (λ h, _) ha), ext, exact h },
-  ..nonneg.nontrivial,
-  ..nonneg.has_inv,
-  ..nonneg.linear_ordered_comm_monoid_with_zero }
-
-instance has_div [linear_ordered_field α] : has_div {x : α // 0 ≤ x} :=
-{ div := λ x y, ⟨x / y, div_nonneg x.2 y.2⟩ }
-
-@[simp, norm_cast]
-protected lemma coe_div [linear_ordered_field α] (a b : {x : α // 0 ≤ x}) :
-  ((a / b : {x : α // 0 ≤ x}) : α) = a / b := rfl
-
-@[simp] lemma mk_div_mk [linear_ordered_field α] {x y : α} (hx : 0 ≤ x) (hy : 0 ≤ y) :
-  (⟨x, hx⟩ : {x : α // 0 ≤ x}) / ⟨y, hy⟩ = ⟨x / y, div_nonneg hx hy⟩ :=
-rfl
-
 instance canonically_ordered_add_monoid [ordered_ring α] :
   canonically_ordered_add_monoid {x : α // 0 ≤ x} :=
 { le_self_add := λ a b, le_add_of_nonneg_right b.2,
@@ -275,6 +242,51 @@ instance canonically_linear_ordered_add_monoid [linear_ordered_ring α] :
   canonically_linear_ordered_add_monoid {x : α // 0 ≤ x} :=
 { ..subtype.linear_order _, ..nonneg.canonically_ordered_add_monoid }
 
+section linear_ordered_semifield
+variables [linear_ordered_semifield α] {x y : α}
+
+instance has_inv : has_inv {x : α // 0 ≤ x} := ⟨λ x, ⟨x⁻¹, inv_nonneg.mpr x.2⟩⟩
+
+@[simp, norm_cast]
+protected lemma coe_inv (a : {x : α // 0 ≤ x}) : ((a⁻¹ : {x : α // 0 ≤ x}) : α) = a⁻¹ := rfl
+
+@[simp] lemma inv_mk (hx : 0 ≤ x) : (⟨x, hx⟩ : {x : α // 0 ≤ x})⁻¹ = ⟨x⁻¹, inv_nonneg.mpr hx⟩ := rfl
+
+instance has_div : has_div {x : α // 0 ≤ x} := ⟨λ x y, ⟨x / y, div_nonneg x.2 y.2⟩⟩
+
+@[simp, norm_cast] protected lemma coe_div (a b : {x : α // 0 ≤ x}) :
+  ((a / b : {x : α // 0 ≤ x}) : α) = a / b := rfl
+
+@[simp] lemma mk_div_mk (hx : 0 ≤ x) (hy : 0 ≤ y) :
+  (⟨x, hx⟩ : {x : α // 0 ≤ x}) / ⟨y, hy⟩ = ⟨x / y, div_nonneg hx hy⟩ := rfl
+
+instance has_zpow : has_pow {x : α // 0 ≤ x} ℤ := ⟨λ a n, ⟨a ^ n, zpow_nonneg a.2 _⟩⟩
+
+@[simp, norm_cast] protected lemma coe_zpow (a : {x : α // 0 ≤ x}) (n : ℤ) :
+  ((a ^ n : {x : α // 0 ≤ x}) : α) = a ^ n := rfl
+
+@[simp] lemma mk_zpow (hx : 0 ≤ x) (n : ℤ) :
+  (⟨x, hx⟩ : {x : α // 0 ≤ x}) ^ n = ⟨x ^ n, zpow_nonneg hx n⟩ := rfl
+
+instance linear_ordered_semifield : linear_ordered_semifield {x : α // 0 ≤ x} :=
+subtype.coe_injective.linear_ordered_semifield _ nonneg.coe_zero nonneg.coe_one nonneg.coe_add
+    nonneg.coe_mul nonneg.coe_inv nonneg.coe_div (λ _ _, rfl) nonneg.coe_pow nonneg.coe_zpow
+    nonneg.coe_nat_cast (λ _ _, rfl) (λ _ _, rfl)
+
+end linear_ordered_semifield
+
+instance linear_ordered_comm_group_with_zero [linear_ordered_field α] :
+  linear_ordered_comm_group_with_zero {x : α // 0 ≤ x} :=
+{ inv_zero := by { ext, exact inv_zero },
+  mul_inv_cancel := by { intros a ha, ext, refine mul_inv_cancel (mt (λ h, _) ha), ext, exact h },
+  ..nonneg.nontrivial,
+  ..nonneg.has_inv,
+  ..nonneg.linear_ordered_comm_monoid_with_zero }
+
+instance canonically_linear_ordered_semifield [linear_ordered_field α] :
+  canonically_linear_ordered_semifield {x : α // 0 ≤ x} :=
+{ ..nonneg.linear_ordered_semifield, ..nonneg.canonically_ordered_comm_semiring }
+
 instance floor_semiring [ordered_semiring α] [floor_semiring α] : floor_semiring {r : α // 0 ≤ r} :=
 { floor := λ a, ⌊(a : α)⌋₊,
   ceil := λ a, ⌈(a : α)⌉₊,