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

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

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.

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.

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

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.

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

Simplifies c₁ using c₂.

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

Simplifies c₁ using c₂.

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

Simplifies c₁ using c₂ exhaustively.

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

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

Simplify the given equation constraint using the current basis.

Note: This function (and simplifyBasis) runs with checkCoeffDvd := true. It rewrites a monomial k'*m' using an equation with leading term k*m only if k ∣ k' (or the ring implements NoNatZeroDivisors). Rewriting without this restriction requires multiplying the equation by k/gcd k k' ≠ ±1 first, and replacing an equation with the result loses information: p = 0 cannot be recovered from (k/gcd k k') * p = 0 in an arbitrary commutative ring. The consequences of the skipped rewrites are not lost: a skipped rewrite at the leading monomial coincides with the S-polynomial computed by superposeWith, so it is derived non-destructively. The price is that the basis is not fully interreduced (e.g., 2*x = 0 and 3*x = 0 may coexist), and reduction is an incomplete ideal-membership test in rings without NoNatZeroDivisors (e.g., x = 0 is not derived from 2*x = 0 and 3*x = 0). The complete alternative is a strong Gröbner basis over Int (Kandri-Rody & Kapur): replace multiply-through rewriting with Euclidean remainder reduction on coefficients (k' = q*k + r, so the equation is never multiplied by a constant), and additionally superpose gcd-polynomials (Bézout combinations producing gcd k k' times the lcm of the leading monomials). We should consider this option in the future.

Note: If using withCheckCoeffDvd becomes too expensive when one does not have NoNatZeroDivisors, we will add a flag to perform the simplification anyway even if information is lost.

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

Returns true if c.p is the constant polynomial.

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.

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

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

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

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.

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

Simplifies the basis using c. Every equation that c rewrites is removed from the basis and requeued in its rewritten form.

See Note at EqCnstr.simplify for why checkCoeffDvd must be enabled here.

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

@[inline]

def Lean.Meta.Grind.Arith.CommRing.withCheckingNumEq0 (k : RingM Unit) : RingM Unit

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

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

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

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

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

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

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

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

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

@[reducible, inline]

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

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

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

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