feat: assert ToInt bounds in grind cutsat (#9050)

This PR ensures the `ToInt` bounds are asserted for every `toInt a`
application internalized in `grind cutsat`.

src/Init/Grind/ToIntLemmas.lean

@@ -130,4 +130,18 @@ theorem ofNat_eq {α i} [ToInt α i] [∀ n, _root_.OfNat α n] [ToInt.OfNat α
 theorem zero_eq {α i} [ToInt α i] [_root_.Zero α] [ToInt.Zero α i] : toInt (0 : α) = 0 := by
   apply ToInt.Zero.toInt_zero
 
+/-! Lower and upper bounds -/
+
+theorem ge_lower {α i} [ToInt α i] (lo : Int) (h : i.lo? == some lo) (a : α) : -1 * toInt a + lo ≤ 0 := by
+  have h' := ToInt.toInt_mem a
+  revert h h'; cases i <;> simp [IntInterval.lo?] <;> intro h <;> subst h <;> intros <;> omega
+
+theorem ge_lower0 {α i} [ToInt α i] (h : i.lo? == some 0) (a : α) : -1 * toInt a ≤ 0 := by
+  have h' := ToInt.toInt_mem a
+  revert h h'; cases i <;> simp [IntInterval.lo?] <;> intro h <;> subst h <;> intros <;> omega
+
+theorem le_upper {α i} [ToInt α i] (hi' : Int) (h : i.hi? == some (-hi' + 1)) (a : α) : toInt a + hi' ≤ 0 := by
+  have h' := ToInt.toInt_mem a
+  revert h h'; cases i <;> simp [IntInterval.hi?] <;> intro h <;> subst h <;> intros <;> omega
+
 end Lean.Grind.ToInt

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

@@ -212,6 +212,7 @@ partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := caching c' do
     let ctx ← getNatContext
     let h := mkApp4 (mkConst ``Int.OfNat.of_not_le) ctx (← mkNatExprDecl lhs) (← mkNatExprDecl rhs) (mkOfEqFalseCore e (← mkEqFalseProof e))
     return mkApp6 (mkConst ``Int.Linear.not_le_norm_expr) (← getContext) (← mkExprDecl lhs') (← mkExprDecl rhs') (← mkPolyDecl c'.p) reflBoolTrue h
+  | .bound h => return h
   | .dec h =>
     return mkFVar h
   | .norm c =>
@@ -399,7 +400,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 .. | .coreToInt .. | .denoteAsIntNonneg .. => return ()
+  | .core .. | .coreNeg .. | .coreNat .. | .coreNatNeg .. | .coreToInt .. | .denoteAsIntNonneg .. | .bound .. => 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

@@ -157,10 +157,19 @@ where
     let powThm? ← mkPowThm? type u toIntInst rangeExpr
     let zeroThm? ← mkSimpleOpThm? ``Zero ``Grind.ToInt.zero_eq
     let ofNatThm? ← mkOfNatThm? type u toIntInst rangeExpr
+    let lowerThm? := if let some lo := range.lo? then
+      if lo == 0 then
+        some <| mkApp4 (mkConst ``Grind.ToInt.ge_lower0 [u]) type rangeExpr toIntInst reflBoolTrue
+      else
+        some <| mkApp5 (mkConst ``Grind.ToInt.ge_lower [u]) type rangeExpr toIntInst (toExpr lo) reflBoolTrue
+    else none
+    let upperThm? := if let some hi := range.hi? then
+      some <| mkApp5 (mkConst ``Grind.ToInt.le_upper [u]) type rangeExpr toIntInst (toExpr (-hi + 1)) reflBoolTrue
+    else none
     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?
+      subThm?, negThm?, divThm?, modThm?, powThm?, zeroThm?, ofNatThm?, lowerThm?, upperThm?
     }
 
 structure ToIntM.Context where
@@ -346,4 +355,24 @@ def isSupportedType (type : Expr) : GoalM Bool := do
   else
     return (← getToIntInfo? type).isSome
 
+/--
+Given `x` whose denotation is `e`, if `e` is of the form `ToInt a`,
+asserts its lower and upper bounds if available
+-/
+def assertToIntBounds (e : Expr) (x : Var) : GoalM Unit := do
+  let_expr Grind.ToInt.toInt α _ _ a := e | return ()
+  ToIntM.run α do
+  let info ← getInfo
+  let i := info.range
+  if let some lo := i.lo? then
+    let some thm := info.lowerThm? | unreachable!
+    let p := .add (-1) x (.num lo)
+    let c := { p, h := .bound (mkApp thm a) : LeCnstr }
+    c.assert
+  if let some hi := i.hi? then
+    let some thm := info.upperThm? | unreachable!
+    let p := .add 1 x (.num (-hi + 1))
+    let c := { p, h := .bound (mkApp thm a) : LeCnstr }
+    c.assert
+
 end Lean.Meta.Grind.Arith.Cutsat

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

@@ -69,6 +69,8 @@ structure ToIntInfo where
   powThm?   : Option Expr
   zeroThm?  : Option Expr
   ofNatThm? : Option Expr
+  lowerThm? : Option Expr
+  upperThm? : Option Expr
 
 /--
 For each term `e` of type `α` which implements the `ToInt α i` class,

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

@@ -166,6 +166,7 @@ inductive LeCnstrProof where
   | 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)
+  | bound (h : Expr)
   | dec (h : FVarId)
   | norm (c : LeCnstr)
   | divCoeffs (c : LeCnstr)

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

@@ -8,6 +8,7 @@ import Lean.Meta.IntInstTesters
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 
@@ -30,6 +31,7 @@ def mkVarImpl (expr : Expr) : GoalM Var := do
   markAsCutsatTerm expr
   assertNatCast expr var
   assertDenoteAsIntNonneg expr
+  assertToIntBounds expr var
   return var
 
 def isInt (e : Expr) : GoalM Bool := do

tests/lean/run/grind_cutsat_toint_1.lean

@@ -15,3 +15,30 @@ example (a b c : UInt32) : a < b → b < c → a < c := by
 
 example (a b c : Fin 11) : c ≤ 9 → a ≤ b → b < c → a < c + 1 := by
   grind
+
+example (a : Fin 11) : a ≤ 10 := by
+  grind
+
+example (a : Fin 11) : a ≥ 0 := by
+  grind
+
+example (a : Fin 1) : a ≥ 0 := by
+  grind
+
+example (a : Fin 1) : a ≤ 0 := by
+  grind
+
+example (a b : Fin 11) : a + b ≤ 10 := by
+  grind
+
+example (a b : Fin 11) : a + b ≥ 0 := by
+  grind
+
+example (a : UInt8) : a ≥ 0 := by
+  grind
+
+example (a : UInt8) : a ≤ 255 := by
+  grind
+
+example (a : Int8) : a ≥ -128 := by
+  grind