feat: Nat inequalities in cutsat (#7494)
This PR implements support for `Nat` inequalities in the cutsat procedure.
This commit is contained in:
Leonardo de Moura
GitHub
parent
1bbd2c183b
commit
c8aae00847
10 changed files with 172 additions and 73 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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. -/
|
||||
|
|
|
|||
|
|
@ -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 ()
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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`
|
||||
|
|
|
|||
|
|
@ -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 }
|
||||
|
|
|
|||
17
tests/lean/run/grind_cutsat_nat_le.lean
Normal file
17
tests/lean/run/grind_cutsat_nat_le.lean
Normal file
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue