def Lean.Meta.Grind.Arith.CommRing.mkEqCnstr (p : Poly) (h : EqCnstrProof) : RingM EqCnstr

Equations

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

def Lean.Grind.CommRing.Mon.findSimp? (k : Int) (m : Mon) : Meta.Grind.Arith.CommRing.RingM (Option Meta.Grind.Arith.CommRing.EqCnstr)

Returns some c, where c is an equation from the basis whose leading monomial divides m. Remark: if the current ring does not satisfy the property

∀ (k : Nat) (a : α), k ≠ 0 → OfNat.ofNat (α := α) k * a = 0 → a = 0

then the leading coefficient of the equation must also divide k

Equations

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

def Lean.Grind.CommRing.Mon.findSimp?.go (k : Int) (m : Mon) (checkCoeff noZeroDiv : Bool) : Mon → Meta.Grind.Arith.CommRing.RingM (Option Meta.Grind.Arith.CommRing.EqCnstr)

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Mon.findSimp?.go k m checkCoeff noZeroDiv Lean.Grind.CommRing.Mon.unit = pure none

def Lean.Grind.CommRing.Poly.findSimp? (p : Poly) : Meta.Grind.Arith.CommRing.RingM (Option Meta.Grind.Arith.CommRing.EqCnstr)

Returns some c, where c is an equation from the basis whose leading monomial divides some monomial in p.

Equations

• (Lean.Grind.CommRing.Poly.num k).findSimp? = pure none
• (Lean.Grind.CommRing.Poly.add k m p_2).findSimp? = do let __do_lift ← Lean.Grind.CommRing.Mon.findSimp? k m match __do_lift with | some c => pure (some c) | none => p_2.findSimp?

def Lean.Meta.Grind.Arith.CommRing.PolyDerivation.simplifyWith (d : PolyDerivation) (c : EqCnstr) : RingM PolyDerivation

Simplifies d.p using c, and returns an extended polynomial derivation.

Equations

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

def Lean.Meta.Grind.Arith.CommRing.PolyDerivation.simplify (d : PolyDerivation) : RingM PolyDerivation

Simplified d.p using the current basis, and returns the extended polynomial derivation.

Equations

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

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.simplifyWith (c₁ c₂ : EqCnstr) : RingM EqCnstr

Simplifies c₁ using c₂.

Equations

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

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.simplify (c : EqCnstr) : RingM EqCnstr

Simplify the given equation constraint using the current basis.

Equations

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

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.checkConstant (c : EqCnstr) : RingM Bool

Returns true if c.p is the constant polynomial.

Equations

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

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.simplifyAndCheck (c : EqCnstr) : RingM (Option EqCnstr)

Simplifies and checks whether the resulting constraint is trivial (i.e., 0 = 0), or inconsistent (i.e., k = 0 where k % c != 0 for a comm-ring with characteristic c), and returns none. Otherwise, returns the simplified constraint.

Equations

• c.simplifyAndCheck = do let c ← c.simplify let __do_lift ← c.checkConstant if __do_lift = true then pure none else pure (some c)

def Lean.Meta.Grind.Arith.CommRing.addToBasisCore (c : EqCnstr) : RingM Unit

Equations

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

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.simplifyBasis (c : EqCnstr) : RingM Unit

Equations

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

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.addToQueue (c : EqCnstr) : RingM Unit

Equations

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

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.superposeWith (c : EqCnstr) : RingM Unit

Equations

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

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.superposeWith.go (c : EqCnstr) : Mon → RingM Unit

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.Arith.CommRing.EqCnstr.superposeWith.go c Lean.Grind.CommRing.Mon.unit = pure ()

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.toMonic (c : EqCnstr) : RingM EqCnstr

Tries to convert the leading monomial into a monic one.

It exploits the fact that given a polynomial with leading coefficient k, if the ring has a nonzero characteristic p and gcd k p = 1, then k has an inverse.

It also handles the easy case where k is -1.

Remark: if the ring implements the class NoNatZeroDivisors, then the coefficients are divided by the gcd of all coefficients.

Equations

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

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.addToBasisAfterSimp (c : EqCnstr) : RingM Unit

Equations

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

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.addToBasis (c : EqCnstr) : RingM Unit

Equations

• c.addToBasis = do let __discr ← c.simplifyAndCheck match __discr with | some c => c.addToBasisAfterSimp | x => pure ()

def Lean.Meta.Grind.Arith.CommRing.addNewEq (c : EqCnstr) : RingM Unit

Equations

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

def Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.checkConstant (c : DiseqCnstr) : RingM Bool

Returns true if c.d.p is the constant polynomial.

Equations

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

def Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.simplify (c : DiseqCnstr) : RingM DiseqCnstr

Equations

• c.simplify = Lean.Meta.Grind.Arith.CommRing.withCheckCoeffDvd do let __do_lift ← c.d.simplify pure { lhs := c.lhs, rhs := c.rhs, rlhs := c.rlhs, rrhs := c.rrhs, d := __do_lift }

def Lean.Meta.Grind.Arith.CommRing.saveDiseq (c : DiseqCnstr) : RingM Unit

Equations

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

def Lean.Meta.Grind.Arith.CommRing.addNewDiseq (c : DiseqCnstr) : RingM Unit

Equations

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

@[export lean_process_ring_eq]

def Lean.Meta.Grind.Arith.CommRing.processNewEqImpl (a b : Expr) : GoalM Unit

Equations

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

@[export lean_process_ring_diseq]

def Lean.Meta.Grind.Arith.CommRing.processNewDiseqImpl (a b : Expr) : GoalM Unit

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.PropagateEqMap : Type

Equations

• Lean.Meta.Grind.Arith.CommRing.PropagateEqMap = Std.HashMap (Int × Lean.Grind.CommRing.Poly) (Lean.Expr × Lean.Meta.Grind.Arith.CommRing.RingExpr)

def Lean.Meta.Grind.Arith.CommRing.checkRing : RingM Bool

Equations

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

def Lean.Meta.Grind.Arith.CommRing.check : GoalM Bool

Equations

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