feat: typeclasses for grind to work with ordered modules (#8347)

This PR adds draft typeclasses for `grind` to process facts about
ordered modules. These interfaces will evolve as the implementation
develops.

Author: kim-em

src/Init/Grind.lean

@@ -15,4 +15,5 @@ import Init.Grind.Util
 import Init.Grind.Offset
 import Init.Grind.PP
 import Init.Grind.CommRing
+import Init.Grind.Module
 import Init.Grind.Ext

src/Init/Grind/Module.lean

@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Init.Grind.Module.Basic
+import Init.Grind.Module.Int

src/Init/Grind/Module/Basic.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Init.Data.Int.Order
+
+namespace Lean.Grind
+
+class NatModule (M : Type u) extends Zero M, Add M, HSMul Nat M M where
+  add_zero : ∀ a : M, a + 0 = a
+  zero_add : ∀ a : M, 0 + a = a
+  add_comm : ∀ a b : M, a + b = b + a
+  add_assoc : ∀ a b c : M, a + b + c = a + (b + c)
+  zero_smul : ∀ a : M, 0 • a = 0
+  one_smul : ∀ a : M, 1 • a = a
+  add_smul : ∀ n m : Nat, ∀ a : M, (n + m) • a = n • a + m • a
+  smul_zero : ∀ n : Nat, n • (0 : M) = 0
+  smul_add : ∀ n : Nat, ∀ a b : M, n • (a + b) = n • a + n • b
+  mul_smul : ∀ n m : Nat, ∀ a : M, (n * m) • a = n • (m • a)
+
+class IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub M, HSMul Int M M where
+  add_zero : ∀ a : M, a + 0 = a
+  zero_add : ∀ a : M, 0 + a = a
+  add_comm : ∀ a b : M, a + b = b + a
+  add_assoc : ∀ a b c : M, a + b + c = a + (b + c)
+  zero_smul : ∀ a : M, (0 : Int) • a = 0
+  one_smul : ∀ a : M, (1 : Int) • a = a
+  add_smul : ∀ n m : Int, ∀ a : M, (n + m) • a = n • a + m • a
+  neg_smul : ∀ n : Int, ∀ a : M, (-n) • a = - (n • a)
+  smul_zero : ∀ n : Int, n • (0 : M) = 0
+  smul_add : ∀ n : Int, ∀ a b : M, n • (a + b) = n • a + n • b
+  mul_smul : ∀ n m : Int, ∀ a : M, (n * m) • a = n • (m • a)
+  neg_add_cancel : ∀ a : M, -a + a = 0
+  sub_eq_add_neg : ∀ a b : M, a - b = a + -b
+
+instance IntModule.toNatModule (M : Type u) [i : IntModule M] : NatModule M :=
+  { i with
+    hSMul a x := (a : Int) • x
+    smul_zero := by simp [IntModule.smul_zero]
+    add_smul := by simp [IntModule.add_smul]
+    smul_add := by simp [IntModule.smul_add]
+    mul_smul := by simp [IntModule.mul_smul] }
+
+/--
+We keep track of rational linear combinations as integer linear combinations,
+but with the assurance that we can cancel the GCD of the coefficients.
+-/
+class RatModule (M : Type u) extends IntModule M where
+  no_int_zero_divisors : ∀ (k : Int) (a : M), k ≠ 0 → k • a = 0 → a = 0
+
+/-- A preorder is a reflexive, transitive relation `≤` with `a < b` defined in the obvious way. -/
+class Preorder (α : Type u) extends LE α, LT α where
+  le_refl : ∀ a : α, a ≤ a
+  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
+  lt := fun a b => a ≤ b ∧ ¬b ≤ a
+  lt_iff_le_not_le : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl
+
+class IntModule.IsOrdered (M : Type u) [Preorder M] [IntModule M] where
+  neg_le_iff : ∀ a b : M, -a ≤ b ↔ -b ≤ a
+  neg_lt_iff : ∀ a b : M, -a < b ↔ -b < a
+  add_lt_left : ∀ a b c : M, a < b → a + c < b + c
+  add_lt_right : ∀ a b c : M, a < b → c + a < c + b
+  smul_pos : ∀ (k : Int) (a : M), 0 < a → (0 < k ↔ 0 < k • a)
+  smul_neg : ∀ (k : Int) (a : M), a < 0 → (0 < k ↔ k • a < 0)
+  smul_nonneg : ∀ (k : Int) (a : M), 0 ≤ a → 0 ≤ k → 0 ≤ k • a
+  smul_nonpos : ∀ (k : Int) (a : M), a ≤ 0 → 0 ≤ k → k • a ≤ 0
+
+end Lean.Grind

src/Init/Grind/Module/Int.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Init.Grind.Module.Basic
+import Init.Omega
+
+/-!
+# `grind` instances for `Int` as an ordered module.
+-/
+
+namespace Lean.Grind
+
+instance : IntModule Int where
+  add_zero := Int.add_zero
+  zero_add := Int.zero_add
+  add_comm := Int.add_comm
+  add_assoc := Int.add_assoc
+  zero_smul := Int.zero_mul
+  one_smul := Int.one_mul
+  add_smul := Int.add_mul
+  neg_smul := Int.neg_mul
+  smul_zero := Int.mul_zero
+  smul_add := Int.mul_add
+  mul_smul := Int.mul_assoc
+  neg_add_cancel := Int.add_left_neg
+  sub_eq_add_neg _ _ := Int.sub_eq_add_neg
+
+instance : Preorder Int where
+  le_refl := Int.le_refl
+  le_trans _ _ _ := Int.le_trans
+  lt_iff_le_not_le := by omega
+
+instance : IntModule.IsOrdered Int where
+  neg_le_iff := by omega
+  neg_lt_iff := by omega
+  add_lt_left := by omega
+  add_lt_right := by omega
+  smul_pos k a ha := ⟨fun hk => Int.mul_pos hk ha, fun h => Int.pos_of_mul_pos_left h ha⟩
+  smul_neg k a ha := ⟨fun hk => Int.mul_neg_of_pos_of_neg hk ha, fun h => Int.pos_of_mul_neg_left h ha⟩
+  smul_nonpos k a ha hk := Int.mul_nonpos_of_nonneg_of_nonpos hk ha
+  smul_nonneg k a ha hk := Int.mul_nonneg hk ha
+
+end Lean.Grind

tests/lean/grind/module_normalization.lean

@@ -0,0 +1,32 @@
+-- Tests for `grind` as a module normalization tactic, when only `NatModule`, `IntModule`, or `RatModule` is available.
+
+open Lean.Grind
+
+section NatModule
+
+variable (R : Type u) [NatModule R]
+
+example (a b : R) : a + b = b + a := by grind
+example (a : R) : a + 0 = a := by grind
+example (a : R) : 0 + a = a := by grind
+example (a b c : R) : a + b + c = a + (b + c) := by grind
+example (a : R) : 2 • a = a + a := by grind
+example (a b : R) : 2 • (b + c) = c + 2 • b + c := by grind
+
+end NatModule
+
+section IntModule
+
+variable (R : Type u) [IntModule R]
+
+example (a b : R) : a + b = b + a := by grind
+example (a : R) : a + 0 = a := by grind
+example (a : R) : 0 + a = a := by grind
+example (a b c : R) : a + b + c = a + (b + c) := by grind
+example (a : R) : 2 • a = a + a := by grind
+example (a : R) : (-2 : Int) • a = -a - a := by grind
+example (a b : R) : 2 • (b + c) = c + 2 • b + c := by grind
+example (a b c : R) : 2 • (b + c) - 3 • c + b + b = c + 5 • b - 2 • c := by grind
+example (a b c : R) : 2 • (b + c) + (-3 : Int) • c + b + b = c + (5 : Int) • b - 2 • c := by grind
+
+end IntModule

tests/lean/grind/module_relations.lean

@@ -0,0 +1,27 @@
+-- Tests for `grind` as solver for linear equations in an `IntModule` or `RatModule`.
+
+open Lean.Grind
+
+section IntModule
+
+variable (R : Type u) [IntModule R]
+
+-- In an `IntModule`, we should be able to handle relations
+-- this is harder, and less important, than being able to do this in `RatModule`.
+example (a b : R) (h : a + b = 0) : 3 • a - 7 • b = 9 • a + a := by grind
+example (a b c : R) (h : 2 • a + 2 • b = 4 • c) : 3 • a + c = 5 • c - b + (-b) + a := by grind
+
+end IntModule
+
+section RatModule
+
+variable (R : Type u) [RatModule R]
+
+example (a b : R) (h : a + b = 0) : 3 • a - 7 • b = 9 • a + a := by grind
+example (a b c : R) (h : 2 • a + 2 • b = 4 • c) : 3 • a + c = 5 • c - b + (-b) + a := by grind
+
+-- In a `RatModule` we can clear common divisors.
+example (a : R) (h : a + a = 0) : a = 0 := by grind
+example (a b c : R) (h : 2 • a + 2 • b = 4 • c) : 3 • a + c = 5 • c - 3 • b := by grind
+
+end RatModule

tests/lean/grind/ordered_modules.lean

@@ -0,0 +1,64 @@
+open Lean.Grind
+
+set_option grind.warning false
+
+variable (R : Type u) [RatModule R] [Preorder R] [IntModule.IsOrdered 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 : R) (h : a < b) : -a < -b := 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 b : R) (h : a ≤ b) : -a ≤ -b := 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 : R) (_ : a < b) (_ : b < a) : False := by grind
+example (a b : R) (_ : a < b ∧ b < a) : False := by grind
+example (a b : R) (_ : a < b) : a ≠ b := 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 : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : 12 * y - 4 * z < 0) : False := by
+  grind
+example (x y z : R) (h1 : 2 • x < 3 • y) (h2 : -4 • x + 2 • z < 0) (h3 : 12 • y - 4 • z < 0) : False := by
+  grind
+
+example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : x * y < 5) (h3 : 12 * y - 4 * z < 0) :
+    False := by grind
+example (x y z : R) (h1 : 2 • x < 3 • y) (h2 : -4 • x + 2 • z < 0) (h3 : 12 • y - 4 • z < 0) :
+    False := by grind
+
+example (x y z : Int) (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 : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : x * y < 5) : ¬ 12*y - 4* z < 0 := by
+  grind
+example (x y z : R) (h1 : 2 • x < 3 • y) (h2 : -4 • x + 2 • z < 0) : ¬ 12 • y - 4 • z < 0 := by
+  grind
+
+example (x y z : Int) (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 : Nat) (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

tests/lean/run/infoFromFailure.lean

@@ -16,7 +16,21 @@ info: B.foo "hello" : String × String
 ---
 trace: [Meta.synthInstance] ❌️ Add String
   [Meta.synthInstance] new goal Add String
-    [Meta.synthInstance.instances] #[@Lean.Grind.Semiring.toAdd]
+    [Meta.synthInstance.instances] #[@Lean.Grind.Semiring.toAdd, @Lean.Grind.NatModule.toAdd, @Lean.Grind.IntModule.toAdd]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAdd to Add String
+    [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
+    [Meta.synthInstance] new goal Lean.Grind.IntModule String
+      [Meta.synthInstance.instances] #[@Lean.Grind.RatModule.toIntModule]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.RatModule.toIntModule to Lean.Grind.IntModule String
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule String ≟ Lean.Grind.IntModule String
+    [Meta.synthInstance] no instances for Lean.Grind.RatModule String
+      [Meta.synthInstance.instances] #[]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAdd to Add String
+    [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
+    [Meta.synthInstance] new goal Lean.Grind.NatModule String
+      [Meta.synthInstance.instances] #[Lean.Grind.IntModule.toNatModule]
+  [Meta.synthInstance] ✅️ apply Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule String
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule String ≟ Lean.Grind.NatModule String
   [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add String
     [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
     [Meta.synthInstance] new goal Lean.Grind.Semiring String
@@ -47,7 +61,21 @@ trace: [Meta.synthInstance] ❌️ Add String
 /--
 trace: [Meta.synthInstance] ❌️ Add Bool
   [Meta.synthInstance] new goal Add Bool
-    [Meta.synthInstance.instances] #[@Lean.Grind.Semiring.toAdd]
+    [Meta.synthInstance.instances] #[@Lean.Grind.Semiring.toAdd, @Lean.Grind.NatModule.toAdd, @Lean.Grind.IntModule.toAdd]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAdd to Add Bool
+    [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
+    [Meta.synthInstance] new goal Lean.Grind.IntModule Bool
+      [Meta.synthInstance.instances] #[@Lean.Grind.RatModule.toIntModule]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.RatModule.toIntModule to Lean.Grind.IntModule Bool
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule Bool ≟ Lean.Grind.IntModule Bool
+    [Meta.synthInstance] no instances for Lean.Grind.RatModule Bool
+      [Meta.synthInstance.instances] #[]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAdd to Add Bool
+    [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
+    [Meta.synthInstance] new goal Lean.Grind.NatModule Bool
+      [Meta.synthInstance.instances] #[Lean.Grind.IntModule.toNatModule]
+  [Meta.synthInstance] ✅️ apply Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule Bool
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule Bool ≟ Lean.Grind.NatModule Bool
   [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add Bool
     [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
     [Meta.synthInstance] new goal Lean.Grind.Semiring Bool

tests/lean/run/info_trees.lean

@@ -61,7 +61,7 @@ info: • command @ ⟨82, 0⟩-⟨82, 40⟩ @ Lean.Elab.Command.elabDeclaration
                   ⊢ 0 ≤ n
                   after no goals
                   • Nat.zero_le n : 0 ≤ n @ ⟨1, 1⟩†-⟨1, 1⟩† @ Lean.Elab.Term.elabApp
-                    • [.] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.41 @ ⟨1, 0⟩†-⟨1, 0⟩†
+                    • [.] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.42 @ ⟨1, 0⟩†-⟨1, 0⟩†
                     • Nat.zero_le : ∀ (n : Nat), 0 ≤ n @ ⟨1, 0⟩†-⟨1, 0⟩†
                     • n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† @ Lean.Elab.Term.elabIdent
                       • [.] n : some Nat @ ⟨1, 5⟩†-⟨1, 5⟩†