The classification of a type as a (commutative) ring or semiring, its instances, and its cached operator functions live in Sym.Arith.State, a SymExtension shared by the whole grind run. This module only stores per-goal solver state, in the structures below, indexed by the ids assigned by Sym.Arith.classify?.

structure Lean.Meta.Grind.Arith.CommRing.EqCnstr : Type

• p : Poly
• h : EqCnstrProof
• sugar : Nat
• id : Nat

inductive Lean.Meta.Grind.Arith.CommRing.EqCnstrProof : Type

• core (a b : Expr) (ra rb : RingExpr) : EqCnstrProof
• coreS (a b : Expr) (sa sb : SemiringExpr) (ra rb : RingExpr) : EqCnstrProof
• superpose (k₁ : Int) (m₁ : Mon) (c₁ : EqCnstr) (k₂ : Int) (m₂ : Mon) (c₂ : EqCnstr) : EqCnstrProof
• simp (k₁ : Int) (c₁ : EqCnstr) (k₂ : Int) (m₂ : Mon) (c₂ : EqCnstr) : EqCnstrProof
• mul (k : Int) (e : EqCnstr) : EqCnstrProof
• div (k : Int) (e : EqCnstr) : EqCnstrProof
• gcd (a b : Int) (c₁ c₂ : EqCnstr) : EqCnstrProof
• numEq0 (k : Nat) (c₁ c₂ : EqCnstr) : EqCnstrProof

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instInhabitedEqCnstrProof : Inhabited EqCnstrProof

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instInhabitedEqCnstr : Inhabited EqCnstr

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.compare (c₁ c₂ : EqCnstr) : Ordering

@[reducible, inline]

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

inductive Lean.Meta.Grind.Arith.CommRing.PolyDerivation : Type

A polynomial p equipped with a chain of rewrite steps that justifies p = C * input, where input is the original polynomial and C is the product of the multipliers k₁ of the .steps in the chain (C = 1 when every step is monic). C ≠ 1 is possible in any ring, including those with NoNatZeroDivisors; the instance only lets C be cancelled. From an input polynomial, we use equations (i.e., EqCnstr) as rewriting rules. For example, consider the following sequence of rewrites for the input polynomial 2*x^2 + x*y using the equations x - 1 = 0 (c₁) and y - 2 = 0 (c₂).

2*x^2 + x*y                  | s₁ := .input (2*x^2 + x*y)
=           - 2*x*(x - 1)
(2*x + x*y)                  | s₂ := .step (2*x + x*y)  1 s₁ (-2) x c₁
=           - 2*1*(x - 1)
(x*y + 2)                    | s₃ := .step (x*y + 2) 1 s₂ (-2) 1 c₁
=           - 1*y*(x - 1)
(y + 2)                      | s₄ := .step (y+2) 1 s₃ (-1) y c₁
=           - 1*1*(y - 2)
4                            | s₅ := .step 4 1 s₄ (-1) 1 c₂

From the chain above, we build the certificate

(-2*x - y - 2)*(x-1) + (-1)*(y-2)

for

4 = (2*x^2 + x*y)

because x-1 = 0 and y-2=0

• input (p : Poly) : PolyDerivation
• step (p : Poly) (k₁ : Int) (d : PolyDerivation) (k₂ : Int) (m₂ : Mon) (c : EqCnstr) : PolyDerivation

  p = k₁*d.p + k₂*m₂*c.p
  

  The coefficient k₁ is used because the leading monomial in c may not be monic. Thus, if we follow the chain back to the input polynomial, we have that p = C * input_p for a C that is equal to the product of all k₁s in the chain. C ≠ 1 can happen in any ring, but C can be cancelled only if the ring implements NoNatZeroDivisors. That is, p = 0 implies input_p = 0 only if C = 1 or the ring implements NoNatZeroDivisors. Simplifying with checkCoeffDvd := true guarantees C = 1 in rings without NoNatZeroDivisors, see Mon.findSimp?. Here is a small example where we simplify x+y using the equations 2*x - 1 = 0 (c₁), 3*y - 1 = 0 (c₂), and 6*z + 5 = 0 (c₃)

  x + y + z            | s₁ := .input (x + y + z)
  *2
  =   - 1*1*(2*x - 1)
  2*y + 2*z + 1        | s₂ := .step (2*y + 2*z + 1) 2 s₁ (-1) 1 c₁
  *3
  =   - 2*1*(3*y - 1)
  6*z + 5              | s₃ := .step (6*z + 5) 3 s₂ (-2) 1 c₂
  =   - 1*1*(6*z + 5)
  0                    | s₄ := .step (0) 1 s₃ (-1) 1 c₃
  

  For this chain, we build the certificate

  (-3)*(2*x - 1) + (-2)*(3*y - 1) + (-1)*(6*z + 5)
  

  for

  0 = 6*(x + y + z)
  

  Recall that if the ring implement NoNatZeroDivisors, then the following property holds:

  ∀ (k : Int) (a : α), k ≠ 0 → (intCast k) * a = 0 → a = 0
  

  grind can deduce that x+y+z = 0

• normEq0 (p : Poly) (d : PolyDerivation) (c : EqCnstr) : PolyDerivation

  Given c.p == .num k

  p = d.p.normEq0 k
  

def Lean.Meta.Grind.Arith.CommRing.PolyDerivation.p : PolyDerivation → Poly

structure Lean.Meta.Grind.Arith.CommRing.DiseqCnstr : Type

A disequality lhs ≠ rhs asserted by the core.

• lhs : Expr
• rhs : Expr
• rlhs : RingExpr

  Reified lhs

• rrhs : RingExpr

  Reified rhs

• d : PolyDerivation

  lhs - rhs simplification chain. If it becomes 0 we have an inconsistency.

• ofSemiring? : Option (SemiringExpr × SemiringExpr)

  If lhs and rhs are semiring expressions that have been adapted as ring ones. The respective semiring reified expressions are stored here.

structure Lean.Meta.Grind.Arith.CommRing.SemiringState : Type

Per-goal solver state of a (commutative or not) semiring classified by Sym.Arith.

• denote : PHashMap ExprPtr SemiringExpr

  Mapping from Lean expressions to their representations as SemiringExpr

• vars : PArray Expr

  Mapping from variables to their denotations. Remark each variable can be in only one ring.

• varMap : PHashMap ExprPtr Var

  Mapping from Expr to a variable representing it.

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instInhabitedSemiringState : Inhabited SemiringState

structure Lean.Meta.Grind.Arith.CommRing.RingState : Type

Per-goal solver state of a (commutative or not) ring classified by Sym.Arith.

• vars : PArray Expr

  Mapping from variables to their denotations. Remark each variable can be in only one ring.

• varMap : PHashMap ExprPtr Var

  Mapping from Expr to a variable representing it.

• denote : PHashMap ExprPtr RingExpr

  Mapping from Lean expressions to their representations as RingExpr

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instInhabitedRingState : Inhabited RingState

structure Lean.Meta.Grind.Arith.CommRing.CommRingState extends Lean.Meta.Grind.Arith.CommRing.RingState : Type

Per-goal solver state of a commutative ring: the Gröbner basis machinery.

• vars : PArray Expr
• varMap : PHashMap ExprPtr Var
• denote : PHashMap ExprPtr RingExpr
• denoteEntries : PArray (Expr × RingExpr)

  denoteEntries is denote as a PArray for deterministic traversal.

• nextId : Nat

  Next unique id for EqCnstrs.

• steps : Nat

  Number of "steps": simplification and superposition.

• queue : Queue

  Equations to process.

• basis : List EqCnstr

  The basis is currently just a list. If this is a performance bottleneck, we should use a better data-structure. For examples, we could use a simple indexing for the linear case where we map variable in the leading monomial to EqCnstr.

• diseqs : PArray DiseqCnstr

  Disequalities.

• recheck : Bool

  If recheck is true, then new equalities have been added to the basis since we checked disequalities and implied equalities.

• invSet : PHashSet Expr

  Inverse theorems that have been already asserted.

• powIdentityVarCount : Nat

  Number of variables for which PowIdentity equations have been pushed.

• numEq0? : Option EqCnstr

  An equality of the form c = 0. It is used to simplify polynomial coefficients.

• numEq0Updated : Bool

  Flag indicating whether numEq0? has been updated.

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instInhabitedCommRingState : Inhabited CommRingState

structure Lean.Meta.Grind.Arith.CommRing.State : Type

Per-goal state of the ring solver.

The four arrays are indexed by the ids assigned by Sym.Arith.classify?: rings[i] is the solver state for Sym.Arith.State.rings[i], and likewise for semirings, ncRings, and ncSemirings. The Sym.Arith arrays are shared by every goal of the run and only grow, while a goal uses only some of the rings. To keep the two indexings aligned, an array here is padded with empty states up to the id being written (see State.modifyRing), and reading an id beyond the array returns the empty state. Rings a goal never used therefore cost at most an empty entry, and rings.size ≤ Sym.Arith.State.rings.size always holds.

• rings : Array CommRingState

  Solver state of the commutative rings, indexed by Sym.Arith ring id.

• exprToRingId : PHashMap ExprPtr Nat
• semirings : Array SemiringState

  Solver state of the commutative semirings, indexed by Sym.Arith semiring id.

• exprToSemiringId : PHashMap ExprPtr Nat
• ncRings : Array RingState

  Solver state of the non-commutative rings, indexed by Sym.Arith id.

• exprToNCRingId : PHashMap ExprPtr Nat
• ncSemirings : Array SemiringState

  Solver state of the non-commutative semirings, indexed by Sym.Arith id.

• exprToNCSemiringId : PHashMap ExprPtr Nat
• steps : Nat
• reportedMaxDegreeIssue : Bool

  true if solver has already reported max degree issue.

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instInhabitedState : Inhabited State

opaque Lean.Meta.Grind.Arith.CommRing.ringExt : SolverExtension State

def Lean.Meta.Grind.Arith.CommRing.get' : GoalM State

@[inline]

def Lean.Meta.Grind.Arith.CommRing.modify' (f : State → State) : GoalM Unit

def Lean.Meta.Grind.Arith.CommRing.State.getRing (s : State) (ringId : Nat) : CommRingState

Solver state of the commutative ring ringId; empty if this goal has not used it yet.

@[inline]

def Lean.Meta.Grind.Arith.CommRing.State.modifyRing (s : State) (ringId : Nat) (f : CommRingState → CommRingState) : State

def Lean.Meta.Grind.Arith.CommRing.State.getSemiring (s : State) (semiringId : Nat) : SemiringState

Solver state of the commutative semiring semiringId; empty if this goal has not used it yet.

@[inline]

def Lean.Meta.Grind.Arith.CommRing.State.modifySemiring (s : State) (semiringId : Nat) (f : SemiringState → SemiringState) : State

def Lean.Meta.Grind.Arith.CommRing.State.getNCRing (s : State) (ringId : Nat) : RingState

Solver state of the non-commutative ring ringId; empty if this goal has not used it yet.

@[inline]

def Lean.Meta.Grind.Arith.CommRing.State.modifyNCRing (s : State) (ringId : Nat) (f : RingState → RingState) : State

def Lean.Meta.Grind.Arith.CommRing.State.getNCSemiring (s : State) (semiringId : Nat) : SemiringState

Solver state of the non-commutative semiring semiringId; empty if this goal has not used it yet.

@[inline]

def Lean.Meta.Grind.Arith.CommRing.State.modifyNCSemiring (s : State) (semiringId : Nat) (f : SemiringState → SemiringState) : State

class Lean.Meta.Grind.Arith.CommRing.MonadRingState (m : Type → Type) : Type

Access to the per-goal state of the current (commutative or not) ring.

• getRingState : m RingState
• modifyRingState : (RingState → RingState) → m Unit

@[instance_reducible, always_inline]

instance Lean.Meta.Grind.Arith.CommRing.instMonadRingStateOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadRingState m] : MonadRingState n

class Lean.Meta.Grind.Arith.CommRing.MonadCommRingState (m : Type → Type) : Type

Access to the per-goal state of the current commutative ring.

• getCommRingState : m CommRingState
• modifyCommRingState : (CommRingState → CommRingState) → m Unit

@[instance_reducible, always_inline]

instance Lean.Meta.Grind.Arith.CommRing.instMonadCommRingStateOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadCommRingState m] : MonadCommRingState n

@[instance_reducible, always_inline]

instance Lean.Meta.Grind.Arith.CommRing.instMonadRingStateOfMonadOfMonadCommRingState (m : Type → Type) [Monad m] [MonadCommRingState m] : MonadRingState m

class Lean.Meta.Grind.Arith.CommRing.MonadSemiringState (m : Type → Type) : Type

Access to the per-goal state of the current (commutative or not) semiring.

• getSemiringState : m SemiringState
• modifySemiringState : (SemiringState → SemiringState) → m Unit

@[instance_reducible, always_inline]

instance Lean.Meta.Grind.Arith.CommRing.instMonadSemiringStateOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadSemiringState m] : MonadSemiringState n