Documentation

Lean.Meta.Tactic.Grind.Arith.Linear.Util

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

Equations

Lean.Meta.Grind.Arith.Linear.get' = do let __do_lift ← get pure __do_lift.arith.linear

@[inline]

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

Equations

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

structure Lean.Meta.Grind.Arith.Linear.LinearM.Context :

structId : Nat

class Lean.Meta.Grind.Arith.Linear.MonadGetStruct (m : Type → Type) :

getStruct : m Struct

Instances

@[always_inline]

instance Lean.Meta.Grind.Arith.Linear.instMonadGetStructOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadGetStruct m] :

MonadGetStruct n

Equations

Lean.Meta.Grind.Arith.Linear.instMonadGetStructOfMonadLift m n = { getStruct := liftM Lean.Meta.Grind.Arith.Linear.getStruct }

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Linear.LinearM (α : Type) :

We don't want to keep carrying the StructId around.

Equations

Lean.Meta.Grind.Arith.Linear.LinearM = ReaderT Lean.Meta.Grind.Arith.Linear.LinearM.Context Lean.Meta.Grind.GoalM

Instances For

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Linear.LinearM.run {α : Type} (structId : Nat) (x : LinearM α) :

Equations

Lean.Meta.Grind.Arith.Linear.LinearM.run structId x = x { structId := structId }

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Linear.getStructId :

Equations

Lean.Meta.Grind.Arith.Linear.getStructId = do let __do_lift ← read pure __do_lift.structId

def Lean.Meta.Grind.Arith.Linear.LinearM.getStruct :

Equations

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

instance Lean.Meta.Grind.Arith.Linear.instMonadGetStructLinearM :

MonadGetStruct LinearM

Equations

Lean.Meta.Grind.Arith.Linear.instMonadGetStructLinearM = { getStruct := Lean.Meta.Grind.Arith.Linear.LinearM.getStruct }

def Lean.Meta.Grind.Arith.Linear.getRingCore? (ringId? : Option Nat) :

GoalM (Option CommRing.Ring)

Equations

Lean.Meta.Grind.Arith.Linear.getRingCore? (some ringId) = Lean.Meta.Grind.Arith.CommRing.RingM.run ringId do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getRing pure (some __do_lift)
Lean.Meta.Grind.Arith.Linear.getRingCore? ringId? = pure none

def Lean.Meta.Grind.Arith.Linear.throwNotRing {α : Type} :

Equations

Lean.Meta.Grind.Arith.Linear.throwNotRing = Lean.throwError (Lean.toMessageData "`grind linarith` internal error, structure is not a ring")

def Lean.Meta.Grind.Arith.Linear.throwNotCommRing {α : Type} :

Equations

Lean.Meta.Grind.Arith.Linear.throwNotCommRing = Lean.throwError (Lean.toMessageData "`grind linarith` internal error, structure is not a commutative ring")

def Lean.Meta.Grind.Arith.Linear.getRing? :

LinearM (Option CommRing.Ring)

Equations

Lean.Meta.Grind.Arith.Linear.getRing? = do let __do_lift ← Lean.Meta.Grind.Arith.Linear.getStruct liftM (Lean.Meta.Grind.Arith.Linear.getRingCore? __do_lift.ringId?)

def Lean.Meta.Grind.Arith.Linear.getRing :

LinearM CommRing.Ring

Equations

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

instance Lean.Meta.Grind.Arith.Linear.instMonadGetRingLinearM :

CommRing.MonadGetRing LinearM

Equations

Lean.Meta.Grind.Arith.Linear.instMonadGetRingLinearM = { getRing := Lean.Meta.Grind.Arith.Linear.getRing }

def Lean.Meta.Grind.Arith.Linear.getZero :

Equations

Lean.Meta.Grind.Arith.Linear.getZero = do let __do_lift ← Lean.Meta.Grind.Arith.Linear.getStruct pure __do_lift.zero

def Lean.Meta.Grind.Arith.Linear.getOne :

Equations

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

def Lean.Meta.Grind.Arith.Linear.withRingM {α : Type} (x : CommRing.RingM α) :

Equations

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

def Lean.Meta.Grind.Arith.Linear.isCommRing :

Equations

Lean.Meta.Grind.Arith.Linear.isCommRing = do let __do_lift ← Lean.Meta.Grind.Arith.Linear.getStruct pure __do_lift.ringId?.isSome

def Lean.Meta.Grind.Arith.Linear.isOrderedCommRing :

Equations

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

def Lean.Meta.Grind.Arith.Linear.isLinearOrder :

Equations

Lean.Meta.Grind.Arith.Linear.isLinearOrder = do let __do_lift ← Lean.Meta.Grind.Arith.Linear.getStruct pure __do_lift.linearInst?.isSome

def Lean.Meta.Grind.Arith.Linear.hasNoNatZeroDivisors :

Equations

Lean.Meta.Grind.Arith.Linear.hasNoNatZeroDivisors = do let __do_lift ← Lean.Meta.Grind.Arith.Linear.getStruct pure __do_lift.noNatDivInst?.isSome

@[inline]

def Lean.Meta.Grind.Arith.Linear.modifyStruct (f : Struct → Struct) :

Equations

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

def Lean.Meta.Grind.Arith.Linear.getTermStructId? (e : Expr) :

GoalM (Option Nat)

Equations

Lean.Meta.Grind.Arith.Linear.getTermStructId? e = do let __do_lift ← Lean.Meta.Grind.Arith.Linear.get' pure (Lean.PersistentHashMap.find? __do_lift.exprToStructId { expr := e })

def Lean.Meta.Grind.Arith.Linear.setTermStructId (e : Expr) :

Equations

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

def Lean.Meta.Grind.Arith.Linear.getNoNatDivInst :

Equations

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

def Lean.Meta.Grind.Arith.Linear.getPreorderInst :

Equations

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

def Lean.Meta.Grind.Arith.Linear.getOrderedAddInst :

Equations

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

def Lean.Meta.Grind.Arith.Linear.isOrderedAdd :

Equations

Lean.Meta.Grind.Arith.Linear.isOrderedAdd = do let __do_lift ← Lean.Meta.Grind.Arith.Linear.getStruct pure __do_lift.orderedAddInst?.isSome

def Lean.Meta.Grind.Arith.Linear.getLtFn {m : Type → Type} [Monad m] [MonadError m] [MonadGetStruct m] :

Equations

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

def Lean.Meta.Grind.Arith.Linear.getLeFn {m : Type → Type} [Monad m] [MonadError m] [MonadGetStruct m] :

Equations

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

def Lean.Meta.Grind.Arith.Linear.getLinearOrderInst :

Equations

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

def Lean.Meta.Grind.Arith.Linear.getRingInst :

Equations

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

def Lean.Meta.Grind.Arith.Linear.getCommRingInst :

Equations

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

def Lean.Meta.Grind.Arith.Linear.getOrderedRingInst :

Equations

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

def Lean.Grind.Linarith.Poly.eval? (p : Poly) :

Meta.Grind.Arith.Linear.LinearM (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.Linear.getStruct have a : Lean.PArray Std.Internal.Rat := __do_lift.assignment pure (Lean.Grind.Linarith.Poly.eval?.go a 0 p)

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

Poly → Option Std.Internal.Rat

Equations

Lean.Grind.Linarith.Poly.eval?.go a v Lean.Grind.Linarith.Poly.nil = some v
Lean.Grind.Linarith.Poly.eval?.go a v (Lean.Grind.Linarith.Poly.add k x_1 p) = if x : x_1 < a.size then Lean.Grind.Linarith.Poly.eval?.go a (v + { num := k } * a[x_1]) p else none

def Lean.Meta.Grind.Arith.Linear.IneqCnstr.satisfied (c : IneqCnstr) :

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 Lean.Meta.Grind.Arith.Linear.DiseqCnstr.satisfied (c : DiseqCnstr) :

Equations

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

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

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

Equations

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

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

Equations

Lean.Meta.Grind.Arith.Linear.getVar x = do let __do_lift ← Lean.Meta.Grind.Arith.Linear.getStruct pure __do_lift.vars[x]!

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

Returns true if the linarith state is inconsistent.

Equations

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

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

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

Equations

Lean.Meta.Grind.Arith.Linear.eliminated x = do let __do_lift ← Lean.Meta.Grind.Arith.Linear.getStruct pure __do_lift.elimEqs[x]!.isSome

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

Returns occurrences of x.

Equations

Lean.Meta.Grind.Arith.Linear.getOccursOf x = do let __do_lift ← Lean.Meta.Grind.Arith.Linear.getStruct pure __do_lift.occurs[x]!

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

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

Equations

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

def Lean.Grind.Linarith.Poly.updateOccs (p : Poly) :

Meta.Grind.Arith.Linear.LinearM Unit

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

Equations

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

partial def Lean.Grind.Linarith.Poly.updateOccs.go (y : Var) (p : Poly) :

Meta.Grind.Arith.Linear.LinearM Unit

def Lean.Grind.Linarith.Poly.findVarToSubst (p : Poly) :

Meta.Grind.Arith.Linear.LinearM (Option (Int × Var × Meta.Grind.Arith.Linear.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.
Lean.Grind.Linarith.Poly.nil.findVarToSubst = pure none

def Lean.Grind.Linarith.Poly.gcdCoeffsAux :

Poly → Nat → Nat

Equations

Lean.Grind.Linarith.Poly.nil.gcdCoeffsAux x✝ = x✝
(Lean.Grind.Linarith.Poly.add k' v p).gcdCoeffsAux x✝ = p.gcdCoeffsAux (k'.gcd ↑x✝)

def Lean.Grind.Linarith.Poly.gcdCoeffs (p : Poly) :

Equations

(Lean.Grind.Linarith.Poly.add k v p_2).gcdCoeffs = p_2.gcdCoeffsAux k.natAbs
Lean.Grind.Linarith.Poly.nil.gcdCoeffs = 1

def Lean.Grind.Linarith.Poly.div (p : Poly) (k : Int) :

Equations

(Lean.Grind.Linarith.Poly.add k_1 v p_2).div k = Lean.Grind.Linarith.Poly.add (k_1 / k) v (p_2.div k)
Lean.Grind.Linarith.Poly.nil.div k = Lean.Grind.Linarith.Poly.nil

def Lean.Grind.Linarith.Poly.pickVarToElim? (p : Poly) :

Option (Int × Var)

Selects the variable in the given linear polynomial whose coefficient has the smallest absolute value.

Equations

Lean.Grind.Linarith.Poly.nil.pickVarToElim? = none
(Lean.Grind.Linarith.Poly.add k x_1 p_1).pickVarToElim? = some (Lean.Grind.Linarith.Poly.pickVarToElim?.go k x_1 p_1)

def Lean.Grind.Linarith.Poly.pickVarToElim?.go (k : Int) (x : Var) (p : Poly) :

Equations

One or more equations did not get rendered due to their size.
Lean.Grind.Linarith.Poly.pickVarToElim?.go k x Lean.Grind.Linarith.Poly.nil = if (k == 1 || k == -1) = true then (k, x) else (k, x)