diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean index 2b6f9ced3d..8e66bd56d1 100644 --- a/src/Init/Data/Int/Linear.lean +++ b/src/Init/Data/Int/Linear.lean @@ -1093,7 +1093,7 @@ def OrOver (n : Nat) (p : Nat → Prop) : Prop := | 0 => False | n+1 => p n ∨ OrOver n p -theorem orOver_unsat {p} : ¬ OrOver 0 p := by simp [OrOver] +theorem orOver_one {p} : OrOver 1 p → p 0 := by simp [OrOver] theorem orOver_resolve {n p} : OrOver (n+1) p → ¬ p n → OrOver n p := by intro h₁ h₂ diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean index a3339093a0..a10d7f2fa7 100644 --- a/src/Init/Grind/Tactics.lean +++ b/src/Init/Grind/Tactics.lean @@ -69,6 +69,10 @@ structure Config where verbose : Bool := true /-- If `clean` is `true`, `grind` uses `expose_names` and only generates accessible names. -/ clean : Bool := true + /-- + If `qlia` is `true`, `grind` may generate counterexamples for integer constraints using rational numbers. + This approach is cheaper but incomplete. -/ + qlia : Bool := false deriving Inhabited, BEq end Lean.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean index 0a2505b66a..1875967600 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean @@ -53,5 +53,6 @@ builtin_initialize registerTraceClass `grind.debug.cutsat.eq builtin_initialize registerTraceClass `grind.debug.cutsat.diseq builtin_initialize registerTraceClass `grind.debug.cutsat.diseq.split builtin_initialize registerTraceClass `grind.debug.cutsat.backtrack +builtin_initialize registerTraceClass `grind.debug.cutsat.search end Lean diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Cooper.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Cooper.lean new file mode 100644 index 0000000000..72393c3a12 --- /dev/null +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Cooper.lean @@ -0,0 +1,24 @@ +/- +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 Lean.Meta.Tactic.Grind.Arith.Cutsat.Util + +namespace Lean.Meta.Grind.Arith.Cutsat + +def CooperSplit.numCases (s : CooperSplit) : Nat := + let a := s.c₁.p.leadCoeff + let b := s.c₂.p.leadCoeff + match s.c₃? with + | none => if s.left then a.natAbs else b.natAbs + | some c₃ => + let c := c₃.p.leadCoeff + let d := c₃.d + if s.left then + Int.lcm a (a * d / Int.gcd (a * d) c) + else + Int.lcm b (b * d / Int.gcd (b * d) c) + +end Lean.Meta.Grind.Arith.Cutsat diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean index 8e3a61ddc4..5588eb4b18 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ prelude import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Cooper namespace Lean.Meta.Grind.Arith.Cutsat @@ -65,6 +66,25 @@ partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := c'.caching do return mkApp10 (mkConst ``Int.Linear.eq_dvd_subst) (← getContext) (toExpr x) (toExpr c₁.p) (toExpr c₂.d) (toExpr c₂.p) (toExpr c'.d) (toExpr c'.p) reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof) + | .cooper₁ c => + let p₁ := c.c₁.p + let p₂ := c.c₂.p + match c.c₃? with + | none => + let thmName := if c.left then ``Int.Linear.cooper_left_split_dvd else ``Int.Linear.cooper_right_split_dvd + return mkApp8 (mkConst thmName) + (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c.k) (toExpr c'.d) (toExpr c'.p) (← c.toExprProof) reflBoolTrue + | some c₃ => + let thmName := if c.left then ``Int.Linear.cooper_dvd_left_split_dvd1 else ``Int.Linear.cooper_dvd_right_split_dvd1 + return mkApp10 (mkConst thmName) + (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr c.k) (toExpr c'.d) (toExpr c'.p) (← c.toExprProof) reflBoolTrue + | .cooper₂ c => + let p₁ := c.c₁.p + let p₂ := c.c₂.p + let some c₃ := c.c₃? | throwError "`grind` internal error, unexpected `cooper₂` proof" + let thmName := if c.left then ``Int.Linear.cooper_dvd_left_split_dvd2 else ``Int.Linear.cooper_dvd_right_split_dvd2 + return mkApp10 (mkConst thmName) + (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr c.k) (toExpr c'.d) (toExpr c'.p) (← c.toExprProof) reflBoolTrue partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := c'.caching do match c'.h with @@ -102,6 +122,19 @@ partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := c'.caching do let hNot := mkLambda `h .default (mkIntLE (← p₂.denoteExpr') (mkIntLit 0)) (hFalse.abstract #[mkFVar fvarId]) return mkApp7 (mkConst ``Int.Linear.diseq_split_resolve) (← getContext) (toExpr c₁.p) (toExpr p₂) (toExpr c'.p) reflBoolTrue (← c₁.toExprProof) hNot + | .cooper c => + let p₁ := c.c₁.p + let p₂ := c.c₂.p + let coeff := if c.left then p₁.leadCoeff else p₂.leadCoeff + match c.c₃? with + | none => + let thmName := if c.left then ``Int.Linear.cooper_left_split_ineq else ``Int.Linear.cooper_right_split_ineq + return mkApp8 (mkConst thmName) + (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c.k) (toExpr coeff) (toExpr c'.p) (← c.toExprProof) reflBoolTrue + | some c₃ => + let thmName := if c.left then ``Int.Linear.cooper_dvd_left_split_ineq else ``Int.Linear.cooper_dvd_right_split_ineq + return mkApp10 (mkConst thmName) + (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr c.k) (toExpr coeff) (toExpr c'.p) (← c.toExprProof) reflBoolTrue partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := c'.caching do match c'.h with @@ -121,6 +154,44 @@ partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := c'.caching (← getContext) (toExpr x) (toExpr c₁.p) (toExpr c₂.p) (toExpr c'.p) reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof) +partial def CooperSplit.toExprProof (s : CooperSplit) : ProofM Expr := caching s.id do + match s.h with + | .dec h => return mkFVar h + | .last hs _ => + let p₁ := s.c₁.p + let p₂ := s.c₂.p + let n := s.numCases + unless hs.size + 1 == n do + throwError "`grind` internal error, unexpected number of cases at `CopperSplit`" + let (base, pred) ← match s.c₃? with + | none => + let thmName := if s.left then ``Int.Linear.cooper_left else ``Int.Linear.cooper_right + let predName := if s.left then ``Int.Linear.cooper_left_split else ``Int.Linear.cooper_right_split + let base := mkApp7 (mkConst thmName) (← getContext) (toExpr p₁) (toExpr p₂) (toExpr n) + reflBoolTrue (← s.c₁.toExprProof) (← s.c₂.toExprProof) + let pred := mkApp3 (mkConst predName) (← getContext) (toExpr p₁) (toExpr p₂) + pure (base, pred) + | some c₃ => + let thmName := if s.left then ``Int.Linear.cooper_dvd_left else ``Int.Linear.cooper_dvd_right + let predName := if s.left then ``Int.Linear.cooper_dvd_left_split else ``Int.Linear.cooper_dvd_right_split + let base := mkApp10 (mkConst thmName) (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr n) + reflBoolTrue (← s.c₁.toExprProof) (← s.c₂.toExprProof) (← c₃.toExprProof) + let pred := mkApp5 (mkConst predName) (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) + pure (base, pred) + -- `pred` is an expressions of the form `cooper_*_split ...` with type `Nat → Prop` + let mut k := n + let mut result := base -- `OrOver k (cooper_*_splti) + -- `result` is of the form `OrOver k pred`, we resolve it using `hs` + for (fvarId, c) in hs do + let type := mkApp pred (toExpr (k-1)) + let h ← c.toExprProofCore -- proof of `False` + -- `hNotCase` is a proof for `¬ pred (k-1)` + let hNotCase := mkLambda `h .default type (h.abstract #[mkFVar fvarId]) + result := mkApp4 (mkConst ``Int.Linear.orOver_resolve) (toExpr k) pred result hNotCase + k := k - 1 + -- `result` is now a proof of `OrOver 1 pred` + return mkApp2 (mkConst ``Int.Linear.orOver_one) pred result + partial def UnsatProof.toExprProofCore (h : UnsatProof) : ProofM Expr := do match h with | .le c => @@ -185,9 +256,15 @@ partial def EqCnstr.collectDecVars (c' : EqCnstr) : CollectDecVarsM Unit := do u | .norm c | .divCoeffs c => c.collectDecVars | .subst _ c₁ c₂ | .ofLeGe c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars +partial def CooperSplit.collectDecVars (c' : CooperSplit) : CollectDecVarsM Unit := do unless (← alreadyVisited c'.id) do + match c'.h with + | .dec h => markAsFound h + | .last (decVars := decVars) .. => decVars.forM markAsFound + partial def DvdCnstr.collectDecVars (c' : DvdCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c'.id) do match c'.h with | .expr h => collectExpr h + | .cooper₁ c | .cooper₂ c | .norm c | .elim c | .divCoeffs c | .ofEq _ c => c.collectDecVars | .solveCombine c₁ c₂ | .solveElim c₁ c₂ | .subst _ c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars @@ -195,12 +272,9 @@ partial def LeCnstr.collectDecVars (c' : LeCnstr) : CollectDecVarsM Unit := do u match c'.h with | .expr h => collectExpr h | .notExpr .. => return () -- This kind of proof is used for connecting with the `grind` core. - | .norm c | .divCoeffs c => c.collectDecVars + | .cooper c | .norm c | .divCoeffs c => c.collectDecVars | .combine c₁ c₂ | .subst _ c₁ c₂ | .ofLeDiseq c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars - | .ofDiseqSplit _ _ _ decVars => - -- Recall that we cache the decision variables used in this kind of proof - for fvar in decVars do - markAsFound fvar + | .ofDiseqSplit (decVars := decVars) .. => decVars.forM markAsFound partial def DiseqCnstr.collectDecVars (c' : DiseqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c'.id) do match c'.h with diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean index 7cdb7f9283..1ac0d03471 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean @@ -240,10 +240,10 @@ def resolveRealLowerUpperConflict (c₁ c₂ : LeCnstr) : GoalM Bool := do return true def resolveCooperLeft (c₁ c₂ : LeCnstr) : GoalM Unit := do - throwError "Cooper-left NIY {← c₁.pp} {← c₂.pp}" + throwError "Cooper-left NIY {← c₁.pp}, {← c₂.pp}" def resolveCooperRight (c₁ c₂ : LeCnstr) : GoalM Unit := do - throwError "Cooper-right NIY {← c₁.pp} {← c₂.pp}" + throwError "Cooper-right NIY {← c₁.pp}, {← c₂.pp}" def resolveCooper (c₁ c₂ : LeCnstr) : GoalM Unit := do if c₁.p.leadCoeff.natAbs < c₂.p.leadCoeff.natAbs then @@ -252,10 +252,10 @@ def resolveCooper (c₁ c₂ : LeCnstr) : GoalM Unit := do resolveCooperRight c₁ c₂ def resolveCooperDvdLeft (c₁ c₂ : LeCnstr) (c : DvdCnstr) : GoalM Unit := do - throwError "Cooper-dvd-left NIY {← c₁.pp} {← c₂.pp} {← c.pp}" + throwError "Cooper-dvd-left NIY {← c₁.pp}, {← c₂.pp}, {← c.pp}" def resolveCooperDvdRight (c₁ c₂ : LeCnstr) (c : DvdCnstr) : GoalM Unit := do - throwError "Cooper-dvd-right NIY {← c₁.pp} {← c₂.pp} {← c.pp}" + throwError "Cooper-dvd-right NIY {← c₁.pp}, {← c₂.pp}, {← c.pp}" def resolveCooperDvd (c₁ c₂ : LeCnstr) (c : DvdCnstr) : GoalM Unit := do if c₁.p.leadCoeff.natAbs < c₂.p.leadCoeff.natAbs then @@ -264,7 +264,7 @@ def resolveCooperDvd (c₁ c₂ : LeCnstr) (c : DvdCnstr) : GoalM Unit := do resolveCooperDvdRight c₁ c₂ c def resolveCooperDiseq (c₁ : DiseqCnstr) (c₂ : LeCnstr) (_c? : Option DvdCnstr) : GoalM Unit := do - throwError "Cooper-diseq NIY {← c₁.pp} {← c₂.pp}" + throwError "Cooper-diseq NIY {← c₁.pp}, {← c₂.pp}" /-- Given `c₁` of the form `-a₁*x + p₁ ≤ 0`, and `c` of the form `b*x + p ≠ 0`, @@ -322,6 +322,7 @@ def processVar (x : Var) : SearchM Unit := do let v := dvdSol.leAvoiding upper diseqVals setAssignment x v | some (lower, c₁), some (upper, c₂) => + trace[grind.debug.cutsat.search] "{lower} ≤ {lower.ceil} ≤ {quoteIfNotAtom (← getVar x)} ≤ {upper.floor} ≤ {upper}" if lower > upper then let .true ← resolveRealLowerUpperConflict c₁ c₂ | throwError "`grind` internal error, conflict resolution failed" @@ -339,6 +340,7 @@ def processVar (x : Var) : SearchM Unit := do setAssignment x v return () if (← isApprox) then + setImprecise if lower < upper then setAssignment x <| findRatVal lower upper diseqVals else if let some c := findRatDiseq? lower diseqVals then @@ -404,9 +406,14 @@ def traceModel : GoalM Unit := do trace[grind.cutsat.model] "{quoteIfNotAtom x} := {v}" def searchAssigment : GoalM Unit := do - -- TODO: .int case - -- TODO: - searchAssigmentMain .rat |>.run' {} + let (_, s) ← searchAssigmentMain .rat |>.run {} + if (← isInconsistent) then return () + if !(← getConfig).qlia && !s.precise then + -- Search for a new model using `.int` mode. + trace[grind.debug.cutsat.search] "restart using Cooper resolution" + modify' fun s => { s with assignment := {} } + searchAssigmentMain .int |>.run' {} + if (← isInconsistent) then return () assignElimVars traceModel diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.lean index b04e5b61b4..a0e81ff204 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.lean @@ -5,9 +5,9 @@ Authors: Leonardo de Moura -/ prelude import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util +-- import Lean.Meta.Tactic.Grind.Arith.Cutsat.Cooper namespace Lean.Meta.Grind.Arith.Cutsat - /-- In principle, we only need to support two kinds of case split. - Disequalities. diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean index dd86ffab16..f6722343a0 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean @@ -93,6 +93,40 @@ structure DvdCnstr where /-- Unique id for caching proofs in `ProofM` -/ id : Nat +/-- +The predicate of type `Nat → Prop`, which serves as the conclusion of the +`cooper_left`, `cooper_right`, `cooper_dvd_left`, and `cooper_dvd_right` theorems. + +The specific predicate used is determined as follows: +- `cooper_left_split` (if `left` is `true` and `c₃?` is `none`) +- `cooper_right_split` (if `left` is `false` and `c₃?` is `none`) +- `cooper_dvd_left_split` (if `left` is `true` and `c₃?` is `some`) +- `cooper_dvd_right_split` (if `left` is `false` and `c₃?` is `some`) + +See `CooperSplitProof` for additional explanations. +-/ +structure CooperSplit where + left : Bool + c₁ : LeCnstr + c₂ : LeCnstr + c₃? : Option DvdCnstr + k : Nat + h : CooperSplitProof + id : Nat + +/-- +The `cooper_left`, `cooper_right`, `cooper_dvd_left`, and `cooper_dvd_right` theorems have a resulting type +that is a big-or of the form `OrOver n (cooper_*_split ...)`. The predicate `(cooper_*_split ...)` has type `Nat → Prop`. +The `cutsat` procedure performs case splitting on `(cooper_*_split ... (n-1))` down to `(cooper_*_split ... 1)`. +If it derives `False` from each case, it uses `orOver_resolve` and `orOver_one` to deduce the final case, +which has type `(cooper_*_split ... 0)`. +-/ +inductive CooperSplitProof where + | /-- The first `n-1` cases are decisions (aka case-splits). -/ + dec (h : FVarId) + | /-- The last case which has type `(cooper_*_split ... 0)` -/ + last (hs : Array (FVarId × UnsatProof)) (decVars : Array FVarId) + inductive DvdCnstrProof where | expr (h : Expr) | norm (c : DvdCnstr) @@ -102,8 +136,11 @@ inductive DvdCnstrProof where | elim (c : DvdCnstr) | ofEq (x : Var) (c : EqCnstr) | subst (x : Var) (c₁ : EqCnstr) (c₂ : DvdCnstr) + | cooper₁ (c : CooperSplit) + /-- `c.c₃?` must be `some` -/ + | cooper₂ (c : CooperSplit) -/-- An inequality constraint and its justification/proof. -/ +/-- An inequalirty constraint and its justification/proof. -/ structure LeCnstr where p : Poly h : LeCnstrProof @@ -118,6 +155,8 @@ inductive LeCnstrProof where | subst (x : Var) (c₁ : EqCnstr) (c₂ : LeCnstr) | ofLeDiseq (c₁ : LeCnstr) (c₂ : DiseqCnstr) | ofDiseqSplit (c₁ : DiseqCnstr) (decVar : FVarId) (h : UnsatProof) (decVars : Array FVarId) + | cooper (c : CooperSplit) + -- TODO: missing constructors /-- A disequality constraint and its justification/proof. -/ @@ -146,6 +185,9 @@ inductive UnsatProof where end +instance : Inhabited LeCnstr where + default := { p := .num 0, h := .expr default, id := 0 } + instance : Inhabited DvdCnstr where default := { d := 0, p := .num 0, h := .expr default, id := 0 }