Documentation

Lean.Meta.Tactic.Grind.Arith.Cutsat.Util

def Int.Linear.Poly.isZero :

Equations

(Int.Linear.Poly.num 0).isZero = true
x✝.isZero = false

def Int.Linear.Poly.isSorted (p : Poly) :

Returns true if the variables in the given polynomial are sorted in decreasing order.

Equations

p.isSorted = Int.Linear.Poly.isSorted.go none p

def Int.Linear.Poly.isSorted.go :

Option Var → Poly → Bool

Equations

Int.Linear.Poly.isSorted.go x✝ (Int.Linear.Poly.num k) = true
Int.Linear.Poly.isSorted.go none (Int.Linear.Poly.add k y p) = Int.Linear.Poly.isSorted.go (some y) p
Int.Linear.Poly.isSorted.go (some x_2) (Int.Linear.Poly.add k y p) = (decide (x_2 > y) && Int.Linear.Poly.isSorted.go (some y) p)

partial def Lean.Meta.Grind.Arith.Cutsat.gcdExt (a b : Int) :

Int × Int × Int

gcdExt a b returns the triple (g, α, β) such that

g = gcd a b (with g ≥ 0), and
g = α * a + β * β.

def Lean.Meta.Grind.Arith.Cutsat.get' :

Equations

Lean.Meta.Grind.Arith.Cutsat.get' = do let __do_lift ← get pure __do_lift.arith.cutsat

@[inline]

def Lean.Meta.Grind.Arith.Cutsat.modify' (f : State → State) :

Equations

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.Cutsat.inconsistent :

Returns true if the cutsat state is inconsistent.

Equations

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.Cutsat.getVars :

GoalM (PArray Expr)

Equations

Lean.Meta.Grind.Arith.Cutsat.getVars = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.get' pure __do_lift.vars

def Lean.Meta.Grind.Arith.Cutsat.getVar (x : Var) :

Equations

Lean.Meta.Grind.Arith.Cutsat.getVar x = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.get' pure __do_lift.vars[x]!

def Lean.Meta.Grind.Arith.Cutsat.eliminated (x : Var) :

Returns true if x has been eliminated using an equality constraint.

Equations

Lean.Meta.Grind.Arith.Cutsat.eliminated x = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.get' pure __do_lift.elimEqs[x]!.isSome

def Lean.Meta.Grind.Arith.Cutsat.mkCnstrId :

Equations

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.Cutsat.mkEqCnstr (p : Poly) (h : EqCnstrProof) :

Equations

Lean.Meta.Grind.Arith.Cutsat.mkEqCnstr p h = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.mkCnstrId pure { p := p, h := h, id := __do_lift }

@[extern lean_grind_cutsat_assert_eq]

opaque Lean.Meta.Grind.Arith.Cutsat.EqCnstr.assert (c : EqCnstr) :

partial def Lean.Meta.Grind.Arith.Cutsat.shrink (a : PArray Rat) (sz : Nat) :

def Lean.Meta.Grind.Arith.Cutsat.resize (a : PArray Rat) (sz : Nat) :

Equations

Lean.Meta.Grind.Arith.Cutsat.resize a sz = if a.size > sz then Lean.Meta.Grind.Arith.Cutsat.shrink a sz else Lean.Meta.Grind.Arith.Cutsat.resize.go sz a

partial def Lean.Meta.Grind.Arith.Cutsat.resize.go (sz : Nat) (a : PArray Rat) :

def Lean.Meta.Grind.Arith.Cutsat.resetAssignmentFrom (x : Var) :

Resets the assingment of any variable bigger or equal to x.

Equations

One or more equations did not get rendered due to their size.

def Int.Linear.Poly.pp (p : Poly) :

Lean.Meta.Grind.GoalM Lean.MessageData

Equations

One or more equations did not get rendered due to their size.
(Int.Linear.Poly.num k).pp = pure (Lean.toMessageData "" ++ Lean.toMessageData k ++ Lean.toMessageData "")
(Int.Linear.Poly.add 1 x p_2).pp = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.getVar x Int.Linear.Poly.pp.go (Lean.quoteIfNotAtom __do_lift) p_2

def Int.Linear.Poly.pp.go (r : Lean.MessageData) (p : Poly) :

Lean.Meta.Grind.GoalM Lean.MessageData

Equations

One or more equations did not get rendered due to their size.
Int.Linear.Poly.pp.go r (Int.Linear.Poly.num 0) = pure r
Int.Linear.Poly.pp.go r (Int.Linear.Poly.num k) = pure (Lean.toMessageData "" ++ Lean.toMessageData r ++ Lean.toMessageData " + " ++ Lean.toMessageData k ++ Lean.toMessageData "")

def Int.Linear.Poly.denoteExpr' (p : Poly) :

Lean.Meta.Grind.GoalM Lean.Expr

Equations

p.denoteExpr' = do let vars ← Lean.Meta.Grind.Arith.Cutsat.getVars let __do_lift ← liftM (Int.Linear.Poly.denoteExpr (fun (x : Nat) => vars[x]!) p) pure __do_lift

def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.isTrivial (c : DvdCnstr) :

Equations

c.isTrivial = match c.p with | Int.Linear.Poly.num k' => k' % c.d == 0 | x => c.d == 1

def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.pp (c : DvdCnstr) :

GoalM MessageData

Equations

c.pp = do let __do_lift ← c.p.pp pure (Lean.toMessageData "" ++ Lean.toMessageData c.d ++ Lean.toMessageData " ∣ " ++ Lean.toMessageData __do_lift ++ Lean.toMessageData "")

def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.denoteExpr (c : DvdCnstr) :

Equations

c.denoteExpr = do let __do_lift ← c.p.denoteExpr' pure (Lean.mkIntDvd (Lean.toExpr c.d) __do_lift)

def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.throwUnexpected {α : Type} (c : DvdCnstr) :

Equations

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.isTrivial (c : DiseqCnstr) :

Equations

c.isTrivial = match c.p with | Int.Linear.Poly.num k => k != 0 | x => c.p.getConst % ↑c.p.gcdCoeffs' != 0

def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.pp (c : DiseqCnstr) :

GoalM MessageData

Equations

c.pp = do let __do_lift ← c.p.pp pure (Lean.toMessageData "" ++ Lean.toMessageData __do_lift ++ Lean.toMessageData " ≠ 0")

def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.throwUnexpected {α : Type} (c : DiseqCnstr) :

Equations

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.denoteExpr (c : DiseqCnstr) :

Equations

c.denoteExpr = do let __do_lift ← c.p.denoteExpr' pure (Lean.mkNot (Lean.mkIntEq __do_lift (Lean.mkIntLit 0)))

def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.isTrivial (c : LeCnstr) :

Equations

c.isTrivial = match c.p with | Int.Linear.Poly.num k => decide (k ≤ 0) | x => false

def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.pp (c : LeCnstr) :

GoalM MessageData

Equations

c.pp = do let __do_lift ← c.p.pp pure (Lean.toMessageData "" ++ Lean.toMessageData __do_lift ++ Lean.toMessageData " ≤ 0")

def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.denoteExpr (c : LeCnstr) :

Equations

c.denoteExpr = do let __do_lift ← c.p.denoteExpr' pure (Lean.mkIntLE __do_lift (Lean.mkIntLit 0))

def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.throwUnexpected {α : Type} (c : LeCnstr) :

Equations

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.isTrivial (c : EqCnstr) :

Equations

c.isTrivial = match c.p with | Int.Linear.Poly.num k => k == 0 | x => false

def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.pp (c : EqCnstr) :

GoalM MessageData

Equations

c.pp = do let __do_lift ← c.p.pp pure (Lean.toMessageData "" ++ Lean.toMessageData __do_lift ++ Lean.toMessageData " = 0")

def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.denoteExpr (c : EqCnstr) :

Equations

c.denoteExpr = do let __do_lift ← c.p.denoteExpr' pure (Lean.mkIntEq __do_lift (Lean.mkIntLit 0))

def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.throwUnexpected {α : Type} (c : EqCnstr) :

Equations

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.Cutsat.getOccursOf (x : Var) :

Returns occurrences of x.

Equations

Lean.Meta.Grind.Arith.Cutsat.getOccursOf x = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.get' pure __do_lift.occurs[x]!

def Lean.Meta.Grind.Arith.Cutsat.addOcc (x y : Var) :

Adds y as an occurrence of x. That is, x occurs in lowers[y], uppers[y], or dvdCnstrs[y].

Equations

One or more equations did not get rendered due to their size.

def Int.Linear.Poly.updateOccs (p : Poly) :

Lean.Meta.Grind.GoalM Unit

Given p a polynomial being inserted into lowers, uppers, or dvdCnstrs, get its leading variable y, and adds y as an occurrence for the remaining variables in p.

Equations

(Int.Linear.Poly.add k x p_2).updateOccs = Int.Linear.Poly.updateOccs.go x p_2
p.updateOccs = Lean.throwError (Lean.toMessageData "`grind` internal error, unexpected constant polynomial")

partial def Int.Linear.Poly.updateOccs.go (y : Var) (p : Poly) :

Lean.Meta.Grind.GoalM Unit

def Lean.Meta.Grind.Arith.Cutsat.toContextExpr :

Equations

One or more equations did not get rendered due to their size.

structure Lean.Meta.Grind.Arith.Cutsat.ProofM.State :

cache : Std.HashMap Nat Expr

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.ProofM (α : Type) :

Auxiliary monad for constructing cutsat proofs.

Equations

Lean.Meta.Grind.Arith.Cutsat.ProofM = ReaderT Lean.Expr (StateRefT' IO.RealWorld Lean.Meta.Grind.Arith.Cutsat.ProofM.State Lean.Meta.Grind.GoalM)

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.getContext :

Returns a Lean expression representing the variable context used to construct cutsat proofs.

Equations

Lean.Meta.Grind.Arith.Cutsat.getContext = read

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.caching (id : Nat) (k : ProofM Expr) :

Equations

One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.caching (c : DvdCnstr) (k : ProofM Expr) :

Equations

c.caching k = Lean.Meta.Grind.Arith.Cutsat.caching c.id k

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.LeCnstr.caching (c : LeCnstr) (k : ProofM Expr) :

Equations

c.caching k = Lean.Meta.Grind.Arith.Cutsat.caching c.id k

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.EqCnstr.caching (c : EqCnstr) (k : ProofM Expr) :

Equations

c.caching k = Lean.Meta.Grind.Arith.Cutsat.caching c.id k

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.caching (c : DiseqCnstr) (k : ProofM Expr) :

Equations

c.caching k = Lean.Meta.Grind.Arith.Cutsat.caching c.id k

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.withProofContext (x : ProofM Expr) :

Equations

One or more equations did not get rendered due to their size.

def Int.Linear.Poly.eval? (p : Poly) :

Lean.Meta.Grind.GoalM (Option Std.Internal.Rat)

Tries to evaluate the polynomial p using the partial model/assignment built so far. The result is none if the polynomial contains variables that have not been assigned.

Equations

p.eval? = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.get' let a : Lean.PArray Std.Internal.Rat := __do_lift.assignment pure (Int.Linear.Poly.eval?.go a 0 p)

def Int.Linear.Poly.eval?.go (a : Lean.PArray Std.Internal.Rat) (v : Std.Internal.Rat) :

Poly → Option Std.Internal.Rat

Equations

Int.Linear.Poly.eval?.go a v (Int.Linear.Poly.num k) = some (v + { num := k, den := 1 })
Int.Linear.Poly.eval?.go a v (Int.Linear.Poly.add k x_1 p) = if x : x_1 < a.size then Int.Linear.Poly.eval?.go a (v + { num := k, den := 1 } * a[x_1]) p else none

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.LeCnstr.isUnsat (c : LeCnstr) :

Equations

c.isUnsat = c.p.isUnsatLe

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.isUnsat (c : DvdCnstr) :

Equations

c.isUnsat = Int.Linear.Poly.isUnsatDvd c.d c.p

def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.satisfied (c : DvdCnstr) :

Returns .true if c is satisfied by the current partial model, .undef if c contains unassigned variables, and .false otherwise.

Equations

One or more equations did not get rendered due to their size.

def Int.Linear.Poly.satisfiedLe (p : Poly) :

Lean.Meta.Grind.GoalM Lean.LBool

Equations

p.satisfiedLe = do let __discr ← p.eval? match __discr with | some v => pure (decide (v ≤ 0)).toLBool | x => pure Lean.LBool.undef

def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.satisfied (c : LeCnstr) :

Returns .true if c is satisfied by the current partial model, .undef if c contains unassigned variables, and .false otherwise.

Equations

c.satisfied = c.p.satisfiedLe

def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.satisfied (c : DiseqCnstr) :

Returns .true if c is satisfied by the current partial model, .undef if c contains unassigned variables, and .false otherwise.

Equations

c.satisfied = do let __discr ← c.p.eval? match __discr with | some v => pure (v != 0).toLBool | x => pure Lean.LBool.undef

def Int.Linear.Poly.findVarToSubst (p : Poly) :

Lean.Meta.Grind.GoalM (Option (Int × Var × Lean.Meta.Grind.Arith.Cutsat.EqCnstr))

Given a polynomial p, returns some (x, k, c) if p contains the monomial k*x, and x has been eliminated using the equality c.

Equations

One or more equations did not get rendered due to their size.
(Int.Linear.Poly.num k).findVarToSubst = pure none