From 18e1cdb7bb69dbafcd5efdf2e9874e4e73b13c8c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 1 Aug 2025 23:30:54 +0200
Subject: [PATCH] fix: user provided `ToInt.toInt` applications (#9673)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR ensures that `grind cutsat` processes `ToInt.toInt` applications
provided by the user. Example:

```lean
open Lean Grind
example (x : Fin 3) : ToInt.toInt x ≠ 0 → ToInt.toInt x ≠ 1 → ToInt.toInt x ≠ 2 → False := by
  grind -ring

example (x y z : Fin 5) : ToInt.toInt (x + z) = ToInt.toInt y → z = 0 → x = y := by
  grind -ring
```
---
 .../Tactic/Grind/Arith/Cutsat/EqCnstr.lean    | 18 +++++++++++++--
 tests/lean/run/grind_toInt_issue.lean         | 22 +++++++++++++++++++
 2 files changed, 38 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/grind_toInt_issue.lean

diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
index 9481101b72..932eb48aac 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
@@ -341,7 +341,7 @@ def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
 
 /-- Different kinds of terms internalized by this module. -/
 private inductive SupportedTermKind where
-  | add | mul | num | div | mod | sub | pow | natAbs | toNat | natCast | neg
+  | add | mul | num | div | mod | sub | pow | natAbs | toNat | natCast | neg | toInt
   deriving BEq, Repr
 
 private def getKindAndType? (e : Expr) : Option (SupportedTermKind × Expr) :=
@@ -359,6 +359,7 @@ private def getKindAndType? (e : Expr) : Option (SupportedTermKind × Expr) :=
   | Int.natAbs _ => some (.natAbs, Nat.mkType)
   | Int.toNat _ => some (.toNat, Nat.mkType)
   | NatCast.natCast α _ _ => some (.natCast, α)
+  | Grind.ToInt.toInt _ _ _ _ => some (.toInt, Int.mkType)
   | _ => none
 
 private def isForbiddenParent (parent? : Option Expr) (k : SupportedTermKind) : Bool := Id.run do
@@ -367,7 +368,7 @@ private def isForbiddenParent (parent? : Option Expr) (k : SupportedTermKind) :
   -- TODO: document `NatCast.natCast` case.
   -- Remark: we added it to prevent natCast_sub from being expanded twice.
   if declName == ``NatCast.natCast then return true
-  if k matches .div | .mod | .sub | .pow | .neg | .natAbs | .toNat | .natCast then return false
+  if k matches .div | .mod | .sub | .pow | .neg | .natAbs | .toNat | .natCast | .toInt then return false
   if declName == ``HAdd.hAdd || declName == ``LE.le || declName == ``Dvd.dvd then return true
   match k with
   | .add => return false
@@ -417,6 +418,18 @@ private def propagateMod (e : Expr) : GoalM Unit := do
     let some b ← getIntValue? b | return ()
     expandDivMod a b
 
+private def propagateToInt (e : Expr) : GoalM Unit := do
+  let_expr Grind.ToInt.toInt α _ _ a := e | return ()
+  if (← isToIntTerm a) then return ()
+  let some (eToInt, he) ← toInt? a α | return ()
+  discard <| mkVar e
+  if isSameExpr e eToInt then return ()
+  modify' fun s => { s with
+    toIntTermMap := s.toIntTermMap.insert { expr := a } { eToInt, he, α }
+  }
+  let prop := mkIntEq e eToInt
+  pushNewFact <| mkExpectedPropHint he prop
+
 private def propagateNatAbs (e : Expr) : GoalM Unit := do
   let_expr Int.natAbs a := e | return ()
   pushNewFact <| mkApp (mkConst ``Lean.Omega.Int.ofNat_natAbs) a
@@ -437,6 +450,7 @@ private def internalizeIntTerm (e type : Expr) (parent? : Option Expr) (k : Supp
   match k with
   | .div => propagateDiv e
   | .mod => propagateMod e
+  | .toInt => propagateToInt e
   | _ => internalizeInt e
 
 private def internalizeNatTerm (e type : Expr) (parent? : Option Expr) (k : SupportedTermKind) : GoalM Unit := do
diff --git a/tests/lean/run/grind_toInt_issue.lean b/tests/lean/run/grind_toInt_issue.lean
new file mode 100644
index 0000000000..832f7d25fa
--- /dev/null
+++ b/tests/lean/run/grind_toInt_issue.lean
@@ -0,0 +1,22 @@
+open Lean Grind
+
+example (x : Fin 2) : ToInt.toInt x ≠ 0 → ToInt.toInt x ≠ 1 → False := by
+  grind -ring
+
+example (x : Fin 3) : x ≠ 1 → x ≠ 2 → x ≠ 0 → False := by
+  grind -ring
+
+example (x : Fin 3) : x ≠ 1 → x ≠ 2 → ToInt.toInt x ≠ 0 → False := by
+  grind -ring
+
+example (x : Fin 3) : ToInt.toInt x ≠ 0 → x ≠ 1 → x ≠ 2 → False := by
+  grind -ring
+
+example (x : Fin 3) : ToInt.toInt x ≠ 0 → ToInt.toInt x ≠ 1 → ToInt.toInt x ≠ 2 → False := by
+  grind -ring
+
+example (x y z : Fin 5) : ToInt.toInt (x + z) = ToInt.toInt y → z = 0 → x = y := by
+  grind -ring
+
+example (x y : Fin 5) : ToInt.toInt (x + 0) = ToInt.toInt y → x = y := by
+  grind -ring