def Int.Linear.Poly.isZero : Poly → Bool

Equations

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

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

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' : GoalM State

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) : GoalM Unit

Equations

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

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

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) : GoalM Expr

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) : GoalM Bool

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 : GoalM Nat

Equations

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

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

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) : GoalM Unit

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

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

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) : PArray Rat

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

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) : Bool

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) : GoalM Expr

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) : GoalM α

Equations

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

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

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) : GoalM α

Equations

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

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

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) : Bool

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) : GoalM Expr

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) : GoalM α

Equations

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

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

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) : GoalM Expr

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) : GoalM α

Equations

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

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

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) : GoalM Unit

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 : GoalM Expr

Equations

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

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

• cache : Std.HashMap Nat Expr

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.ProofM (α : Type) : 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 : ProofM Expr

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) : 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) : 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) : 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) : 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) : 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) : GoalM 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) : Bool

Equations

• c.isUnsat = c.p.isUnsatLe

@[reducible, inline]

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

Equations

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

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

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) : GoalM LBool

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) : GoalM LBool

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