From c8aae00847d34d63c123ef53bb3920ad31bd07e4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 14 Mar 2025 17:43:18 -0700 Subject: [PATCH] feat: `Nat` inequalities in cutsat (#7494) This PR implements support for `Nat` inequalities in the cutsat procedure. --- src/Init/Data/Int/Linear.lean | 16 +++ src/Init/Data/Int/OfNat.lean | 9 ++ .../Tactic/Grind/Arith/Cutsat/DvdCnstr.lean | 2 +- .../Tactic/Grind/Arith/Cutsat/EqCnstr.lean | 14 +- .../Tactic/Grind/Arith/Cutsat/LeCnstr.lean | 21 +-- .../Meta/Tactic/Grind/Arith/Cutsat/Nat.lean | 10 +- .../Meta/Tactic/Grind/Arith/Cutsat/Proof.lean | 122 ++++++++++++------ .../Tactic/Grind/Arith/Cutsat/Search.lean | 2 +- .../Meta/Tactic/Grind/Arith/Cutsat/Types.lean | 32 +++-- tests/lean/run/grind_cutsat_nat_le.lean | 17 +++ 10 files changed, 172 insertions(+), 73 deletions(-) create mode 100644 tests/lean/run/grind_cutsat_nat_le.lean diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean index 00cf6dbb1f..1679cddc19 100644 --- a/src/Init/Data/Int/Linear.lean +++ b/src/Init/Data/Int/Linear.lean @@ -1737,6 +1737,22 @@ theorem dvd_neg_le_tight (ctx : Context) (d : Int) (p₁ p₂ p₃ : Poly) intro h₁ h₂; rw [Int.add_comm] at h₁ exact dvd_le_tight' hd h₂ h₁ +theorem le_norm_expr (ctx : Context) (lhs rhs : Expr) (p : Poly) + : norm_eq_cert lhs rhs p → lhs.denote ctx ≤ rhs.denote ctx → p.denote' ctx ≤ 0 := by + intro h₁ h₂; rwa [norm_le ctx lhs rhs p h₁] at h₂ + +def not_le_norm_expr_cert (lhs rhs : Expr) (p : Poly) : Bool := + p == (((lhs.sub rhs).norm).mul (-1)).addConst 1 + +theorem not_le_norm_expr (ctx : Context) (lhs rhs : Expr) (p : Poly) + : not_le_norm_expr_cert lhs rhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → p.denote' ctx ≤ 0 := by + simp [not_le_norm_expr_cert] + intro; subst p; simp + intro h + replace h := Int.sub_nonpos_of_le h + rw [Int.add_comm, Int.add_sub_assoc] at h + rw [Int.neg_sub]; assumption + end Int.Linear theorem Int.not_le_eq (a b : Int) : (¬a ≤ b) = (b + 1 ≤ a) := by diff --git a/src/Init/Data/Int/OfNat.lean b/src/Init/Data/Int/OfNat.lean index 80cb8fd0bd..9b8dc217a7 100644 --- a/src/Init/Data/Int/OfNat.lean +++ b/src/Init/Data/Int/OfNat.lean @@ -26,6 +26,7 @@ inductive Expr where | mul (a b : Expr) | div (a b : Expr) | mod (a b : Expr) + deriving BEq def Expr.denote (ctx : Context) : Expr → Nat | .num k => k @@ -58,4 +59,12 @@ theorem Expr.dvd (ctx : Context) (lhs rhs : Expr) : (lhs.denote ctx ∣ rhs.denote ctx) = (lhs.denoteAsInt ctx ∣ rhs.denoteAsInt ctx) := by simp [denoteAsInt_eq, Int.ofNat_dvd] +theorem of_nat_le (ctx : Context) (lhs rhs : Expr) + : lhs.denote ctx ≤ rhs.denote ctx → lhs.denoteAsInt ctx ≤ rhs.denoteAsInt ctx := by + rw [Expr.le ctx lhs rhs]; simp + +theorem of_not_nat_le (ctx : Context) (lhs rhs : Expr) + : ¬ lhs.denote ctx ≤ rhs.denote ctx → ¬ lhs.denoteAsInt ctx ≤ rhs.denoteAsInt ctx := by + rw [Expr.le ctx lhs rhs]; simp + end Int.OfNat diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean index b1e6ee1270..2fad9d733b 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean @@ -95,7 +95,7 @@ builtin_grind_propagator propagateDvd ↓Dvd.dvd := fun e => do return () if (← isEqTrue e) then let p ← toPoly b - let c := { d, p, h := .expr (← mkOfEqTrue (← mkEqTrueProof e)) : DvdCnstr } + let c := { d, p, h := .core e : DvdCnstr } trace[grind.cutsat.assert.dvd] "{← c.pp}" c.assert else if (← isEqFalse e) then diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean index 41454c0911..6c4dcc08b7 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import Lean.Meta.Tactic.Grind.Diseq import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr @@ -241,34 +240,31 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do let p₁ ← exprAsPoly a let p₂ ← exprAsPoly b let p := p₁.combine (p₂.mul (-1)) - { p, h := .core p₁ p₂ (← mkEqProof a b) : EqCnstr }.assert + { p, h := .core a b p₁ p₂ : EqCnstr }.assert @[export lean_process_cutsat_eq_lit] def processNewEqLitImpl (a ke : Expr) : GoalM Unit := do trace[grind.debug.cutsat.eq] "{a} = {ke}" let some k ← getIntValue? ke | return () let p₁ ← exprAsPoly a - let h ← mkEqProof a ke let c ← if k == 0 then - pure { p := p₁, h := .expr h : EqCnstr } + pure { p := p₁, h := .core0 a ke : EqCnstr } else let p₂ ← exprAsPoly ke let p := p₁.combine (p₂.mul (-1)) - pure { p, h := .core p₁ p₂ h : EqCnstr } + pure { p, h := .core a ke p₁ p₂ : EqCnstr } c.assert @[export lean_process_cutsat_diseq] def processNewDiseqImpl (a b : Expr) : GoalM Unit := do trace[grind.debug.cutsat.diseq] "{a} ≠ {b}" let p₁ ← exprAsPoly a - let some h ← mkDiseqProof? a b - | throwError "internal `grind` error, failed to build disequality proof for{indentExpr a}\nand{indentExpr b}" let c ← if let some 0 ← getIntValue? b then - pure { p := p₁, h := .expr h : DiseqCnstr } + pure { p := p₁, h := .core0 a b : DiseqCnstr } else let p₂ ← exprAsPoly b let p := p₁.combine (p₂.mul (-1)) - pure {p, h := .core p₁ p₂ h : DiseqCnstr } + pure {p, h := .core a b p₁ p₂ : DiseqCnstr } c.assert /-- Different kinds of terms internalized by this module. -/ diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean index 6e3d6f2b55..2931c99e81 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean @@ -141,22 +141,25 @@ integer inequality, asserts it to the cutsat state. def propagateIntLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do let some p ← toPolyLe? e | return () let c ← if eqTrue then - pure { p, h := .expr (← mkOfEqTrue (← mkEqTrueProof e)) : LeCnstr } + pure { p, h := .core e : LeCnstr } else - pure { p := p.mul (-1) |>.addConst 1, h := .notExpr p (← mkOfEqFalse (← mkEqFalseProof e)) : LeCnstr } + pure { p := p.mul (-1) |>.addConst 1, h := .coreNeg e p : LeCnstr } trace[grind.cutsat.assert.le] "{← c.pp}" c.assert -def propagateNatLe (e : Expr) (_eqTrue : Bool) : GoalM Unit := do - let some (lhs, rhs, _h) ← Int.OfNat.toIntLe? e | return () +def propagateNatLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do + let some (lhs, rhs, ctx) ← Int.OfNat.toIntLe? e | return () let gen ← getGeneration e - let lhs' ← toLinearExpr lhs gen - let rhs' ← toLinearExpr rhs gen + let lhs' ← toLinearExpr (lhs.denoteAsIntExpr ctx) gen + let rhs' ← toLinearExpr (rhs.denoteAsIntExpr ctx) gen let p := lhs'.sub rhs' |>.norm - trace[grind.debug.cutsat.nat] "{lhs} ≤ {rhs}" trace[grind.debug.cutsat.nat] "{← p.pp}" - -- TODO: WIP - return () + let c ← if eqTrue then + pure { p, h := .coreNat e ctx lhs rhs lhs' rhs' : LeCnstr } + else + pure { p := p.mul (-1) |>.addConst 1, h := .coreNatNeg e ctx lhs rhs lhs' rhs' : LeCnstr } + trace[grind.cutsat.assert.le] "{← c.pp}" + c.assert def propagateIfSupportedLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do let_expr LE.le α _ _ _ := e | return () diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean index ef1e5c26fc..a27b354b4b 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean @@ -74,17 +74,13 @@ partial def toOfNatExpr (e : Lean.Expr) : M Expr := do /-- Given `e` of the form `lhs ≤ rhs` where `lhs` and `rhs` have type `Nat`, -returns `(lhs', rhs', h)` where `lhs'` and `rhs'` are integer expressions and `h` is a proof -that `(lhs ≤ rhs) = (lhs', rhs')` +returns `(lhs, rhs, ctx)` where `lhs` and `rhs` are `Int.OfNat.Expr` and `ctx` is the context. -/ -def toIntLe? (e : Lean.Expr) : MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr)) := do +def toIntLe? (e : Lean.Expr) : MetaM (Option (Expr × Expr × Array Lean.Expr)) := do let_expr LE.le _ inst lhs rhs := e | return none unless (← isInstLENat inst) do return none let ((lhs, rhs), s) ← conv lhs rhs |>.run {} - let lhs' := lhs.denoteAsIntExpr s.ctx - let rhs' := rhs.denoteAsIntExpr s.ctx - let h := mkApp3 (mkConst ``Int.OfNat.Expr.le) (Simp.Arith.Nat.toContextExpr s.ctx) (toExpr lhs) (toExpr rhs) - return some (lhs', rhs', h) + return some (lhs, rhs, s.ctx) where conv (lhs rhs : Lean.Expr) : M (Expr × Expr) := return (← toOfNatExpr lhs, ← toOfNatExpr rhs) diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean index e637355f43..213656803b 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean @@ -4,13 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude +import Lean.Meta.Tactic.Grind.Diseq import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat namespace Lean.Meta.Grind.Arith.Cutsat +deriving instance Hashable for Int.Linear.Expr +deriving instance Hashable for Int.OfNat.Expr + structure ProofM.State where cache : Std.HashMap UInt64 Expr := {} polyMap : Std.HashMap Poly Expr := {} + natCtxMap : Std.HashMap (Array Expr) Expr := {} + exprMap : Std.HashMap Int.Linear.Expr Expr := {} + natExprMap : Std.HashMap Int.OfNat.Expr Expr := {} /-- Auxiliary monad for constructing cutsat proofs. -/ abbrev ProofM := ReaderT Expr (StateRefT ProofM.State GoalM) @@ -29,27 +37,61 @@ abbrev caching (c : α) (k : ProofM Expr) : ProofM Expr := do return h def mkPolyDecl (p : Poly) : ProofM Expr := do - if let some e := (← get).polyMap[p]? then - return e + if let some x := (← get).polyMap[p]? then + return x let x := mkFVar (← mkFreshFVarId) - modify fun s => { s with - polyMap := s.polyMap.insert p x - } + modify fun s => { s with polyMap := s.polyMap.insert p x } return x +def mkNatCtxDecl (ctx : Array Expr) : ProofM Expr := do + if let some x := (← get).natCtxMap[ctx]? then + return x + let x := mkFVar (← mkFreshFVarId) + modify fun s => { s with natCtxMap := s.natCtxMap.insert ctx x } + return x + +def mkExprDecl (e : Int.Linear.Expr) : ProofM Expr := do + if let some x := (← get).exprMap[e]? then + return x + let x := mkFVar (← mkFreshFVarId) + modify fun s => { s with exprMap := s.exprMap.insert e x } + return x + +def mkNatExprDecl (e : Int.OfNat.Expr) : ProofM Expr := do + if let some x := (← get).natExprMap[e]? then + return x + let x := mkFVar (← mkFreshFVarId) + modify fun s => { s with natExprMap := s.natExprMap.insert e x } + return x + +private def mkDiseqProof (a b : Expr) : GoalM Expr := do + let some h ← mkDiseqProof? a b + | throwError "internal `grind` error, failed to build disequality proof for{indentExpr a}\nand{indentExpr b}" + return h + +private def mkLetOfMap {_ : Hashable α} {_ : BEq α} (m : Std.HashMap α Expr) (e : Expr) + (varPrefix : Name) (varType : Expr) (toExpr : α → Expr) : GoalM Expr := do + if m.isEmpty then + return e + else + let as := m.toArray + let mut e := e.abstract <| as.map (·.2) + let mut i := as.size + for (p, _) in as.reverse do + e := mkLet (varPrefix.appendIndexAfter i) varType (toExpr p) e + i := i - 1 + return e + abbrev withProofContext (x : ProofM Expr) : GoalM Expr := do withLetDecl `ctx (mkApp (mkConst ``RArray) (mkConst ``Int)) (← toContextExpr) fun ctx => do go ctx |>.run' {} where go : ProofM Expr := do - let mut h ← x - let ps := (← get).polyMap.toArray - h := h.abstract <| ps.map (·.2) - let polyType := mkConst ``Int.Linear.Poly - let mut i := ps.size - for (p, _) in ps.reverse do - h := mkLet ((`p).appendIndexAfter i) polyType (toExpr p) h - i := i - 1 + let h ← x + let h ← mkLetOfMap (← get).polyMap h `p (mkConst ``Int.Linear.Poly) toExpr + let h ← mkLetOfMap (← get).exprMap h `e (mkConst ``Int.Linear.Expr) toExpr + let h ← mkLetOfMap (← get).natExprMap h `a (mkConst ``Int.OfNat.Expr) toExpr + let h ← mkLetOfMap (← get).natCtxMap h `nctx (mkApp (mkConst ``Lean.RArray) (mkConst ``Nat)) Simp.Arith.Nat.toContextExpr let ctx ← read mkLetFVars #[ctx] h @@ -62,9 +104,10 @@ mutual partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := caching c' do trace[grind.debug.cutsat.proof] "{← c'.pp}" match c'.h with - | .expr h => - return h - | .core p₁ p₂ h => + | .core0 a zero => + mkEqProof a zero + | .core a b p₁ p₂ => + let h ← mkEqProof a b return mkApp6 (mkConst ``Int.Linear.eq_of_core) (← getContext) (← mkPolyDecl p₁) (← mkPolyDecl p₂) (← mkPolyDecl c'.p) reflBoolTrue h | .norm c => return mkApp5 (mkConst ``Int.Linear.eq_norm) (← getContext) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) reflBoolTrue (← c.toExprProof) @@ -83,8 +126,8 @@ partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := caching c' do partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := caching c' do trace[grind.debug.cutsat.proof] "{← c'.pp}" match c'.h with - | .expr h => - return h + | .core e => + mkOfEqTrue (← mkEqTrueProof e) | .norm c => return mkApp6 (mkConst ``Int.Linear.dvd_norm) (← getContext) (toExpr c.d) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) reflBoolTrue (← c.toExprProof) | .elim c => @@ -140,15 +183,26 @@ partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := caching c' do partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := caching c' do trace[grind.debug.cutsat.proof] "{← c'.pp}" match c'.h with - | .expr h => - return h + | .core e => + mkOfEqTrue (← mkEqTrueProof e) + | .coreNeg e p => + let h ← mkOfEqFalse (← mkEqFalseProof e) + return mkApp5 (mkConst ``Int.Linear.le_neg) (← getContext) (← mkPolyDecl p) (← mkPolyDecl c'.p) reflBoolTrue h + | .coreNat e ctx lhs rhs lhs' rhs' => + let ctx ← mkNatCtxDecl ctx + let h := mkApp4 (mkConst ``Int.OfNat.of_nat_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 + | .coreNatNeg e ctx lhs rhs lhs' rhs' => + let ctx ← mkNatCtxDecl ctx + let h := mkApp4 (mkConst ``Int.OfNat.of_not_nat_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 + | .dec h => + return mkFVar h | .norm c => return mkApp5 (mkConst ``Int.Linear.le_norm) (← getContext) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) reflBoolTrue (← c.toExprProof) | .divCoeffs c => let k := c.p.gcdCoeffs' return mkApp6 (mkConst ``Int.Linear.le_coeff) (← getContext) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) (toExpr (Int.ofNat k)) reflBoolTrue (← c.toExprProof) - | .notExpr p h => - return mkApp5 (mkConst ``Int.Linear.le_neg) (← getContext) (← mkPolyDecl p) (← mkPolyDecl c'.p) reflBoolTrue h | .combine c₁ c₂ => return mkApp7 (mkConst ``Int.Linear.le_combine) (← getContext) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c'.p) @@ -205,9 +259,10 @@ partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := caching c' do partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := caching c' do trace[grind.debug.cutsat.proof] "{← c'.pp}" match c'.h with - | .expr h => - return h - | .core p₁ p₂ h => + | .core0 a zero => + mkDiseqProof a zero + | .core a b p₁ p₂ => + let h ← mkDiseqProof a b return mkApp6 (mkConst ``Int.Linear.diseq_of_core) (← getContext) (← mkPolyDecl p₁) (← mkPolyDecl p₂) (← mkPolyDecl c'.p) reflBoolTrue h | .norm c => return mkApp5 (mkConst ``Int.Linear.diseq_norm) (← getContext) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) reflBoolTrue (← c.toExprProof) @@ -316,16 +371,10 @@ private def alreadyVisited (c : α) : CollectDecVarsM Bool := do private def markAsFound (fvarId : FVarId) : CollectDecVarsM Unit := do modify fun s => { s with found := s.found.insert fvarId } -private def collectExpr (e : Expr) : CollectDecVarsM Unit := do - let .fvar fvarId := e | return () - if (← read).contains fvarId then - markAsFound fvarId - mutual partial def EqCnstr.collectDecVars (c' : EqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do match c'.h with - | .expr h => collectExpr h - | .core .. => return () -- Equalities coming from the core never contain cutsat decision variables + | .core0 .. | .core .. => return () -- Equalities coming from the core never contain cutsat decision variables | .norm c | .divCoeffs c => c.collectDecVars | .subst _ c₁ c₂ | .ofLeGe c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars @@ -340,15 +389,15 @@ partial def CooperSplit.collectDecVars (s : CooperSplit) : CollectDecVarsM Unit partial def DvdCnstr.collectDecVars (c' : DvdCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do match c'.h with - | .expr h => collectExpr h + | .core _ => return () | .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 partial def LeCnstr.collectDecVars (c' : LeCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do match c'.h with - | .expr h => collectExpr h - | .notExpr .. => return () -- This kind of proof is used for connecting with the `grind` core. + | .core .. | .coreNeg .. | .coreNat .. | .coreNatNeg .. => return () + | .dec h => markAsFound h | .cooper c | .norm c | .divCoeffs c => c.collectDecVars | .dvdTight c₁ c₂ | .negDvdTight c₁ c₂ | .combine c₁ c₂ | .combineDivCoeffs c₁ c₂ _ @@ -357,8 +406,7 @@ partial def LeCnstr.collectDecVars (c' : LeCnstr) : CollectDecVarsM Unit := do u partial def DiseqCnstr.collectDecVars (c' : DiseqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do match c'.h with - | .expr h => collectExpr h - | .core .. => return () -- Disequalities coming from the core never contain cutsat decision variables + | .core0 .. | .core .. => return () -- Disequalities coming from the core never contain cutsat decision variables | .norm c | .divCoeffs c | .neg c => c.collectDecVars | .subst _ c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean index f80c60358d..8ab5a227f7 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean @@ -355,7 +355,7 @@ def DiseqCnstr.split (c : DiseqCnstr) : SearchM LeCnstr := do modify' fun s => { s with diseqSplits := s.diseqSplits.insert c.p fvarId } pure fvarId let p₂ := c.p.addConst 1 - return { p := p₂, h := .expr (mkFVar fvarId) } + return { p := p₂, h := .dec fvarId } /-- Given `c₁` of the form `a₁*x + p₁ ≠ 0`, and `c₂` of the form `b*x + p ≤ 0` diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean index e7fb274a36..f37f42f451 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean @@ -77,8 +77,13 @@ structure EqCnstr where h : EqCnstrProof inductive EqCnstrProof where - | expr (h : Expr) - | core (p₁ p₂ : Poly) (h : Expr) + | /-- An equality `a = 0` coming from the core. -/ + core0 (a : Expr) (zero : Expr) + | /-- + An equality `a = b` coming from the core. + `p₁` and `p₂` are the polynomials corresponding to `a` and `b`. + -/ + core (a b : Expr) (p₁ p₂ : Poly) | norm (c : EqCnstr) | divCoeffs (c : EqCnstr) | subst (x : Var) (c₁ : EqCnstr) (c₂ : EqCnstr) @@ -130,7 +135,8 @@ inductive CooperSplitProof where last (hs : Array (FVarId × UnsatProof)) (decVars : Array FVarId) inductive DvdCnstrProof where - | expr (h : Expr) + | /-- Given `e` of the form `k ∣ p` s.t. `e = True` in the core. -/ + core (e : Expr) | norm (c : DvdCnstr) | divCoeffs (c : DvdCnstr) | solveCombine (c₁ c₂ : DvdCnstr) @@ -148,8 +154,11 @@ structure LeCnstr where h : LeCnstrProof inductive LeCnstrProof where - | expr (h : Expr) - | notExpr (p : Poly) (h : Expr) + | core (e : Expr) + | coreNeg (e : Expr) (p : Poly) + | coreNat (e : Expr) (ctx : Array Expr) (lhs rhs : Int.OfNat.Expr) (lhs' rhs' : Int.Linear.Expr) + | coreNatNeg (e : Expr) (ctx : Array Expr) (lhs rhs : Int.OfNat.Expr) (lhs' rhs' : Int.Linear.Expr) + | dec (h : FVarId) | norm (c : LeCnstr) | divCoeffs (c : LeCnstr) | combine (c₁ c₂ : LeCnstr) @@ -167,8 +176,13 @@ structure DiseqCnstr where h : DiseqCnstrProof inductive DiseqCnstrProof where - | expr (h : Expr) - | core (p₁ p₂ : Poly) (h : Expr) + | /-- An disequality `a != 0` coming from the core. That is, `(a = 0) = False` in the core. -/ + core0 (a : Expr) (zero : Expr) + | /-- + An disequality `a ≠ b` coming from the core. That is, `(a = b) = False` in the core. + `p₁` and `p₂` are the polynomials corresponding to `a` and `b`. + -/ + core (a b : Expr) (p₁ p₂ : Poly) | norm (c : DiseqCnstr) | divCoeffs (c : DiseqCnstr) | neg (c : DiseqCnstr) @@ -188,10 +202,10 @@ inductive UnsatProof where end instance : Inhabited LeCnstr where - default := { p := .num 0, h := .expr default } + default := { p := .num 0, h := .core default} instance : Inhabited DvdCnstr where - default := { d := 0, p := .num 0, h := .expr default } + default := { d := 0, p := .num 0, h := .core default } instance : Inhabited CooperSplitPred where default := { left := false, c₁ := default, c₂ := default, c₃? := none } diff --git a/tests/lean/run/grind_cutsat_nat_le.lean b/tests/lean/run/grind_cutsat_nat_le.lean new file mode 100644 index 0000000000..c1c8b9643b --- /dev/null +++ b/tests/lean/run/grind_cutsat_nat_le.lean @@ -0,0 +1,17 @@ +set_option grind.warning false + +theorem ex1 (x y z : Nat) : x < y + z → y + 1 < z → z + x < 3*z := by + grind + +theorem ex2 {p : Prop} (x y z : Nat) : x < y + z → y + 1 < z → (p ↔ z + x < 3*z) → p := by + grind + +theorem ex3 (x y : Nat) : + 27 ≤ 13*x + 11*y → 13*x + 11*y ≤ 30 → + 7*y ≤ 9*x + 10 → 9*x ≤ 4 + 7*y → False := by + grind + +open Int.Linear Int.OfNat +#print ex1 +#print ex2 +#print ex3