From 0ab69a32cbc59aafdc9a143672974c299e040452 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Fri, 25 Jul 2025 18:46:05 +1000
Subject: [PATCH] chore: parameterize NoNatZeroDivisors by NatModule instead of
 HMul (#9527)

This PR changes `Lean.Grind.NoNatZeroDivisors` so that it is
parametrised by a `NatModule` instance rather than just a `HMul`
instance. This is sufficiently general for our purposes, and is a
band-aid (~40% improvement) for the performance problems we've been
seeing coming from inference here. The problems observed in Mathlib may
not see much improvement, however.
---
 src/Init/Grind/Module/Basic.lean                      | 2 +-
 src/Lean/Meta/Tactic/Grind/Arith/Insts.lean           | 6 +++---
 src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean | 6 +++---
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/Init/Grind/Module/Basic.lean b/src/Init/Grind/Module/Basic.lean
index 9ba285283b..d0352a7182 100644
--- a/src/Init/Grind/Module/Basic.lean
+++ b/src/Init/Grind/Module/Basic.lean
@@ -255,7 +255,7 @@ For a module over the integers this is equivalent to
 (See the alternative constructor `NoNatZeroDivisors.mk'`,
 and the theorem `eq_zero_of_mul_eq_zero`.)
 -/
-class NoNatZeroDivisors (α : Type u) [HMul Nat α α] where
+class NoNatZeroDivisors (α : Type u) [NatModule α] where
   /-- If `k * a ≠ k * b` then `k ≠ 0` or `a ≠ b`.-/
   no_nat_zero_divisors : ∀ (k : Nat) (a b : α), k ≠ 0 → k * a = k * b → a = b
 
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Insts.lean b/src/Lean/Meta/Tactic/Grind/Arith/Insts.lean
index aaacc95af5..08ec0ee2c2 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Insts.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Insts.lean
@@ -18,9 +18,9 @@ def getIsCharInst? (u : Level) (type : Expr) (semiringInst : Expr) : GoalM (Opti
   return some (charInst, n)
 
 def getNoZeroDivInst? (u : Level) (type : Expr) : GoalM (Option Expr) := do
-  let hmulType := mkApp3 (mkConst ``HMul [0, u, u]) (mkConst ``Nat []) type type
-  let some hmulInst ← synthInstance? hmulType | return none
-  let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type hmulInst
+  let natModuleType := mkApp (mkConst ``Grind.NatModule [u]) type
+  let some natModuleInst ← synthInstance? natModuleType | return none
+  let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type natModuleInst
   synthInstance? noZeroDivType
 
 end Lean.Meta.Grind.Arith
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean
index 748f7bec87..7013bcf63e 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean
@@ -103,9 +103,9 @@ private def mkOrderedRingInst? (u : Level) (type : Expr) (semiringInst? preorder
   return some inst
 
 private def mkNoNatZeroDivInst? (u : Level) (type : Expr) : GoalM (Option Expr) := do
-  let hmulNat := mkApp3 (mkConst ``HMul [0, u, u]) Nat.mkType type type
-  let some hmulInst ← synthInstance? hmulNat | return none
-  synthInstance? <| mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type hmulInst
+  let natModuleType := mkApp (mkConst ``Grind.NatModule [u]) type
+  let some natModuleInst ← synthInstance? natModuleType | return none
+  synthInstance? <| mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type natModuleInst
 
 def getStructId? (type : Expr) : GoalM (Option Nat) := do
   unless (← getConfig).linarith do return none