From 97d63db52cd2fc3353f8a75f48209de0011f1bd3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 25 Oct 2025 21:35:34 -0700
Subject: [PATCH] fix: `mbtc` for nonlinear terms in `grind cutsat` (#10965)

This PR ensures that model-based theory combination in `grind cutsat`
considers nonlinear terms. Nonlinear multiplications such as `x * y` are
treated as uninterpreted symbols in `cutsat`.

Closes #10885
---
 .../Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean  | 29 ++++++++++++++++++-
 tests/lean/run/grind_10885.lean               | 11 +++++++
 2 files changed, 39 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/grind_10885.lean

diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean
index 68ea31e07c..678f593876 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean
@@ -46,8 +46,35 @@ private def getAssignmentExt? (e : Expr) : GoalM (Option Rat) := do
 private def hasTheoryVar (e : Expr) : GoalM Bool := do
   cutsatExt.hasTermAtRoot e
 
+/-
+**Note**: cutsat is a procedure for linear integer arithmetic. Thus, morally a
+nonlinear multiplication, division, and modulo are **not** interpreted by cutsat.
+Thus, we enable model-theory combination for them. This is necessary for examples
+such as:
+```
+example {a b : Nat} (ha : 1 ≤ a) : (a - 1 + 1) * b = a * b := by grind
+```
+Note that we currently use a restrictive/cheaper version of mbtc. We only case-split
+on `a = b`, if they have the same assignment **and** occur as the `i`-th argument of
+the same function symbol. The latter reduces the number of case-splits we have to
+perform, but misses the following variant of the problem above.
+```
+example {a b : Nat} (ha : 1 ≤ a) : (a - 1 + 1) * b = b * a := by grind
+```
+If this becomes an issue in practice, we can add a flag for enabling the more
+expensive version of `mbtc`.
+-/
+
+private def isNonlinearTerm (e : Expr) : GoalM Bool :=
+  match_expr e with
+  | HMul.hMul _ _ _ _ a b => return (← getIntValue? a <|> getIntValue? b).isNone
+  | HDiv.hDiv _ _ _ _ _ b => return (← getIntValue? b).isNone
+  | HMod.hMod _ _ _ _ _ b => return (← getIntValue? b).isNone
+  | _ => return false
+
 private def isInterpreted (e : Expr) : GoalM Bool := do
-  if isInterpretedTerm e then return true
+  if isInterpretedTerm e then
+    return !(← isNonlinearTerm e)
   let f := e.getAppFn
   /-
   **Note**: `grind` normalizes terms, but some of them cannot be rewritten by `simp` because
diff --git a/tests/lean/run/grind_10885.lean b/tests/lean/run/grind_10885.lean
new file mode 100644
index 0000000000..f1dff54024
--- /dev/null
+++ b/tests/lean/run/grind_10885.lean
@@ -0,0 +1,11 @@
+example {a b : Nat} (ha : 1 ≤ a) : (a - 1 + 1) * b = a * b := by grind
+
+/--
+info: Try this:
+  [apply] ⏎
+    mbtc
+    cases #9501
+-/
+#guard_msgs in
+example {a b : Nat} (ha : 1 ≤ a) : (a - 1 + 1) * b = a * b := by
+  grind => finish? -- mbtc was applied consider nonlinear `*`