feat: LinearOrder α extends Ord α (#2858)

This PR makes `LinearOrder` lawfully extend `Ord`.

Since `LinearOrder` has decidable order relations, we take `compare` to be `compareOfLessAndEq` by default for a linear order.

Since typeclass synthesis is preferred by structure instances to optparams, this does not create non-defeq diamonds for types which already have a different implementation of `Ord`.

We also add a field `compare_eq_compareOfLessAndEq` which encodes the lawful quality by demanding equality to the canonical comparison.

Motivation: `Array` functions like `min` largely use `Ord`, so this lets us seamlessly use these array functions when we only have a linear order.

See [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Ord.20.C9.91.20from.20LinearOrder.20.C9.91.3F).



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

Mathlib/Data/Fin/Basic.lean

@@ -300,9 +300,9 @@ theorem val_fin_le {n : ℕ} {a b : Fin n} : (a : ℕ) ≤ (b : ℕ) ↔ a ≤ b
 #align fin.coe_fin_le Fin.val_fin_le
 
 instance {n : ℕ} : LinearOrder (Fin n) :=
-  @LinearOrder.lift (Fin n) _ _ ⟨fun x y => ⟨max x y, max_rec' (· < n) x.2 y.2⟩⟩
-    ⟨fun x y => ⟨min x y, min_rec' (· < n) x.2 y.2⟩⟩ Fin.val Fin.val_injective (fun _ _ => rfl)
-    fun _ _ => rfl
+  @LinearOrder.liftWithOrd (Fin n) _ _ ⟨fun x y => ⟨max x y, max_rec' (· < n) x.2 y.2⟩⟩
+    ⟨fun x y => ⟨min x y, min_rec' (· < n) x.2 y.2⟩⟩ _ Fin.val Fin.val_injective (fun _ _ => rfl)
+    (fun _ _ => rfl) (fun _ _ => rfl)
 
 @[simp]
 theorem mk_le_mk {x y : Nat} {hx} {hy} : (⟨x, hx⟩ : Fin n) ≤ ⟨y, hy⟩ ↔ x ≤ y :=

Mathlib/Init/Algebra/Order.lean

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Deniz Aydin
 -/
 import Mathlib.Init.Logic
+import Mathlib.Init.Data.Ordering.Basic
 import Mathlib.Tactic.Relation.Rfl
+import Mathlib.Tactic.SplitIfs
 
 /-!
 # Orders
@@ -214,9 +216,23 @@ if a ≤ b then b else a
 def minDefault {α : Type u} [LE α] [DecidableRel ((· ≤ ·) : α → α → Prop)] (a b : α) :=
 if a ≤ b then a else b
 
+/-- This attempts to prove that a given instance of `compare` is equal to `compareOfLessAndEq` by
+introducing the arguments and trying the following approaches in order:
+
+1. seeing if `rfl` works
+2. seeing if the `compare` at hand is nonetheless essentially `compareOfLessAndEq`, but, because of
+implicit arguments, requires us to unfold the defs and split the `if`s in the definition of
+`compareOfLessAndEq`
+3. seeing if we can split by cases on the arguments, then see if the defs work themselves out
+  (useful when `compare` is defined via a `match` statement, as it is for `Bool`) -/
+macro "compareOfLessAndEq_rfl" : tactic =>
+  `(tactic| (intros a b; first | rfl |
+    (simp only [compare, compareOfLessAndEq]; split_ifs <;> rfl) |
+    (induction a <;> induction b <;> simp only [])))
+
 /-- A linear order is reflexive, transitive, antisymmetric and total relation `≤`.
 We assume that every linear ordered type has decidable `(≤)`, `(<)`, and `(=)`. -/
-class LinearOrder (α : Type u) extends PartialOrder α, Min α, Max α :=
+class LinearOrder (α : Type u) extends PartialOrder α, Min α, Max α, Ord α :=
   /-- A linear order is total. -/
   le_total (a b : α) : a ≤ b ∨ b ≤ a
   /-- In a linearly ordered type, we assume the order relations are all decidable. -/
@@ -232,6 +248,10 @@ class LinearOrder (α : Type u) extends PartialOrder α, Min α, Max α :=
   min_def : ∀ a b, min a b = if a ≤ b then a else b := by intros; rfl
   /-- The minimum function is equivalent to the one you get from `maxOfLe`. -/
   max_def : ∀ a b, max a b = if a ≤ b then b else a := by intros; rfl
+  compare a b := compareOfLessAndEq a b
+  /-- Comparison via `compare` is equal to the canonical comparison given decidable `<` and `=`. -/
+  compare_eq_compareOfLessAndEq : ∀ a b, compare a b = compareOfLessAndEq a b := by
+    compareOfLessAndEq_rfl
 
 variable [LinearOrder α]
 
@@ -337,4 +357,54 @@ theorem le_imp_le_of_lt_imp_lt {β} [Preorder α] [LinearOrder β]
   {a b : α} {c d : β} (H : d < c → b < a) (h : a ≤ b) : c ≤ d :=
 le_of_not_lt $ λ h' => not_le_of_gt (H h') h
 
+section Ord
+
+theorem compare_lt_iff_lt {a b : α} : (compare a b = .lt) ↔ a < b := by
+  rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
+  split_ifs <;> simp only [*, lt_irrefl]
+
+theorem compare_gt_iff_gt {a b : α} : (compare a b = .gt) ↔ a > b := by
+  rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
+  split_ifs <;> simp only [*, lt_irrefl, not_lt_of_gt]
+  case _ h₁ h₂ =>
+    have h : b < a := lt_trichotomy a b |>.resolve_left h₁ |>.resolve_left h₂
+    exact true_iff_iff.2 h
+
+theorem compare_eq_iff_eq {a b : α} : (compare a b = .eq) ↔ a = b := by
+  rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
+  split_ifs <;> simp only []
+  case _ h   => exact false_iff_iff.2 <| ne_iff_lt_or_gt.2 <| .inl h
+  case _ _ h => exact true_iff_iff.2 h
+  case _ _ h => exact false_iff_iff.2 h
+
+theorem compare_le_iff_le {a b : α} : (compare a b ≠ .gt) ↔ a ≤ b := by
+  cases h : compare a b <;> simp only []
+  · exact true_iff_iff.2 <| le_of_lt <| compare_lt_iff_lt.1 h
+  · exact true_iff_iff.2 <| le_of_eq <| compare_eq_iff_eq.1 h
+  · exact false_iff_iff.2 <| not_le_of_gt <| compare_gt_iff_gt.1 h
+
+theorem compare_ge_iff_ge {a b : α} : (compare a b ≠ .lt) ↔ a ≥ b := by
+  cases h : compare a b <;> simp only []
+  · exact false_iff_iff.2 <| (lt_iff_not_ge a b).1 <| compare_lt_iff_lt.1 h
+  · exact true_iff_iff.2 <| le_of_eq <| (·.symm) <| compare_eq_iff_eq.1 h
+  · exact true_iff_iff.2 <| le_of_lt <| compare_gt_iff_gt.1 h
+
+theorem compare_iff (a b : α) {o : Ordering} : compare a b = o ↔ o.toRel a b := by
+  cases o <;> simp only [Ordering.toRel]
+  · exact compare_lt_iff_lt
+  · exact compare_eq_iff_eq
+  · exact compare_gt_iff_gt
+
+instance : Std.TransCmp (compare (α := α)) where
+  symm a b := by
+    cases h : compare a b <;>
+    simp only [Ordering.swap] <;> symm
+    · exact compare_gt_iff_gt.2 <| compare_lt_iff_lt.1 h
+    · exact compare_eq_iff_eq.2 <| compare_eq_iff_eq.1 h |>.symm
+    · exact compare_lt_iff_lt.2 <| compare_gt_iff_gt.1 h
+  le_trans := fun h₁ h₂ ↦
+    compare_le_iff_le.2 <| le_trans (compare_le_iff_le.1 h₁) (compare_le_iff_le.1 h₂)
+
+end Ord
+
 end LinearOrder

Mathlib/Init/Data/Ordering/Basic.lean

@@ -19,6 +19,12 @@ def orElse : Ordering → Ordering → Ordering
   | eq, o => o
   | gt, _ => gt
 
+/-- The relation corresponding to each `Ordering` constructor (e.g. `.lt.toProp a b` is `a < b`). -/
+def toRel [LT α] : Ordering → α → α → Prop
+| .lt => (· < ·)
+| .eq => Eq
+| .gt => (· > ·)
+
 end Ordering
 
 /--

Mathlib/Order/Basic.lean

@@ -15,6 +15,7 @@ import Mathlib.Tactic.Convert
 import Mathlib.Tactic.Inhabit
 import Mathlib.Tactic.SimpRw
 import Mathlib.Tactic.Spread
+import Mathlib.Tactic.SplitIfs
 
 /-!
 # Basic definitions about `≤` and `<`
@@ -616,12 +617,18 @@ theorem PartialOrder.toPreorder_injective {α : Type _} :
 theorem LinearOrder.toPartialOrder_injective {α : Type _} :
     Function.Injective (@LinearOrder.toPartialOrder α) :=
   fun A B h ↦ match A, B with
-  | { le := A_le, lt := A_lt, decidable_le := A_decidable_le,
-      min := A_min, max := A_max, min_def := A_min_def, max_def := A_max_def, .. },
-    { le := B_le, lt := B_lt, decidable_le := B_decidable_le,
-      min := B_min, max := B_max, min_def := B_min_def, max_def := B_max_def, .. } => by
+  | { le := A_le, lt := A_lt,
+      decidable_le := A_decidable_le, decidable_eq := A_decidable_eq, decidable_lt := A_decidable_lt
+      min := A_min, max := A_max, min_def := A_min_def, max_def := A_max_def,
+      compare := A_compare, compare_eq_compareOfLessAndEq := A_compare_canonical,  .. },
+    { le := B_le, lt := B_lt,
+      decidable_le := B_decidable_le, decidable_eq := B_decidable_eq, decidable_lt := B_decidable_lt
+      min := B_min, max := B_max, min_def := B_min_def, max_def := B_max_def,
+      compare := B_compare, compare_eq_compareOfLessAndEq := B_compare_canonical, .. } => by
     cases h
     obtain rfl : A_decidable_le = B_decidable_le := Subsingleton.elim _ _
+    obtain rfl : A_decidable_eq = B_decidable_eq := Subsingleton.elim _ _
+    obtain rfl : A_decidable_lt = B_decidable_lt := Subsingleton.elim _ _
     have : A_min = B_min := by
       funext a b
       exact (A_min_def _ _).trans (B_min_def _ _).symm
@@ -630,7 +637,10 @@ theorem LinearOrder.toPartialOrder_injective {α : Type _} :
       funext a b
       exact (A_max_def _ _).trans (B_max_def _ _).symm
     cases this
-    congr <;> exact Subsingleton.elim _ _
+    have : A_compare = B_compare := by
+      funext a b
+      exact (A_compare_canonical _ _).trans (B_compare_canonical _ _).symm
+    congr
 #align linear_order.to_partial_order_injective LinearOrder.toPartialOrder_injective
 
 theorem Preorder.ext {α} {A B : Preorder α}
@@ -985,19 +995,37 @@ def PartialOrder.lift {α β} [PartialOrder β] (f : α → β) (inj : Injective
   { Preorder.lift f with le_antisymm := fun _ _ h₁ h₂ ↦ inj (h₁.antisymm h₂) }
 #align partial_order.lift PartialOrder.lift
 
+theorem compare_of_injective_eq_compareOfLessAndEq (a b : α) [LinearOrder β]
+    [DecidableEq α] (f : α → β) (inj : Injective f)
+    [Decidable (LT.lt (self := PartialOrder.lift f inj |>.toLT) a b)] :
+    compare (f a) (f b) =
+      @compareOfLessAndEq _ a b (PartialOrder.lift f inj |>.toLT) _ _ := by
+  have h := LinearOrder.compare_eq_compareOfLessAndEq (f a) (f b)
+  simp only [h, compareOfLessAndEq]
+  split_ifs <;> try (first | rfl | contradiction)
+  · have : ¬ f a = f b := by rename_i h; exact inj.ne h
+    contradiction
+  · have : f a = f b := by rename_i h; exact congrArg f h
+    contradiction
+
 /-- Transfer a `LinearOrder` on `β` to a `LinearOrder` on `α` using an injective
 function `f : α → β`. This version takes `[Sup α]` and `[Inf α]` as arguments, then uses
 them for `max` and `min` fields. See `LinearOrder.lift'` for a version that autogenerates `min` and
-`max` fields. See note [reducible non-instances]. -/
+`max` fields, and `LinearOrder.liftWithOrd` for one that does not auto-generate `compare`
+fields. See note [reducible non-instances]. -/
 @[reducible]
 def LinearOrder.lift {α β} [LinearOrder β] [Sup α] [Inf α] (f : α → β) (inj : Injective f)
     (hsup : ∀ x y, f (x ⊔ y) = max (f x) (f y)) (hinf : ∀ x y, f (x ⊓ y) = min (f x) (f y)) :
     LinearOrder α :=
-  { PartialOrder.lift f inj with
+  letI instOrdα : Ord α := ⟨fun a b ↦ compare (f a) (f b)⟩
+  letI decidable_le := fun x y ↦ (inferInstance : Decidable (f x ≤ f y))
+  letI decidable_lt := fun x y ↦ (inferInstance : Decidable (f x < f y))
+  letI decidable_eq := fun x y ↦ decidable_of_iff (f x = f y) inj.eq_iff
+  { PartialOrder.lift f inj, instOrdα with
     le_total := fun x y ↦ le_total (f x) (f y)
-    decidable_le := fun x y ↦ (inferInstance : Decidable (f x ≤ f y))
-    decidable_lt := fun x y ↦ (inferInstance : Decidable (f x < f y))
-    decidable_eq := fun x y ↦ decidable_of_iff (f x = f y) inj.eq_iff
+    decidable_le := decidable_le
+    decidable_lt := decidable_lt
+    decidable_eq := decidable_eq
     min := (· ⊓ ·)
     max := (· ⊔ ·)
     min_def := by
@@ -1009,12 +1037,14 @@ def LinearOrder.lift {α β} [LinearOrder β] [Sup α] [Inf α] (f : α → β)
       intros x y
       apply inj
       rw [apply_ite f]
-      exact (hsup _ _).trans (max_def _ _) }
-#align linear_order.lift LinearOrder.lift
+      exact (hsup _ _).trans (max_def _ _)
+    compare_eq_compareOfLessAndEq := fun a b ↦
+      compare_of_injective_eq_compareOfLessAndEq a b f inj }
 
 /-- Transfer a `LinearOrder` on `β` to a `LinearOrder` on `α` using an injective
 function `f : α → β`. This version autogenerates `min` and `max` fields. See `LinearOrder.lift`
-for a version that takes `[Sup α]` and `[Inf α]`, then uses them as `max` and `min`.
+for a version that takes `[Sup α]` and `[Inf α]`, then uses them as `max` and `min`. See
+`LinearOrder.liftWithOrd'` for a version which does not auto-generate `compare` fields.
 See note [reducible non-instances]. -/
 @[reducible]
 def LinearOrder.lift' {α β} [LinearOrder β] (f : α → β) (inj : Injective f) : LinearOrder α :=
@@ -1024,6 +1054,55 @@ def LinearOrder.lift' {α β} [LinearOrder β] (f : α → β) (inj : Injective
     (apply_ite f _ _ _).trans (min_def _ _).symm
 #align linear_order.lift' LinearOrder.lift'
 
+/-- Transfer a `LinearOrder` on `β` to a `LinearOrder` on `α` using an injective
+function `f : α → β`. This version takes `[Sup α]` and `[Inf α]` as arguments, then uses
+them for `max` and `min` fields. It also takes `[Ord α]` as an argument and uses them for `compare`
+fields. See `LinearOrder.lift` for a version that autogenerates `compare` fields, and
+`LinearOrder.liftWithOrd'` for one that auto-generates `min` and `max` fields.
+fields. See note [reducible non-instances]. -/
+@[reducible]
+def LinearOrder.liftWithOrd {α β} [LinearOrder β] [Sup α] [Inf α] [Ord α] (f : α → β)
+    (inj : Injective f) (hsup : ∀ x y, f (x ⊔ y) = max (f x) (f y))
+    (hinf : ∀ x y, f (x ⊓ y) = min (f x) (f y))
+    (compare_f : ∀ a b : α, compare a b = compare (f a) (f b)) : LinearOrder α :=
+  letI decidable_le := fun x y ↦ (inferInstance : Decidable (f x ≤ f y))
+  letI decidable_lt := fun x y ↦ (inferInstance : Decidable (f x < f y))
+  letI decidable_eq := fun x y ↦ decidable_of_iff (f x = f y) inj.eq_iff
+  { PartialOrder.lift f inj with
+    le_total := fun x y ↦ le_total (f x) (f y)
+    decidable_le := decidable_le
+    decidable_lt := decidable_lt
+    decidable_eq := decidable_eq
+    min := (· ⊓ ·)
+    max := (· ⊔ ·)
+    min_def := by
+      intros x y
+      apply inj
+      rw [apply_ite f]
+      exact (hinf _ _).trans (min_def _ _)
+    max_def := by
+      intros x y
+      apply inj
+      rw [apply_ite f]
+      exact (hsup _ _).trans (max_def _ _)
+    compare_eq_compareOfLessAndEq := fun a b ↦
+      (compare_f a b).trans <| compare_of_injective_eq_compareOfLessAndEq a b f inj }
+
+/-- Transfer a `LinearOrder` on `β` to a `LinearOrder` on `α` using an injective
+function `f : α → β`. This version auto-generates `min` and `max` fields. It also takes `[Ord α]`
+as an argument and uses them for `compare` fields. See `LinearOrder.lift` for a version that
+autogenerates `compare` fields, and `LinearOrder.liftWithOrd` for one that doesn't auto-generate
+`min` and `max` fields. fields. See note [reducible non-instances]. -/
+@[reducible]
+def LinearOrder.liftWithOrd' {α β} [LinearOrder β] [Ord α] (f : α → β)
+    (inj : Injective f)
+    (compare_f : ∀ a b : α, compare a b = compare (f a) (f b)) : LinearOrder α :=
+  @LinearOrder.liftWithOrd α β _ ⟨fun x y ↦ if f x ≤ f y then y else x⟩
+    ⟨fun x y ↦ if f x ≤ f y then x else y⟩ _ f inj
+    (fun _ _ ↦ (apply_ite f _ _ _).trans (max_def _ _).symm)
+    (fun _ _ ↦ (apply_ite f _ _ _).trans (min_def _ _).symm)
+    compare_f
+
 /-! ### Subtype of an order -/
 
 

Mathlib/Tactic/Ring/Basic.lean

@@ -77,10 +77,6 @@ This feature wasn't needed yet, so it's not implemented yet.
 ring, semiring, exponent, power
 -/
 
--- TODO: move somewhere else
-instance : Ord ℚ where
-  compare x y := compareOfLessAndEq x y
-
 namespace Mathlib.Tactic
 namespace Ring
 open Mathlib.Meta Qq NormNum Lean.Meta AtomM