fix: user provided ToInt.toInt applications (#9673)

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

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

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