feat: add missing order instances and lemmas (#12419)

This PR adds `LawfulOrderOrd` instances for `Nat`, `Int`, and all
fixed-width integer types (`Int8`, `Int16`, `Int32`, `Int64`, `ISize`,
`UInt8`, `UInt16`, `UInt32`, `UInt64`, `USize`). These instances
establish that the `Ord` instances for these types are compatible with
their `LE` instances. Additionally, this PR adds a few missing lemmas
and `grind` patterns.

src/Init/Data/Int/Compare.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Ord.Basic
+public import Init.Data.Order.ClassesExtra
 import all Init.Data.Ord.Basic
 import Init.Omega
 
@@ -73,4 +74,8 @@ protected theorem isGE_compare {a b : Int} :
   rw [← Int.compare_swap, Ordering.isGE_swap]
   exact Int.isLE_compare
 
+public instance : Std.LawfulOrderOrd Int where
+  isLE_compare _ _ := Int.isLE_compare
+  isGE_compare _ _ := Int.isGE_compare
+
 end Int

src/Init/Data/Nat/Compare.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 module
 
 prelude
-public import Init.Data.Ord.Basic
+public import Init.Data.Order.ClassesExtra
 import all Init.Data.Ord.Basic
 
 public section
@@ -70,4 +70,8 @@ protected theorem isGE_compare {a b : Nat} :
   rw [← Nat.compare_swap, Ordering.isGE_swap]
   exact Nat.isLE_compare
 
+public instance : Std.LawfulOrderOrd Nat where
+  isLE_compare _ _ := Nat.isLE_compare
+  isGE_compare _ _ := Nat.isGE_compare
+
 end Nat

src/Init/Data/Ord/Basic.lean

@@ -437,6 +437,14 @@ theorem isLE_compareOfLessAndEq
     · exact Or.inr <| antisymm hle hge
     · exact Or.inl <| not_le.mp hge
 
+theorem isGE_compareOfLessAndEq
+    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α]
+    (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
+    (not_le : ∀ {x y : α}, ¬ x ≤ y ↔ y < x) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) {x y : α} :
+    (compareOfLessAndEq x y).isGE ↔ y ≤ x := by
+  rw [compareOfLessAndEq_eq_swap antisymm total not_le, Ordering.isGE_swap,
+    isLE_compareOfLessAndEq antisymm not_le total]
+
 end Lemmas
 
 /--

src/Init/Data/Ord/SInt.lean

@@ -7,8 +7,10 @@ module
 
 prelude
 public import Init.Data.Order.Ord
+public import Init.Data.Order.ClassesExtra
 public import Init.Data.SInt.Basic
 import Init.Data.SInt.Lemmas
+import Init.Data.Order.Lemmas
 
 public section
 
@@ -34,6 +36,10 @@ instance : TransOrd Int8 :=
 instance : LawfulEqOrd Int8 where
   eq_of_compare h := compareOfLessAndEq_eq_eq Int8.le_refl Int8.not_le |>.mp h
 
+instance : LawfulOrderOrd Int8 where
+  isLE_compare _ _ := isLE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+  isGE_compare _ _ := isGE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+
 end Int8
 
 namespace Int16
@@ -48,6 +54,10 @@ instance : TransOrd Int16 :=
 instance : LawfulEqOrd Int16 where
   eq_of_compare h := compareOfLessAndEq_eq_eq Int16.le_refl Int16.not_le |>.mp h
 
+instance : LawfulOrderOrd Int16 where
+  isLE_compare _ _ := isLE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+  isGE_compare _ _ := isGE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+
 end Int16
 
 namespace Int32
@@ -62,6 +72,10 @@ instance : TransOrd Int32 :=
 instance : LawfulEqOrd Int32 where
   eq_of_compare h := compareOfLessAndEq_eq_eq Int32.le_refl Int32.not_le |>.mp h
 
+instance : LawfulOrderOrd Int32 where
+  isLE_compare _ _ := isLE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+  isGE_compare _ _ := isGE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+
 end Int32
 
 namespace Int64
@@ -76,6 +90,10 @@ instance : TransOrd Int64 :=
 instance : LawfulEqOrd Int64 where
   eq_of_compare h := compareOfLessAndEq_eq_eq Int64.le_refl Int64.not_le |>.mp h
 
+instance : LawfulOrderOrd Int64 where
+  isLE_compare _ _ := isLE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+  isGE_compare _ _ := isGE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+
 end Int64
 
 namespace ISize
@@ -90,4 +108,8 @@ instance : TransOrd ISize :=
 instance : LawfulEqOrd ISize where
   eq_of_compare h := compareOfLessAndEq_eq_eq ISize.le_refl ISize.not_le |>.mp h
 
+instance : LawfulOrderOrd ISize where
+  isLE_compare _ _ := isLE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+  isGE_compare _ _ := isGE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+
 end ISize

src/Init/Data/Ord/UInt.lean

@@ -7,8 +7,10 @@ module
 
 prelude
 public import Init.Data.Order.Ord
+public import Init.Data.Order.ClassesExtra
 public import Init.Data.UInt.Basic
 import Init.Data.UInt.Lemmas
+import Init.Data.Order.Lemmas
 
 public section
 
@@ -34,6 +36,10 @@ instance : TransOrd UInt8 :=
 instance : LawfulEqOrd UInt8 where
   eq_of_compare h := compareOfLessAndEq_eq_eq UInt8.le_refl UInt8.not_le |>.mp h
 
+instance : LawfulOrderOrd UInt8 where
+  isLE_compare _ _ := isLE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+  isGE_compare _ _ := isGE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+
 end UInt8
 
 namespace UInt16
@@ -48,6 +54,10 @@ instance : TransOrd UInt16 :=
 instance : LawfulEqOrd UInt16 where
   eq_of_compare h := compareOfLessAndEq_eq_eq UInt16.le_refl UInt16.not_le |>.mp h
 
+instance : LawfulOrderOrd UInt16 where
+  isLE_compare _ _ := isLE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+  isGE_compare _ _ := isGE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+
 end UInt16
 
 namespace UInt32
@@ -62,6 +72,10 @@ instance : TransOrd UInt32 :=
 instance : LawfulEqOrd UInt32 where
   eq_of_compare h := compareOfLessAndEq_eq_eq UInt32.le_refl UInt32.not_le |>.mp h
 
+instance : LawfulOrderOrd UInt32 where
+  isLE_compare _ _ := isLE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+  isGE_compare _ _ := isGE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+
 end UInt32
 
 namespace UInt64
@@ -76,6 +90,10 @@ instance : TransOrd UInt64 :=
 instance : LawfulEqOrd UInt64 where
   eq_of_compare h := compareOfLessAndEq_eq_eq UInt64.le_refl UInt64.not_le |>.mp h
 
+instance : LawfulOrderOrd UInt64 where
+  isLE_compare _ _ := isLE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+  isGE_compare _ _ := isGE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+
 end UInt64
 
 namespace USize
@@ -90,4 +108,8 @@ instance : TransOrd USize :=
 instance : LawfulEqOrd USize where
   eq_of_compare h := compareOfLessAndEq_eq_eq USize.le_refl USize.not_le |>.mp h
 
+instance : LawfulOrderOrd USize where
+  isLE_compare _ _ := isLE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+  isGE_compare _ _ := isGE_compareOfLessAndEq Std.le_antisymm Std.not_le (fun _ _ => Std.le_total)
+
 end USize

src/Init/Data/Order/FactoriesExtra.lean

@@ -69,6 +69,27 @@ public theorem compare_eq_eq {α : Type u} [Ord α] [BEq α] [LE α] [LawfulOrde
   rw [LawfulOrderBEq.beq_iff_le_and_ge, ← isLE_compare, ← isGE_compare]
   cases compare a b <;> simp
 
+public theorem compare_ne_eq {α : Type u} [Ord α] [BEq α] [LE α] [LawfulOrderOrd α] [LawfulOrderBEq α]
+    {a b : α} :
+    compare a b ≠ .eq ↔ ¬ a == b := by
+  simp [compare_eq_eq]
+
+public theorem compare_ne_eq_iff_ne {α : Type u} [Ord α] [LawfulEqOrd α] {a b : α} :
+    compare a b ≠ .eq ↔ a ≠ b := by
+  simp
+
+grind_pattern compare_eq_lt => compare a b, Ordering.lt where
+  guard compare a b = .lt
+
+grind_pattern compare_eq_eq => compare a b, Ordering.eq where
+  guard compare a b = .eq
+
+grind_pattern compare_eq_gt => compare a b, Ordering.gt where
+  guard compare a b = .gt
+
+grind_pattern compare_ne_eq => compare a b, Ordering.eq where
+  guard compare a b ≠ .eq
+
 /--
 Creates a `DecidableLT α` instance using a well-behaved `Ord α` instance.
 -/