From af22926d53556500e173cbc802e21328585bbf19 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Wed, 25 Jun 2025 12:44:59 +1000
Subject: [PATCH] chore: updates to (failing) grind algebra tests (#8987)

---
 tests/lean/grind/algebra/nat.lean        | 3 ++-
 tests/lean/grind/algebra/nat_module.lean | 4 ++--
 tests/lean/grind/algebra/nlinarith.lean  | 2 ++
 3 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/tests/lean/grind/algebra/nat.lean b/tests/lean/grind/algebra/nat.lean
index 28f42aa4e4..7b3f6a84b8 100644
--- a/tests/lean/grind/algebra/nat.lean
+++ b/tests/lean/grind/algebra/nat.lean
@@ -5,7 +5,8 @@ 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`!
+-- These don't work because `cutsat` disables `linarith`.
+-- We could use the CommRing normalizer in cutsat to solve these.
 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
 
diff --git a/tests/lean/grind/algebra/nat_module.lean b/tests/lean/grind/algebra/nat_module.lean
index e8af18dc6a..1e0608adc7 100644
--- a/tests/lean/grind/algebra/nat_module.lean
+++ b/tests/lean/grind/algebra/nat_module.lean
@@ -6,7 +6,7 @@ variable (M : Type) [IntModule M]
 
 example (x y : M) : 2 * x + 3 * y + x = 3 * (x + y) := by grind
 
-variable [LinearOrder M]
+variable [LinearOrder M] [OrderedAdd M]
 
 example {x y : M} (h : x ≤ y) : 2 * x + y ≤ 3 * y := by grind
 
@@ -19,7 +19,7 @@ variable (M : Type) [NatModule M]
 
 example (x y : M) : 2 * x + 3 * y + x = 3 * (x + y) := by grind
 
-variable [LinearOrder M]
+variable [LinearOrder M] [OrderedAdd M]
 
 example {x y : M} (h : x ≤ y) : 2 * x + y ≤ 3 * y := by grind
 
diff --git a/tests/lean/grind/algebra/nlinarith.lean b/tests/lean/grind/algebra/nlinarith.lean
index bc91ad220e..2999558e23 100644
--- a/tests/lean/grind/algebra/nlinarith.lean
+++ b/tests/lean/grind/algebra/nlinarith.lean
@@ -1,5 +1,7 @@
 open Lean.Grind
 
+-- TODO which other systems, e.g. Mathematica, Isabelle, nlia, can handle these?
+
 variable (R : Type) [CommRing R] [LinearOrder R] [OrderedRing R]
 
 example (a : R) : 0 ≤ a^2 := by grind