source
def Lean.Meta.Grind.Arith.Linear.getZero :
LinearM Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Linear.getOne :
LinearM Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Linear.isCommRing :
LinearM Bool
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Linear.isOrderedCommRing :
LinearM Bool
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Linear.isLinearOrder :
LinearM Bool
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Linear.hasNoNatZeroDivisors :
LinearM Bool
Equations

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

Instances For

source
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 })

Instances For

source
def Lean.Meta.Grind.Arith.Linear.setTermStructId (e : Expr) :
LinearM Unit
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Linear.getNoNatDivInst :
LinearM Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Linear.getLEInst :
LinearM Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Linear.getLTInst :
LinearM Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Linear.getLawfulOrderLTInst :
LinearM Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Linear.getIsPreorderInst :
LinearM Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Linear.getOrderedAddInst :
LinearM Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Linear.isOrderedAdd :
LinearM Bool
Equations

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

Instances For

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

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

Instances For

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

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

Instances For

source
def Lean.Meta.Grind.Arith.Linear.getIsLinearOrderInst :
LinearM Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Linear.getRingInst :
LinearM Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Linear.getCommRingInst :
LinearM Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Linear.getOrderedRingInst :
LinearM Expr
Equations

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

Instances For

source
def Lean.Grind.Linarith.Poly.eval? (p : Poly) :
Meta.Grind.Arith.Linear.LinearM (Option 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 Rat := __do_lift.assignment pure (Lean.Grind.Linarith.Poly.eval?.go✝ a 0 p)

Instances For

source
def Lean.Meta.Grind.Arith.Linear.IneqCnstr.satisfied (c : IneqCnstr) :
LinearM 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.

Instances For

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

Instances For

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

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

Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Linear.getVar (x : Var) :
LinearM Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Linear.inconsistent :
LinearM Bool

Returns `true` if the linarith state is inconsistent.

Equations

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

Instances For

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

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

Instances For

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

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]!

Instances For

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

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.

Instances For

source
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")

Instances For

source
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

Instances For

source
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✝)

Instances For

source
def Lean.Grind.Linarith.Poly.gcdCoeffs (p : Poly) :
Nat
Equations

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

Instances For

source
def Lean.Grind.Linarith.Poly.div (p : Poly) (k : Int) :
Poly
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

Instances For

source
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)

Instances For