From 422eb68f6fbc69d31e970b63d9f8a6363c4601a3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 27 Jun 2025 11:42:35 -0700 Subject: [PATCH] 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 | 14 +++++++++ .../Meta/Tactic/Grind/Arith/Cutsat/Proof.lean | 3 +- .../Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean | 31 ++++++++++++++++++- .../Tactic/Grind/Arith/Cutsat/ToIntInfo.lean | 2 ++ .../Meta/Tactic/Grind/Arith/Cutsat/Types.lean | 1 + .../Meta/Tactic/Grind/Arith/Cutsat/Var.lean | 2 ++ tests/lean/run/grind_cutsat_toint_1.lean | 27 ++++++++++++++++ 7 files changed, 78 insertions(+), 2 deletions(-) diff --git a/src/Init/Grind/ToIntLemmas.lean b/src/Init/Grind/ToIntLemmas.lean index 82fe35451f..4e2263db8a 100644 --- a/src/Init/Grind/ToIntLemmas.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean index 335ea5fb13..1cdc5fdd33 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean +++ b/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₂ diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean index 3059aaa4bb..591ba8373a 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.lean index 5f2da87ef3..9ee419cf3d 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.lean +++ b/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, diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean index 3706d1bda4..b5f40faae3 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean +++ b/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) diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean index 1c18398d15..6c3e95b325 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean +++ b/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 diff --git a/tests/lean/run/grind_cutsat_toint_1.lean b/tests/lean/run/grind_cutsat_toint_1.lean index 1c2e436b0e..2c33891e0c 100644 --- a/tests/lean/run/grind_cutsat_toint_1.lean +++ b/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