feat: model-based theory combination for ToInt types (#10325)

This PR implements model-based theory combination for types `A` which
implement the `ToInt` interface. Examples:
```lean
example {C : Type} (h : Fin 4 → C) (x : Fin 4)
    : 3 ≤ x → x ≤ 3 → h x = h (-1) := by
  grind

example {C : Type} (h : UInt8 → C) (x y z w : UInt8)
    : y + 1 + w ≤ x + w → x + w ≤ z → z ≤ y + w + 1 → h (x + w) = h (y + w + 1) := by
  grind

example {C : Type} (h : Fin 8 → C) (x y w r : Fin 8)
    : y + 1 + w ≤ r → r ≤ y + w + x → x = 1 → h r = h (y + w + 1) := by
  grind
```

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean

@@ -602,7 +602,10 @@ private def propagateMod (e : Expr) : GoalM Unit := do
 
 private def propagateToInt (e : Expr) : GoalM Unit := do
   let_expr Grind.ToInt.toInt α _ _ a := e | return ()
-  if (← isToIntTerm a) then return ()
+  if (← isToIntTerm a) then
+    -- Save the mapping `a ==> e` for model construction
+    modify' fun s => { s with toIntVarMap := s.toIntVarMap.insert { expr := a } e }
+    return ()
   let some (eToInt, he) ← toInt? a α | return ()
   discard <| mkVar e
   if isSameExpr e eToInt then return ()

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.Tactic.Grind.MBTC
 import Lean.Meta.Tactic.Grind.Arith.ModelUtil
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
@@ -13,19 +13,38 @@ public section
 namespace Lean.Meta.Grind.Arith.Cutsat
 
 private def getAssignmentExt? (e : Expr) : GoalM (Option Rat) := do
-  let val? ← getAssignment? (← get) e
-  if val?.isSome then
-    return val?
+  if let some val ← getAssignment? (← get) e then
+    -- Easy case when `e : Int`
+    return some val
   let type ← inferType e
-  if type == Nat.mkType then
+  if type == Int.mkType then
+    -- It should have been handled in the previous getAssignment?
+    return none
+  else if type == Nat.mkType then
+    -- TODO: improve this case.
     for parent in (← getParents e) do
       let_expr NatCast.natCast _ inst _ := parent | pure ()
       let_expr instNatCastInt := inst | pure ()
       return (← getAssignment? (← get) parent)
+  else
+    -- It may be a `ToInt` term.
+    if let some x := (← get').toIntVarMap.find? { expr := e } then
+      -- If there is an int variable `x` for `toInt e`, use its assignment.
+      if let some val ← getAssignment? (← get) x then
+        return some val
+    if let some info := (← get').toIntTermMap.find? { expr := e } then
+      -- If `toInt e` is an integer value, return it.
+      if let some val ← getIntValue? info.eToInt then
+        return some val
+      -- If `toInt e` is a composite int term that has been internalized
+      -- and has an assignment, return it.
+      if (← alreadyInternalized info.eToInt) then
+        if let some val ← getAssignment? (← get) info.eToInt then
+          return some val
   return none
 
 private def hasTheoryVar (e : Expr) : GoalM Bool := do
-  return (← getAssignmentExt? e).isSome
+  cutsatExt.hasTermAtRoot e
 
 private def isInterpreted (e : Expr) : GoalM Bool := do
   if isInterpretedTerm e then return true

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean

@@ -349,6 +349,13 @@ structure State where
   from a α-term `e` to the pair `(toInt e, α)`.
   -/
   toIntTermMap : PHashMap ExprPtr ToIntTermInfo := {}
+  -- Note: the terms in the range `toIntTermMap` may not have been internalized.
+  -- Note: we may reconsider this design decision to simplify model construction.
+  /--
+  Mapping from `a : α` (where `ToInt α`) to `toInt a` that has been internalized.
+  We use this information during model construction.
+  -/
+  toIntVarMap : PHashMap ExprPtr Expr := {}
   /--
   `usedCommRing` is `true` if the `CommRing` has been used to normalize expressions.
   -/

tests/lean/run/grind_toInt_mbtc.lean

@@ -0,0 +1,19 @@
+example {C : Type} (h : Fin 4 → C) (x y z : Fin 4)
+    : y + 1 ≤ x → x ≤ z → z ≤ y + 1 → h x = h (y + 1) := by
+  grind
+
+example {C : Type} (h : Fin 4 → C) (x : Fin 4)
+    : 3 ≤ x → x ≤ 3 → h x = h (-1) := by
+  grind
+
+example {C : Type} (h : UInt8 → C) (x y z w : UInt8)
+    : y + 1 + w ≤ x + w → x + w ≤ z → z ≤ y + w + 1 → h (x + w) = h (y + w + 1) := by
+  grind
+
+example {C : Type} (h : Nat → C) (x y z w r : Nat)
+    : y + 1 + w ≤ x + w → x + w ≤ r → r ≤ x + w → x + w ≤ z → z ≤ y + w + 1 → h r = h (y + w + 1) := by
+  grind
+
+example {C : Type} (h : Fin 8 → C) (x y w r : Fin 8)
+    : y + 1 + w ≤ r → r ≤ y + w + x → x = 1 → h r = h (y + w + 1) := by
+  grind