feat: infrastructure for cutsat generic ToInt (#9008)

This PR implements the basic infrastructure for the generic `ToInt`
support in `cutsat`.

src/Init/Grind.lean

@@ -19,4 +19,5 @@ import Init.Grind.Module
 import Init.Grind.Ordered
 import Init.Grind.Ext
 import Init.Grind.ToInt
+import Init.Grind.ToIntLemmas
 import Init.Data.Int.OfNat -- This may not have otherwise been imported, breaking `grind` proofs.

src/Init/Grind/ToInt.lean

@@ -35,6 +35,11 @@ inductive IntInterval : Type where
     io (hi : Int)
   | /-- The infinite interval `(-∞, ∞)`. -/
     ii
+  deriving BEq, DecidableEq
+
+instance : LawfulBEq IntInterval where
+   rfl := by intro a; cases a <;> simp_all! [BEq.beq]
+   eq_of_beq := by intro a b; cases a <;> cases b <;> simp_all! [BEq.beq]
 
 namespace IntInterval
 

src/Init/Grind/ToIntLemmas.lean

@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+
+prelude
+import all Init.Grind.ToInt
+
+namespace Lean.Grind.ToInt
+
+/-! Wrap -/
+
+theorem of_eq_wrap_co_0 (i : IntInterval) (hi : Int) (h : i == .co 0 hi) {a b : Int} : a = i.wrap b → a = b % hi := by
+  revert h
+  cases i <;> simp
+  intro h₁ h₂; subst h₁ h₂; simp
+
+/-! Asserted propositions -/
+
+theorem of_eq {α i} [ToInt α i] {a b : α} {a' b' : Int}
+    (h₁ : toInt a = a') (h₂ : toInt b = b') : a = b → a' = b' := by
+  intro h; replace h := congrArg toInt h
+  rw [h₁, h₂] at h; assumption
+
+theorem of_diseq {α i} [ToInt α i] {a b : α} {a' b' : Int}
+    (h₁ : toInt a = a') (h₂ : toInt b = b') : a ≠ b → a' ≠ b' := by
+  intro hne h; rw [← h₁, ← h₂] at h
+  replace h := ToInt.toInt_inj _ _ h; contradiction
+
+theorem of_le {α i} [ToInt α i] [_root_.LE α] [ToInt.LE α i] {a b : α} {a' b' : Int}
+    (h₁ : toInt a = a') (h₂ : toInt b = b') : a ≤ b → a' ≤ b' := by
+  intro h; replace h := ToInt.LE.le_iff _ _ |>.mp h
+  rw [h₁, h₂] at h; assumption
+
+theorem of_not_le {α i} [ToInt α i] [_root_.LE α] [ToInt.LE α i] {a b : α} {a' b' : Int}
+    (h₁ : toInt a = a') (h₂ : toInt b = b') : ¬ (a ≤ b) → b' + 1 ≤ a' := by
+  intro h; have h' := ToInt.LE.le_iff a b
+  simp [h, h₁, h₂] at h'; exact h'
+
+theorem of_lt {α i} [ToInt α i] [_root_.LT α] [ToInt.LT α i] {a b : α} {a' b' : Int}
+    (h₁ : toInt a = a') (h₂ : toInt b = b') : a < b → a' + 1 ≤ b' := by
+  intro h; replace h := ToInt.LT.lt_iff _ _ |>.mp h
+  rw [h₁, h₂] at h; assumption
+
+theorem of_not_lt {α i} [ToInt α i] [_root_.LT α] [ToInt.LT α i] {a b : α} {a' b' : Int}
+    (h₁ : toInt a = a') (h₂ : toInt b = b') : ¬ (a < b) → b' ≤ a' := by
+  intro h; have h' := ToInt.LT.lt_iff a b
+  simp [h, h₁, h₂] at h'; assumption
+
+/-! Addition -/
+
+theorem add_congr {α i} [ToInt α i] [_root_.Add α] [ToInt.Add α i] {a b : α} {a' b' : Int}
+    (h₁ : toInt a = a') (h₂ : toInt b = b') : toInt (a + b) = i.wrap (a' + b') := by
+  rw [ToInt.Add.toInt_add, h₁, h₂]
+
+theorem add_congr.ww {α i} [ToInt α i] [_root_.Add α] [ToInt.Add α i] (h : i.isFinite) {a b : α} {a' b' : Int}
+    (h₁ : toInt a = i.wrap a') (h₂ : toInt b = i.wrap b') : toInt (a + b) = i.wrap (a' + b') := by
+  rw [add_congr h₁ h₂, ← i.wrap_add h]
+
+theorem add_congr.wr {α i} [ToInt α i] [_root_.Add α] [ToInt.Add α i] (h : i.isFinite) (h' : i.nonEmpty) {a b : α} {a' b' : Int}
+    (h₁ : toInt a = a') (h₂ : toInt b = i.wrap b') : toInt (a + b) = i.wrap (a' + b') := by
+  have := i.wrap_eq_self_iff h' _ |>.mpr (ToInt.toInt_mem a)
+  rw [h₁] at this; rw [← this] at h₁; apply add_congr.ww h h₁ h₂
+
+theorem add_congr.wl {α i} [ToInt α i] [_root_.Add α] [ToInt.Add α i] (h : i.isFinite) (h' : i.nonEmpty) {a b : α} {a' b' : Int}
+    (h₁ : toInt a = i.wrap a') (h₂ : toInt b = b') : toInt (a + b) = i.wrap (a' + b') := by
+  have := i.wrap_eq_self_iff h' _ |>.mpr (ToInt.toInt_mem b)
+  rw [h₂] at this; rw [← this] at h₂; apply add_congr.ww h h₁ h₂
+
+/-! Multiplication -/
+
+theorem mul_congr {α i} [ToInt α i] [_root_.Mul α] [ToInt.Mul α i] {a b : α} {a' b' : Int}
+    (h₁ : toInt a = a') (h₂ : toInt b = b') : toInt (a * b) = i.wrap (a' * b') := by
+  rw [ToInt.Mul.toInt_mul, h₁, h₂]
+
+theorem mul_congr.ww {α i} [ToInt α i] [_root_.Mul α] [ToInt.Mul α i] (h : i.isFinite) {a b : α} {a' b' : Int}
+    (h₁ : toInt a = i.wrap a') (h₂ : toInt b = i.wrap b') : toInt (a * b) = i.wrap (a' * b') := by
+  rw [ToInt.Mul.toInt_mul, h₁, h₂, ← i.wrap_mul]; apply h
+
+theorem mul_congr.wr {α i} [ToInt α i] [_root_.Mul α] [ToInt.Mul α i] (h : i.isFinite) (h' : i.nonEmpty) {a b : α} {a' b' : Int}
+    (h₁ : toInt a = a') (h₂ : toInt b = i.wrap b') : toInt (a * b) = i.wrap (a' * b') := by
+  have := i.wrap_eq_self_iff h' _ |>.mpr (ToInt.toInt_mem a)
+  rw [h₁] at this; rw [← this] at h₁; apply mul_congr.ww h h₁ h₂
+
+theorem mul_congr.wl {α i} [ToInt α i] [_root_.Mul α] [ToInt.Mul α i] (h : i.isFinite) (h' : i.nonEmpty) {a b : α} {a' b' : Int}
+    (h₁ : toInt a = i.wrap a') (h₂ : toInt b = b') : toInt (a * b) = i.wrap (a' * b') := by
+  have := i.wrap_eq_self_iff h' _ |>.mpr (ToInt.toInt_mem b)
+  rw [h₂] at this; rw [← this] at h₂; apply mul_congr.ww h h₁ h₂
+
+-- TODO: add theorems for other operations
+
+
+
+end Lean.Grind.ToInt

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

@@ -35,5 +35,6 @@ builtin_initialize registerTraceClass `grind.debug.cutsat.search.assign (inherit
 builtin_initialize registerTraceClass `grind.debug.cutsat.search.conflict (inherited := true)
 builtin_initialize registerTraceClass `grind.debug.cutsat.search.backtrack (inherited := true)
 builtin_initialize registerTraceClass `grind.debug.cutsat.internalize
+builtin_initialize registerTraceClass `grind.debug.cutsat.toInt
 
 end Lean

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

@@ -8,6 +8,7 @@ import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 
@@ -274,7 +275,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
+  | add | mul | num | div | mod | sub | pow | natAbs | toNat | natCast | neg
   deriving BEq
 
 private def getKindAndType? (e : Expr) : Option (SupportedTermKind × Expr) :=
@@ -285,9 +286,9 @@ private def getKindAndType? (e : Expr) : Option (SupportedTermKind × Expr) :=
   | HDiv.hDiv α _ _ _ _ _ => some (.div, α)
   | HMod.hMod α _ _ _ _ _ => some (.mod, α)
   | HPow.hPow α _ _ _ _ _ => some (.pow, α)
-  | OfNat.ofNat α _ _ => some (.num, α)
+  | OfNat.ofNat α _ _     => some (.num, α)
   | Neg.neg α _ a =>
-    let_expr OfNat.ofNat _ _ _ := a | none
+    let_expr OfNat.ofNat _ _ _ := a | some (.neg, α)
     some (.num, α)
   | Int.natAbs _ => some (.natAbs, Nat.mkType)
   | Int.toNat _ => some (.toNat, Nat.mkType)
@@ -300,7 +301,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 | .natAbs | .toNat | .natCast then return false
+  if k matches .div | .mod | .sub | .pow | .neg | .natAbs | .toNat | .natCast then return false
   if declName == ``HAdd.hAdd || declName == ``LE.le || declName == ``Dvd.dvd then return true
   match k with
   | .add => return false
@@ -408,5 +409,10 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
     | .natAbs => propagateNatAbs e
     | .toNat => propagateToNat e
     | _ => internalizeNat e
+  else if let some (e', h) ← toInt? e type then
+    -- TODO: save `(e', h)`
+    trace[grind.debug.cutsat.toInt] "{e} ==> {e'}"
+    trace[grind.debug.cutsat.toInt] "{h} : {← inferType h}"
+    check h
 
 end Lean.Meta.Grind.Arith.Cutsat

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

@@ -501,7 +501,7 @@ def resolveConflict (h : UnsatProof) : SearchM Unit := do
     s.assert
 
 /-- Search for an assignment/model for the linear constraints. -/
-private def searchAssigmentMain : SearchM Unit := do
+private def searchAssignmentMain : SearchM Unit := do
   repeat
     trace[grind.debug.cutsat.search] "main loop"
     checkSystem "cutsat"
@@ -527,7 +527,7 @@ private def resetDecisionStack : SearchM Unit := do
 
 private def searchQLiaAssignment : GoalM Bool := do
   let go : SearchM Bool := do
-    searchAssigmentMain
+    searchAssignmentMain
     let precise := (← get).precise
     resetDecisionStack
     return precise
@@ -535,11 +535,11 @@ private def searchQLiaAssignment : GoalM Bool := do
 
 private def searchLiaAssignment : GoalM Unit := do
   let go : SearchM Unit := do
-    searchAssigmentMain
+    searchAssignmentMain
     resetDecisionStack
   go .int |>.run' {}
 
-def searchAssigment : GoalM Unit := do
+def searchAssignment : GoalM Unit := do
   let precise ← searchQLiaAssignment
   if (← isInconsistent) then return ()
   if !(← getConfig).qlia && !precise then
@@ -564,7 +564,7 @@ def check : GoalM Bool := do
   if (← hasAssignment) then
     return false
   else
-    searchAssigment
+    searchAssignment
     return true
 
 end Lean.Meta.Grind.Arith.Cutsat

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

@@ -0,0 +1,210 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind.ToIntLemmas
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
+
+namespace Lean.Meta.Grind.Arith.Cutsat
+
+private def reportMissingToIntAdapter (type : Expr) (instType : Expr) : MetaM Unit := do
+  trace[grind.debug.cutsat.debug] "`ToInt` initialization failure, failed to synthesize{indentExpr instType}\nfor type{indentExpr type}"
+
+private def throwMissingDecl (declName : Name) : MetaM Unit :=
+  throwError "`grind cutsat`, unexpected missing declaration {declName}"
+
+private def checkDecl (declName : Name) : MetaM Unit := do
+  unless (← getEnv).contains declName do
+    throwMissingDecl declName
+
+private def mkOpCongr (type : Expr) (u : Level) (toIntInst : Expr) (rangeExpr : Expr) (range : Grind.IntInterval) (opBaseName : Name) (thmName : Name) : MetaM ToIntCongr := do
+  let op := mkApp (mkConst opBaseName [u]) type
+  let .some opInst ← trySynthInstance op | return {}
+  let toIntOpName := ``Grind.ToInt ++ opBaseName
+  checkDecl toIntOpName
+  let toIntOp := mkApp4 (mkConst toIntOpName [u]) type opInst rangeExpr toIntInst
+  let .some toIntOpInst ← trySynthInstance toIntOp
+    | reportMissingToIntAdapter type toIntOp; return {}
+  checkDecl thmName
+  let c := mkApp5 (mkConst thmName [u]) type rangeExpr toIntInst opInst toIntOpInst
+  let env ← getEnv
+  let cwwName := thmName ++ `ww
+  let cwlName := thmName ++ `wl
+  let cwrName := thmName ++ `wr
+  let c_ww? := if range.isFinite && env.contains cwwName then
+    some <| mkApp6 (mkConst cwwName [u]) type rangeExpr toIntInst opInst toIntOpInst reflBoolTrue
+  else
+    none
+  let c_wl? := if range.isFinite && range.nonEmpty && env.contains cwwName then
+    some <| mkApp7 (mkConst cwlName [u]) type rangeExpr toIntInst opInst toIntOpInst reflBoolTrue reflBoolTrue
+  else
+    none
+  let c_wr? := if range.isFinite && range.nonEmpty && env.contains cwwName then
+    some <| mkApp7 (mkConst cwrName [u]) type rangeExpr toIntInst opInst toIntOpInst reflBoolTrue reflBoolTrue
+  else
+    none
+  return { c? := some c, c_ww?, c_wl?, c_wr? }
+
+-- TODO: improve this function
+private def evalInt? (e : Expr) : MetaM (Option Int) := do
+  let e ← whnfD e
+  match_expr e with
+  | Int.ofNat a =>
+    let some a ← getNatValue? (← whnfD a) | return none
+    return some (a : Int)
+  | Int.negSucc a =>
+    let some a ← getNatValue? (← whnfD a) | return none
+    return some (- (a : Int) - 1)
+  | _ => return none
+
+def getToIntInfo? (type : Expr) : GoalM (Option ToIntInfo) := do
+  if let some id? := (← get').toIntInfos.find? { expr := type } then
+    return id?
+  else
+    let info? ← go?
+    modify' fun s => { s with toIntInfos := s.toIntInfos.insert { expr := type } info? }
+    return info?
+where
+  toIntInterval? (rangeExpr : Expr) : GoalM (Option Grind.IntInterval) := do
+    let rangeExpr ← whnfD rangeExpr
+    match_expr rangeExpr with
+    | Grind.IntInterval.co lo hi =>
+      let some lo ← evalInt? lo
+        | trace[grind.debug.cutsat.toInt] "`ToInt` lower bound could not be reduced to an integer{indentExpr (← whnfD lo)}\nfor type{indentExpr type}"
+          return none
+      let some hi ← evalInt? hi
+        | trace[grind.debug.cutsat.toInt] "`ToInt` upper bound could not be reduced to an integer{indentExpr hi}\nfor type{indentExpr type}"
+          return none
+      return some (.co lo hi)
+    | _ =>
+      trace[grind.debug.cutsat.toInt] "unsupported `ToInt` interval{indentExpr rangeExpr}\nfor type{indentExpr type}"
+      return none
+
+  go? : GoalM (Option ToIntInfo) := withNewMCtxDepth do
+    let u' ← getLevel type
+    let u ← decLevel u'
+    let rangeExpr ← mkFreshExprMVar (mkConst ``Grind.IntInterval)
+    let toIntType := mkApp2 (mkConst ``Grind.ToInt [u]) type rangeExpr
+    let .some toIntInst ← trySynthInstance toIntType |
+      trace[grind.debug.cutsat.toInt] "failed to synthesize {indentExpr toIntType}"
+      return none
+    let rangeExpr ← instantiateMVars rangeExpr
+    let some range ← toIntInterval? rangeExpr | return none
+    let toInt := mkApp3 (mkConst ``Grind.ToInt.toInt [u]) type rangeExpr toIntInst
+    let wrap := mkApp (mkConst ``Grind.IntInterval.wrap) rangeExpr
+    let ofWrap0? := if let .co 0 hi := range then
+      some <| mkApp3 (mkConst ``Grind.ToInt.of_eq_wrap_co_0) rangeExpr (toExpr hi) reflBoolTrue
+    else
+      none
+    let ofEq := mkApp3 (mkConst ``Grind.ToInt.of_eq [u]) type rangeExpr toIntInst
+    let ofDiseq := mkApp3 (mkConst ``Grind.ToInt.of_diseq [u]) type rangeExpr toIntInst
+    let (ofLE?, ofNotLE?) ← do
+      let toLE := mkApp (mkConst ``LE [u]) type
+      let .some leInst ← LOption.toOption <$> trySynthInstance toLE | pure (none, none)
+      let toIntLE := mkApp4 (mkConst ``Grind.ToInt.LE [u]) type leInst rangeExpr toIntInst
+      let .some toIntLEInst ← LOption.toOption <$> trySynthInstance toIntLE
+        | reportMissingToIntAdapter type toIntLE; pure (none, none)
+      let ofLE := mkApp5 (mkConst ``Grind.ToInt.of_le [u]) type rangeExpr toIntInst leInst toIntLEInst
+      let ofNotLE := mkApp5 (mkConst ``Grind.ToInt.of_not_le [u]) type rangeExpr toIntInst leInst toIntLEInst
+      pure (some ofLE, some ofNotLE)
+    let (ofLT?, ofNotLT?) ← do
+      let toLT := mkApp (mkConst ``LT [u]) type
+      let .some ltInst ← LOption.toOption <$> trySynthInstance toLT | pure (none, none)
+      let toIntLT := mkApp4 (mkConst ``Grind.ToInt.LT [u]) type ltInst rangeExpr toIntInst
+      let .some toIntLTInst ← LOption.toOption <$> trySynthInstance toIntLT
+        | reportMissingToIntAdapter type toIntLT; pure (none, none)
+      let ofLT := mkApp5 (mkConst ``Grind.ToInt.of_lt [u]) type rangeExpr toIntInst ltInst toIntLTInst
+      let ofNotLT := mkApp5 (mkConst ``Grind.ToInt.of_not_lt [u]) type rangeExpr toIntInst ltInst toIntLTInst
+      pure (some ofLT, some ofNotLT)
+    let mkOp (opBaseName : Name) (thmName : Name) :=
+      mkOpCongr type u toIntInst rangeExpr range opBaseName thmName
+    let add ← mkOp ``Add ``Grind.ToInt.add_congr
+    let mul ← mkOp ``Mul ``Grind.ToInt.mul_congr
+    -- TODO: other operators
+    return some {
+      type, u, toIntInst, rangeExpr, range, toInt, wrap, ofWrap0?, ofEq, ofDiseq, ofLE?, ofNotLE?, ofLT?, ofNotLT?, add, mul
+    }
+
+structure ToIntM.Context where
+  info : ToIntInfo
+
+abbrev ToIntM := ReaderT ToIntM.Context GoalM
+
+def getInfo : ToIntM ToIntInfo :=
+  return (← read).info
+
+def ToIntM.run? (type : Expr) (x : ToIntM α) : GoalM (Option α) := do
+  let some info ← getToIntInfo? type | return none
+  return some (← x { info })
+
+private def isHomo (α β γ : Expr) : Bool :=
+  isSameExpr α β && isSameExpr α γ
+
+private def intRfl := mkApp (mkConst ``Eq.refl [1]) Int.mkType
+
+private def toIntDef (e : Expr) : ToIntM (Expr × Expr) := do
+  let e' := mkApp (← getInfo).toInt e
+  let he := mkApp intRfl e'
+  return (e', he)
+
+private def isWrap (e : Expr) : Option Expr :=
+  match_expr e with
+  | Grind.IntInterval.wrap _ a => some a
+  | _ => none
+
+/--
+Given `h : toInt a = i.wrap b`, return `(b', h)` where
+`b'` is the expanded form of `i.wrap b`, and `h : toInt a = b'`
+-/
+private def expandWrap (a b : Expr) (h : Expr) : ToIntM (Expr × Expr) := do
+  match (← getInfo).range with
+  | .ii => return (b, h)
+  | .co 0 hi =>
+    let b' := mkIntMod b (toExpr hi)
+    let toA := mkApp (← getInfo).toInt a
+    let h := mkApp3 (← getInfo).ofWrap0?.get! toA b h
+    return (b', h)
+  | .co lo hi =>
+    let b' := mkIntAdd (mkIntMod (mkIntSub b (toExpr lo)) (toExpr (hi - lo))) (toExpr lo)
+    return (b', h)
+  | _ => throwError "`grind cutsat`, `ToInt` interval not supported yet"
+
+private def mkToIntResult (toIntOp : ToIntCongr) (mkBinOp : Expr → Expr → Expr) (a b : Expr) (a' b' : Expr) (h₁ h₂ : Expr) : ToIntM (Expr × Expr) := do
+  let f := toIntOp.c?.get!
+  let mk (f : Expr) (a' b' : Expr) : ToIntM (Expr × Expr) := do
+    let h := mkApp6 f a b a' b' h₁ h₂
+    let r := mkApp (← getInfo).wrap (mkBinOp a' b')
+    return (r, h)
+  match isWrap a', isWrap b' with
+  | none,     none     => mk f a' b'
+  | some a'', none     => if let some f := toIntOp.c_wl? then mk f a'' b' else mk f a' b'
+  | none,     some b'' => if let some f := toIntOp.c_wr? then mk f a' b'' else mk f a' b'
+  | some a'', some b'' => if let some f := toIntOp.c_ww? then mk f a'' b'' else mk f a' b'
+
+partial def toInt (e : Expr) : ToIntM (Expr × Expr) := do
+  match_expr e with
+  | HAdd.hAdd α β γ _ a b =>
+    unless isHomo α β γ do return (← toIntDef e)
+    toIntBin (← getInfo).add mkIntAdd a b
+  | HMul.hMul α β γ _ a b =>
+    unless isHomo α β γ do return (← toIntDef e)
+    toIntBin (← getInfo).mul mkIntMul a b
+  -- TODO: other operators
+  | _ => toIntDef e
+where
+  toIntBin (toIntOp : ToIntCongr) (mkBinOp : Expr → Expr → Expr) (a b : Expr) : ToIntM (Expr × Expr) := do
+    unless toIntOp.c?.isSome do return (← toIntDef e)
+    let (a', h₁) ← toInt a
+    let (b', h₂) ← toInt b
+    mkToIntResult toIntOp mkBinOp a b a' b' h₁ h₂
+
+def toInt? (a : Expr) (type : Expr) : GoalM (Option (Expr × Expr)) := do
+  ToIntM.run? type do
+    let (b, h) ← toInt a
+    match isWrap b with
+    | some b' => expandWrap a b' h
+    | _ => return (b, h)
+
+end Lean.Meta.Grind.Arith.Cutsat

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

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind.ToInt
+import Lean.Meta.Tactic.Grind.Arith.Util
+
+namespace Lean.Meta.Grind.Arith.Cutsat
+open Lean Grind
+
+structure ToIntCongr where
+  c?    : Option Expr := none
+  c_ww? : Option Expr := none
+  c_wl? : Option Expr := none
+  c_wr? : Option Expr := none
+
+structure ToIntInfo where
+  type      : Expr
+  u         : Level
+  toIntInst : Expr
+  rangeExpr : Expr
+  range     : IntInterval
+  toInt     : Expr
+  wrap      : Expr
+  -- theorem `of_eq_wrap_co_0` if `range == .co 0 hi`
+  ofWrap0?  : Option Expr
+  ofEq      : Expr
+  ofDiseq   : Expr
+  ofLE?     : Option Expr
+  ofNotLE?  : Option Expr
+  ofLT?     : Option Expr
+  ofNotLT?  : Option Expr
+  add       : ToIntCongr
+  mul       : ToIntCongr
+  -- TODO: other operators
+
+end Lean.Meta.Grind.Arith.Cutsat

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

@@ -9,6 +9,7 @@ import Std.Internal.Rat
 import Lean.Data.PersistentArray
 import Lean.Meta.Tactic.Grind.ExprPtr
 import Lean.Meta.Tactic.Grind.Arith.Util
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 
@@ -153,7 +154,7 @@ inductive DvdCnstrProof where
   /-- `c.c₃?` must be `some` -/
   | cooper₂ (c : CooperSplit)
 
-/-- An inequalirty constraint and its justification/proof. -/
+/-- An inequality constraint and its justification/proof. -/
 structure LeCnstr where
   p  : Poly
   h  : LeCnstrProof
@@ -197,7 +198,7 @@ inductive DiseqCnstrProof where
 
 /--
 A proof of `False`.
-Remark: We will later add support for a backtraking search inside of cutsat.
+Remark: We will later add support for a backtracking search inside of cutsat.
 -/
 inductive UnsatProof where
   | dvd (c : DvdCnstr)
@@ -306,7 +307,7 @@ structure State where
   - `Int.Linear.emod_le`
   -/
   divMod : PHashSet (Expr × Int) := {}
-  /- TODO: Model-based theory combination. -/
+  toIntInfos : PHashMap ExprPtr (Option ToIntInfo) := {}
   deriving Inhabited
 
 end Lean.Meta.Grind.Arith.Cutsat