chore: further algebra tests for grind

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

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

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

tests/lean/grind/algebra/ordered_modules.lean

@@ -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