From 449bc31832604562dc46c203e110077eff8598a9 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Tue, 24 Jun 2025 13:51:39 +1000
Subject: [PATCH] chore: adds (failing) grind algebra tests (#8961)

---
 src/Init/Grind/Ordered/Int.lean               |  4 ++-
 tests/lean/grind/algebra/nat.lean             | 15 ++++++++
 tests/lean/grind/algebra/nlinarith.lean       | 14 ++++++++
 tests/lean/grind/algebra/ordered_modules.lean | 36 -------------------
 4 files changed, 32 insertions(+), 37 deletions(-)
 create mode 100644 tests/lean/grind/algebra/nat.lean
 create mode 100644 tests/lean/grind/algebra/nlinarith.lean
 delete mode 100644 tests/lean/grind/algebra/ordered_modules.lean

diff --git a/src/Init/Grind/Ordered/Int.lean b/src/Init/Grind/Ordered/Int.lean
index 5e3e095ec2..fbcbe6e356 100644
--- a/src/Init/Grind/Ordered/Int.lean
+++ b/src/Init/Grind/Ordered/Int.lean
@@ -16,10 +16,12 @@ import Init.Omega
 
 namespace Lean.Grind
 
-instance : Preorder Int where
+instance : LinearOrder Int where
   le_refl := Int.le_refl
   le_trans := Int.le_trans
   lt_iff_le_not_le := by omega
+  le_antisymm := Int.le_antisymm
+  le_total := Int.le_total
 
 instance : OrderedAdd Int where
   add_le_left_iff := by omega
diff --git a/tests/lean/grind/algebra/nat.lean b/tests/lean/grind/algebra/nat.lean
new file mode 100644
index 0000000000..28f42aa4e4
--- /dev/null
+++ b/tests/lean/grind/algebra/nat.lean
@@ -0,0 +1,15 @@
+
+open Lean.Grind
+
+variable [CommRing R] [LinearOrder R] [OrderedRing R]
+example (a b : R) (h : 0 ≤ a * b) : 0 ≤ b * a := by grind
+example (a b : R) (h : 7 ≤ a * b) : 7 ≤ b * a := by grind
+
+-- These should work by specializing `R` to `Int`!
+example (a b : Int) (h : 0 ≤ a * b) : 0 ≤ b * a := by grind
+example (a b : Int) (h : 7 ≤ a * b) : 7 ≤ b * a := by grind
+
+-- These should work by embedding `Nat` into its Grothendieck completion,
+-- and using that the embedding is monotone.
+example (a b : Nat) (h : 0 ≤ a * b) : 0 ≤ b * a := by grind
+example (a b : Nat) (h : 7 ≤ a * b) : 7 ≤ b * a := by grind
diff --git a/tests/lean/grind/algebra/nlinarith.lean b/tests/lean/grind/algebra/nlinarith.lean
new file mode 100644
index 0000000000..bc91ad220e
--- /dev/null
+++ b/tests/lean/grind/algebra/nlinarith.lean
@@ -0,0 +1,14 @@
+open Lean.Grind
+
+variable (R : Type) [CommRing R] [LinearOrder R] [OrderedRing R]
+
+example (a : R) : 0 ≤ a^2 := by grind
+example (a : R) : 0 ≤ a^6 := by grind
+example (a b : R) (_ : 0 ≤ a) (_ : 0 ≤ b) : 0 ≤ a * b := by grind
+example (a b : R) (_ : a ≤ 0) (_ : 0 ≤ b) : a * b ≤ 0 := by grind
+example (a b c : R) (_ : 0 ≤ a) (_ : b ≤ c) : a * b ≤ a * c := by grind
+example (a b : R) (_ : 1 ≤ a) (_ : 1 ≤ b) : 1 ≤ a * b := by grind
+example (a b : R) (_ : 3 ≤ a) (_ : 4 ≤ b) : 12 ≤ a * b := by grind
+example (a : R) (_ : 3 ≤ a) : 9 ≤ a^2 := by grind
+example (a b : R) (_ : 0 ≤ a) (_ : a ≤ b) : a^2 ≤ b^2 := by grind
+example (a b : R) (_ : 0 ≤ a^3) (_ : 0 ≤ a * b) (_ : 0 ≤ b^3) : 0 ≤ a^5 * b^5 := by grind
diff --git a/tests/lean/grind/algebra/ordered_modules.lean b/tests/lean/grind/algebra/ordered_modules.lean
deleted file mode 100644
index dc437fa82e..0000000000
--- a/tests/lean/grind/algebra/ordered_modules.lean
+++ /dev/null
@@ -1,36 +0,0 @@
-open Lean.Grind
-
--- Many of these should work with less than `LinearOrder`.
-variable (R : Type u) [IntModule R] [NoNatZeroDivisors R] [LinearOrder R] [OrderedAdd R]
-
-example (a b c : R) (h : a < b) : a + c < b + c := by grind
-example (a b c : R) (h : a < b) : c + a < c + b := by grind
-example (a b : R) (h : a < b) : -b < -a := by grind
-
-example (a b c : R) (h : a ≤ b) : a + c ≤ b + c := by grind
-example (a b c : R) (h : a ≤ b) : c + a ≤ c + b := by grind
-example (a b : R) (h : a ≤ b) : -b ≤ -a := by grind
-
-example (a : R) (h : 0 < a) : 0 ≤ a := by grind
-example (a : R) (h : 0 < a) : -2 * a < 0 := by grind
-
-example (a b c : R) (_ : a ≤ b) (_ : b ≤ c) : a ≤ c := by grind
-example (a b c : R) (_ : a ≤ b) (_ : b < c) : a < c := by grind
-example (a b c : R) (_ : a < b) (_ : b ≤ c) : a < c := by grind
-example (a b c : R) (_ : a < b) (_ : b < c) : a < c := by grind
-
-example (a : R) (h : 2 * a < 0) : a < 0 := by grind
-example (a : R) (h : 2 * a < 0) : 0 ≤ -a := by grind
-
-example (a b c e v0 v1 : R) (h1 : v0 = 5 * a) (h2 : v1 = 3 * b) (h3 : v0 + v1 + c = 10 * e) :
-    v0 + 5 * e + (v1 - 3 * e) + (c - 2 * e) = 10 * e := by
-  grind
-
-example (x y z : R) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
-  grind
-
-example (x y z : R) (hx : ¬ x > 3 * y) (h2 : ¬ y > 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
-  grind
-
-example (x y z : R) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
-  grind