feat: Toint inequalities in cutsat (#9026)

This PR implements support for (non strict) `ToInt` inequalities in
`grind cutsat`. `grind cutsat` can solve simple problems such as:
```lean
example (a b c : Fin 11) : a ≤ b → b ≤ c → a ≤ c := by
  grind

example (a b c : Fin 11) : c ≤ 9 → a ≤ b → b ≤ c → a ≤ c + 1 := by
  grind

example (a b c : UInt8) : a ≤ b → b ≤ c → a ≤ c := by
  grind

example (a b c d : UInt32) : a ≤ b → b ≤ c → c ≤ d → a ≤ d := by
  grind
```
Next step: strict inequalities, and equalities.

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

@@ -382,7 +382,6 @@ private def internalizeNat (e : Expr) : GoalM Unit := do
   let c := { p := .add (-1) x p, h := .defnNat e' x e'' : EqCnstr }
   c.assert
 
-
 private def isToIntForbiddenParent (parent? : Option Expr) : Bool :=
   if let some parent := parent? then
     getKindAndType? parent |>.isSome
@@ -410,20 +409,25 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
     | _ => internalizeInt e
   else if type.isConstOf ``Nat then
     if isForbiddenParent parent? k then return ()
-    trace[grind.debug.cutsat.internalize] "{e} : {type}"
     if (← isNatTerm e) then return ()
+    trace[grind.debug.cutsat.internalize] "{e} : {type}"
     discard <| mkNatVar e
     match k with
     | .sub => propagateNatSub e
     | .natAbs => propagateNatAbs e
     | .toNat => propagateToNat e
     | _ => internalizeNat e
-  else if let some (e', h) ← toInt? e type then
+  else
     if isToIntForbiddenParent parent? then return ()
-    trace[grind.debug.cutsat.internalize] "{e} : {type}"
-    -- TODO: save `(e', h)`
-    trace[grind.debug.cutsat.toInt] "{e} ==> {e'}"
-    trace[grind.debug.cutsat.toInt] "{h} : {← inferType h}"
-    check h
+    -- Term has already been internalized
+    if (← isToIntTerm e) then return ()
+    if let some (eToInt, he) ← toInt? e type then
+      trace[grind.debug.cutsat.internalize] "{e} : {type}"
+      trace[grind.debug.cutsat.toInt] "{e} ==> {eToInt}"
+      let α := type
+      modify' fun s => { s with
+        toIntTermMap := s.toIntTermMap.insert { expr := e } { eToInt, he, α }
+      }
+      markAsCutsatTerm e
 
 end Lean.Meta.Grind.Arith.Cutsat

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

@@ -11,6 +11,7 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 
@@ -160,12 +161,29 @@ def propagateNatLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do
   trace[grind.cutsat.assert.le] "{← c.pp}"
   c.assert
 
-def propagateIfSupportedLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do
+def propagateToIntLe (e : Expr) (eqTrue : Bool) : ToIntM Unit := do
+  let some thm ← if eqTrue then pure (← getInfo).ofLE? else pure (← getInfo).ofNotLE? | return ()
+  let_expr LE.le _ _ a b := e | return ()
+  let gen ← getGeneration e
+  let (a', h₁) ← toInt a
+  let (b', h₂) ← toInt b
+  let thm := mkApp6 thm a b a' b' h₁ h₂
+  let (a', b') := if eqTrue then (a', b') else (mkIntAdd b' (mkIntLit 1), a')
+  let lhs ← toLinearExpr a' gen
+  let rhs ← toLinearExpr b' gen
+  let p := lhs.sub rhs |>.norm
+  let c := { p, h := .coreToInt e eqTrue thm lhs rhs : LeCnstr }
+  trace[grind.cutsat.assert.le] "{← c.pp}"
+  c.assert
+
+def propagateLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do
   unless (← getConfig).cutsat do return ()
   let_expr LE.le α _ _ _ := e | return ()
   if α.isConstOf ``Nat then
     propagateNatLe e eqTrue
-  else
+  else if α.isConstOf ``Int then
     propagateIntLe e eqTrue
+  else ToIntM.run α do
+    propagateToIntLe e eqTrue
 
 end Lean.Meta.Grind.Arith.Cutsat

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

@@ -200,6 +200,10 @@ partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := caching c' do
     let ctx ← getNatContext
     let h := mkApp4 (mkConst ``Int.OfNat.of_le) ctx (← mkNatExprDecl lhs) (← mkNatExprDecl rhs) (mkOfEqTrueCore e (← mkEqTrueProof e))
     return mkApp6 (mkConst ``Int.Linear.le_norm_expr) (← getContext) (← mkExprDecl lhs') (← mkExprDecl rhs') (← mkPolyDecl c'.p) reflBoolTrue h
+  | .coreToInt e pos toIntThm lhs rhs =>
+    let h ← if pos then pure <| mkOfEqTrueCore e (← mkEqTrueProof e) else pure <| mkOfEqFalseCore e (← mkEqFalseProof e)
+    let h := mkApp toIntThm h
+    return mkApp6 (mkConst ``Int.Linear.le_norm_expr) (← getContext) (← mkExprDecl lhs) (← mkExprDecl rhs) (← mkPolyDecl c'.p) reflBoolTrue h
   | .denoteAsIntNonneg rhs rhs' =>
     let ctx ← getNatContext
     let h := mkApp2 (mkConst ``Int.OfNat.Expr.denoteAsInt_nonneg) ctx (toExpr rhs)
@@ -395,7 +399,7 @@ partial def DvdCnstr.collectDecVars (c' : DvdCnstr) : CollectDecVarsM Unit := do
 
 partial def LeCnstr.collectDecVars (c' : LeCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do
   match c'.h with
-  | .core .. | .coreNeg .. | .coreNat .. | .coreNatNeg .. | .denoteAsIntNonneg .. => return ()
+  | .core .. | .coreNeg .. | .coreNat .. | .coreNatNeg .. | .coreToInt .. | .denoteAsIntNonneg .. => return ()
   | .dec h => markAsFound h
   | .cooper c | .norm c | .divCoeffs c => c.collectDecVars
   | .dvdTight c₁ c₂ | .negDvdTight c₁ c₂

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

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Grind.ToIntLemmas
+import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 
 namespace Lean.Meta.Grind.Arith.Cutsat
@@ -156,6 +157,7 @@ where
     let powThm? ← mkPowThm? type u toIntInst rangeExpr
     let zeroThm? ← mkSimpleOpThm? ``Zero ``Grind.ToInt.zero_eq
     let ofNatThm? ← mkOfNatThm? type u toIntInst rangeExpr
+    trace[grind.debug.cutsat.toInt] "registered toInt: {type}"
     return some {
       type, u, toIntInst, rangeExpr, range, toInt, wrap, ofWrap0?, ofEq, ofDiseq, ofLE?, ofNotLE?, ofLT?, ofNotLT?, addThms, mulThms,
       subThm?, negThm?, divThm?, modThm?, powThm?, zeroThm?, ofNatThm?
@@ -173,15 +175,33 @@ 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 α γ
+def ToIntM.run (type : Expr) (x : ToIntM Unit) : GoalM Unit := do
+  let some info ← getToIntInfo? type | return ()
+  x { info }
 
 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)
+def mkToIntVar (e : Expr) : ToIntM (Expr × Expr) := do
+  if let some info := (← get').toIntTermMap.find? { expr := e } then
+    return (info.eToInt, info.he)
+  let eToInt := mkApp (← getInfo).toInt e
+  let he := mkApp intRfl eToInt
+  let α := (← getInfo).type
+  modify' fun s => { s with
+    toIntTermMap := s.toIntTermMap.insert { expr := e } { eToInt, he, α }
+  }
+  markAsCutsatTerm e
+  return (eToInt, he)
+
+def getToIntTermType? (e : Expr) : GoalM (Option Expr) := do
+  let some info := (← get').toIntTermMap.find? { expr := e } | return none
+  return some info.α
+
+def isToIntTerm (e : Expr) : GoalM Bool :=
+  return (← get').toIntTermMap.contains { expr := e }
+
+private def isHomo (α β γ : Expr) : Bool :=
+  isSameExpr α β && isSameExpr α γ
 
 private def isWrap (e : Expr) : Option Expr :=
   match_expr e with
@@ -232,52 +252,52 @@ private def ToIntThms.mkResult (toIntThms : ToIntThms) (mkBinOp : Expr → Expr
   | none,     some b'' => if let some f := toIntThms.c_wr? then mk f a' b'' else mk f a' b'
   | some a'', some b'' => if let some f := toIntThms.c_ww? then mk f a'' b'' else mk f a' b'
 
-partial def toInt (e : Expr) : ToIntM (Expr × Expr) := do
+private partial def toInt' (e : Expr) : ToIntM (Expr × Expr) := do
   match_expr e with
   | HAdd.hAdd α β γ _ a b =>
-    unless isHomo α β γ do return (← toIntDef e)
+    unless isHomo α β γ do return (← mkToIntVar e)
     toIntBin (← getInfo).addThms mkIntAdd a b
   | HMul.hMul α β γ _ a b =>
-    unless isHomo α β γ do return (← toIntDef e)
+    unless isHomo α β γ do return (← mkToIntVar e)
     toIntBin (← getInfo).mulThms mkIntMul a b
   | HDiv.hDiv α β γ _ a b =>
-    unless isHomo α β γ do return (← toIntDef e)
+    unless isHomo α β γ do return (← mkToIntVar e)
     processDivMod (isDiv := true) a b
   | HMod.hMod α β γ _ a b =>
-    unless isHomo α β γ do return (← toIntDef e)
+    unless isHomo α β γ do return (← mkToIntVar e)
     processDivMod (isDiv := false) a b
   | HSub.hSub α β γ _ a b =>
-    unless isHomo α β γ do return (← toIntDef e)
+    unless isHomo α β γ do return (← mkToIntVar e)
     processSub a b
   | Neg.neg _ _ a =>
     processNeg a
   | HPow.hPow α β γ _ a b =>
-    unless isSameExpr α γ && β.isConstOf ``Nat do return (← toIntDef e)
+    unless isSameExpr α γ && β.isConstOf ``Nat do return (← mkToIntVar e)
     processPow a b
   | Zero.zero _ _ =>
-    let some thm := (← getInfo).zeroThm? | toIntDef e
+    let some thm := (← getInfo).zeroThm? | mkToIntVar e
     return (mkIntLit 0, thm)
   | OfNat.ofNat _ n _ =>
-    let some thm := (← getInfo).ofNatThm? | toIntDef e
-    let some n ← getNatValue? n | toIntDef e
+    let some thm := (← getInfo).ofNatThm? | mkToIntVar e
+    let some n ← getNatValue? n | mkToIntVar e
     let r := mkIntLit ((← getInfo).range.wrap n)
     let h := mkApp thm (toExpr n)
     return (r, h)
-  | _ => toIntDef e
+  | _ => mkToIntVar e
 where
   toIntBin (toIntOp : ToIntThms) (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
+    unless toIntOp.c?.isSome do return (← mkToIntVar e)
+    let (a', h₁) ← toInt' a
+    let (b', h₂) ← toInt' b
     toIntOp.mkResult mkBinOp a b a' b' h₁ h₂
 
   toIntAndExpandWrap (a : Expr) : ToIntM (Expr × Expr) := do
-    let (a', h₁) ← toInt a
+    let (a', h₁) ← toInt' a
     expandIfWrap a a' h₁
 
   processDivMod (isDiv : Bool) (a b : Expr) : ToIntM (Expr × Expr) := do
     let some thm ← if isDiv then pure (← getInfo).divThm? else pure (← getInfo).modThm?
-      | return (← toIntDef e)
+      | return (← mkToIntVar e)
     let (a', h₁) ← toIntAndExpandWrap a
     let (b', h₂) ← toIntAndExpandWrap b
     let r := if isDiv then mkIntDiv a' b' else mkIntMod a' b'
@@ -285,7 +305,7 @@ where
     return (r, h)
 
   processSub (a b : Expr) : ToIntM (Expr × Expr) := do
-    let some thm := (← getInfo).subThm? | return (← toIntDef e)
+    let some thm := (← getInfo).subThm? | return (← mkToIntVar e)
     let (a', h₁) ← toIntAndExpandWrap a
     let (b', h₂) ← toIntAndExpandWrap b
     let r ← mkWrap (mkIntSub a' b')
@@ -293,24 +313,37 @@ where
     return (r, h)
 
   processNeg (a : Expr) : ToIntM (Expr × Expr) := do
-    let some thm := (← getInfo).negThm? | return (← toIntDef e)
+    let some thm := (← getInfo).negThm? | return (← mkToIntVar e)
     let (a', h₁) ← toIntAndExpandWrap a
     let r ← mkWrap (mkIntNeg a')
     let h := mkApp3 thm a a' h₁
     return (r, h)
 
   processPow (a b : Expr) : ToIntM (Expr × Expr) := do
-    let some thm := (← getInfo).powThm? | return (← toIntDef e)
+    let some thm := (← getInfo).powThm? | return (← mkToIntVar e)
     let (a', h₁) ← toIntAndExpandWrap a
     let r ← mkWrap (mkIntPowNat a' b)
     let h := mkApp4 thm a b a' h₁
     return (r, 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
+def toInt (a : Expr) : ToIntM (Expr × Expr) := do
+  let (b, h) ← toInt' a
+  let (b, h) ← match isWrap b with
     | some b' => expandWrap a b' h
-    | _ => return (b, h)
+    | _ => pure (b, h)
+  let r ← preprocess b
+  if let some proof := r.proof? then
+    return (r.expr, (← mkEqTrans h proof))
+  else
+    return (r.expr, h)
+
+def toInt? (a : Expr) (type : Expr) : GoalM (Option (Expr × Expr)) := do
+  ToIntM.run? type do toInt a
+
+def isSupportedType (type : Expr) : GoalM Bool := do
+  if type == Nat.mkType || type == Int.mkType then
+    return true
+  else
+    return (← getToIntInfo? type).isSome
 
 end Lean.Meta.Grind.Arith.Cutsat

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

@@ -70,4 +70,14 @@ structure ToIntInfo where
   zeroThm?  : Option Expr
   ofNatThm? : Option Expr
 
+/--
+For each term `e` of type `α` which implements the `ToInt α i` class,
+we store its corresponding `Int` term `eToInt`, a proof `he : toInt e = eToInt`,
+and the type `α`.
+-/
+structure ToIntTermInfo where
+  eToInt : Expr
+  α      : Expr
+  he     : Expr
+
 end Lean.Meta.Grind.Arith.Cutsat

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

@@ -164,6 +164,7 @@ inductive LeCnstrProof where
   | coreNeg (e : Expr) (p : Poly)
   | coreNat (e : Expr) (lhs rhs : Int.OfNat.Expr) (lhs' rhs' : Int.Linear.Expr)
   | coreNatNeg (e : Expr) (lhs rhs : Int.OfNat.Expr) (lhs' rhs' : Int.Linear.Expr)
+  | coreToInt (e : Expr) (pos : Bool) (toIntThm : Expr) (lhs rhs : Int.Linear.Expr)
   | denoteAsIntNonneg (rhs : Int.OfNat.Expr) (rhs' : Int.Linear.Expr)
   | dec (h : FVarId)
   | norm (c : LeCnstr)
@@ -303,7 +304,16 @@ structure State where
   - `Int.Linear.emod_le`
   -/
   divMod : PHashSet (Expr × Int) := {}
+  /--
+  Mapping from a type `α` to its corresponding `ToIntInfo` object, which contains
+  the information needed to embed `α` terms into `Int` terms.
+  -/
   toIntInfos : PHashMap ExprPtr (Option ToIntInfo) := {}
+  /--
+  For each type `α` in `toIntInfos`, the mapping `toIntVarMap` contains a mapping
+  from a α-term `e` to the pair `(toInt e, α)`.
+  -/
+  toIntTermMap : PHashMap ExprPtr ToIntTermInfo := {}
   deriving Inhabited
 
 end Lean.Meta.Grind.Arith.Cutsat

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

@@ -28,9 +28,6 @@ end Int.Linear
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 
-def isSupportedType (type : Expr) : Bool :=
-  type == Nat.mkType || type == Int.mkType
-
 def get' : GoalM State := do
   return (← get).arith.cutsat
 

src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Grind.Ordered.Module
 import Lean.Meta.Tactic.Grind.Simp
-import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
 import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 import Lean.Meta.Tactic.Grind.Arith.Linear.Util
 import Lean.Meta.Tactic.Grind.Arith.Linear.Var
@@ -55,11 +55,16 @@ private def isNonTrivialIsCharInst (isCharInst? : Option (Expr × Nat)) : Bool :
   | some (_, c) => c != 1
   | none => false
 
+private def isCutsatType (type : Expr) : GoalM Bool := do
+  if (← getConfig).cutsat then
+    if (← Cutsat.isSupportedType type) then
+      -- If `type` is supported by cutsat, let it handle
+      return true
+  return false
+
 def getStructId? (type : Expr) : GoalM (Option Nat) := do
   unless (← getConfig).linarith do return none
-  if (← getConfig).cutsat && Cutsat.isSupportedType type then
-    -- If `type` is supported by cutsat, let it handle
-    return none
+  if (← isCutsatType type) then return none
   if let some id? := (← get').typeIdOf.find? { expr := type } then
     return id?
   else
@@ -150,11 +155,11 @@ where
       pure (some leFn, some ltFn)
     else
       pure (none, none)
-    let getHSMulFn? : GoalM (Option Expr) := do
+    let rec getHSMulFn? : GoalM (Option Expr) := do
       let smulType := mkApp3 (mkConst ``HSMul [0, u, u]) Int.mkType type type
       let .some smulInst ← trySynthInstance smulType | return none
       internalizeFn <| mkApp4 (mkConst ``HSMul.hSMul [0, u, u]) Int.mkType type smulInst smulInst
-    let getHSMulNatFn? : GoalM (Option Expr) := do
+    let rec getHSMulNatFn? : GoalM (Option Expr) := do
       let smulType := mkApp3 (mkConst ``HSMul [0, u, u]) Nat.mkType type type
       let .some smulInst ← trySynthInstance smulType | return none
       internalizeFn <| mkApp4 (mkConst ``HSMul.hSMul [0, u, u]) Nat.mkType type smulInst smulInst
@@ -164,7 +169,7 @@ where
     let semiringInst? ← getInst? ``Grind.Semiring
     let ringInst? ← getInst? ``Grind.Ring
     let fieldInst? ← getInst? ``Grind.Field
-    let getOne? : GoalM (Option Expr) := do
+    let rec getOne? : GoalM (Option Expr) := do
       let some oneInst ← getInst? ``One | return none
       let one ← internalizeConst <| mkApp2 (mkConst ``One.one [u]) type oneInst
       let one' ← mkNumeral type 1
@@ -182,7 +187,7 @@ where
       return some inst
     let orderedRingInst? ← getOrderedRingInst?
     let charInst? ← if let some semiringInst := semiringInst? then getIsCharInst? u type semiringInst else pure none
-    let getNoNatZeroDivInst? : GoalM (Option Expr) := do
+    let rec getNoNatZeroDivInst? : GoalM (Option Expr) := do
       let hmulNat := mkApp3 (mkConst ``HMul [0, u, u]) Nat.mkType type type
       let .some hmulInst ← trySynthInstance hmulNat | return none
       let noNatZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type hmulInst

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

@@ -32,12 +32,12 @@ builtin_grind_propagator propagateLE ↓LE.le := fun e => do
   if (← isEqTrue e) then
     if let some c ← Offset.isCnstr? e then
       Offset.assertTrue c (← mkEqTrueProof e)
-    Cutsat.propagateIfSupportedLe e (eqTrue := true)
+    Cutsat.propagateLe e (eqTrue := true)
     Linear.propagateIneq e (eqTrue := true)
   else if (← isEqFalse e) then
     if let some c ← Offset.isCnstr? e then
       Offset.assertFalse c (← mkEqFalseProof e)
-    Cutsat.propagateIfSupportedLe e (eqTrue := false)
+    Cutsat.propagateLe e (eqTrue := false)
     Linear.propagateIneq e (eqTrue := false)
 
 builtin_grind_propagator propagateLT ↓LT.lt := fun e => do

tests/lean/run/grind_cutsat_toint_1.lean

@@ -0,0 +1,11 @@
+example (a b c : Fin 11) : a ≤ b → b ≤ c → a ≤ c := by
+  grind
+
+example (a b c : Fin 11) : c ≤ 9 → a ≤ b → b ≤ c → a ≤ c + 1 := by
+  grind
+
+example (a b c : UInt8) : a ≤ b → b ≤ c → a ≤ c := by
+  grind
+
+example (a b c d : UInt32) : a ≤ b → b ≤ c → c ≤ d → a ≤ d := by
+  grind