@[reducible, inline]

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

Equations

• Lean.Meta.Grind.Arith.CommRing.RingExpr = Lean.Grind.CommRing.Expr

@[reducible, inline]

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

Equations

• Lean.Meta.Grind.Arith.CommRing.SemiringExpr = Lean.Grind.Ring.OfSemiring.Expr

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 Lean.Meta.Grind.Arith.CommRing.instInhabitedEqCnstrProof : Inhabited EqCnstrProof

Equations

• Lean.Meta.Grind.Arith.CommRing.instInhabitedEqCnstrProof = { default := Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.core default default default default }

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

Equations

• Lean.Meta.Grind.Arith.CommRing.instInhabitedEqCnstr = { default := { p := default, h := default, sugar := 0, id := 0 } }

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

Equations

• c₁.compare c₂ = ((compare c₁.sugar c₂.sugar).then (compare c₁.p.degree c₂.p.degree)).then (compare c₁.id c₂.id)

@[reducible, inline]

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

Equations

• Lean.Meta.Grind.Arith.CommRing.Queue = Std.TreeSet Lean.Meta.Grind.Arith.CommRing.EqCnstr Lean.Meta.Grind.Arith.CommRing.EqCnstr.compare

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

A polynomial equipped with a chain of rewrite steps that justifies its equality to the original input. From an input polynomial p, we use equations (i.e., EqCnstr) as rewriting rules. For example, consider the following sequence of rewrites for the input polynomial 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.getPoly + 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. We have that C ≠ 1 only if the ring does not implement NoNatZeroDivisors. 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.getPoly.normEq0 k
  

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

Equations

• (Lean.Meta.Grind.Arith.CommRing.PolyDerivation.input p).p = p
• (Lean.Meta.Grind.Arith.CommRing.PolyDerivation.step p k₁ d k₂ m₂ c).p = p
• (Lean.Meta.Grind.Arith.CommRing.PolyDerivation.normEq0 p d c).p = p

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.Ring : Type

Shared state for non-commutative and commutative rings.

• id : Nat
• type : Expr
• u : Level

  Cached getDecLevel type

• ringInst : Expr

  Ring instance for type

• semiringInst : Expr

  Semiring instance for type

• charInst? : Option (Expr × Nat)

  IsCharP instance for type if available.

• addFn? : Option Expr
• mulFn? : Option Expr
• subFn? : Option Expr
• negFn? : Option Expr
• powFn? : Option Expr
• intCastFn? : Option Expr
• natCastFn? : Option Expr
• one? : Option Expr
• 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

def Lean.Meta.Grind.Arith.CommRing.instInhabitedRing.default : Ring

Equations

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

instance Lean.Meta.Grind.Arith.CommRing.instInhabitedRing : Inhabited Ring

Equations

• Lean.Meta.Grind.Arith.CommRing.instInhabitedRing = { default := Lean.Meta.Grind.Arith.CommRing.instInhabitedRing.default }

structure Lean.Meta.Grind.Arith.CommRing.CommRingextends Lean.Meta.Grind.Arith.CommRing.Ring : Type

State for each CommRing processed by this module.

• id : Nat
• type : Expr
• u : Level
• ringInst : Expr
• semiringInst : Expr
• charInst? : Option (Expr × Nat)
• addFn? : Option Expr
• mulFn? : Option Expr
• subFn? : Option Expr
• negFn? : Option Expr
• powFn? : Option Expr
• intCastFn? : Option Expr
• natCastFn? : Option Expr
• one? : Option Expr
• vars : PArray Expr
• varMap : PHashMap ExprPtr Var
• denote : PHashMap ExprPtr RingExpr
• invFn? : Option Expr

  Inverse if fieldInst? is some inst

• semiringId? : Option Nat

  If this is a OfSemiring.Q α ring, this field contain the semiringId for α.

• commSemiringInst : Expr

  CommSemiring instance for type

• commRingInst : Expr

  CommRing instance for type

• noZeroDivInst? : Option Expr

  NoNatZeroDivisors instance for type if available.

• fieldInst? : Option Expr

  Field instance for type if available.

• 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.

• 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 Lean.Meta.Grind.Arith.CommRing.instInhabitedCommRing : Inhabited CommRing

Equations

• Lean.Meta.Grind.Arith.CommRing.instInhabitedCommRing = { default := Lean.Meta.Grind.Arith.CommRing.instInhabitedCommRing.default }

def Lean.Meta.Grind.Arith.CommRing.instInhabitedCommRing.default : CommRing

Equations

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

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

State for each CommSemiring processed by this module. Recall that CommSemiring are processed using the envelop OfCommSemiring.Q

• id : Nat
• ringId : Nat

  Id for OfCommSemiring.Q

• type : Expr
• u : Level

  Cached getDecLevel type

• semiringInst : Expr

  Semiring instance for type

• commSemiringInst : Expr

  CommSemiring instance for type

• addRightCancelInst? : Option (Option Expr)

  AddRightCancel instance for type if available.

• toQFn? : Option Expr
• addFn? : Option Expr
• mulFn? : Option Expr
• powFn? : Option Expr
• natCastFn? : Option Expr
• 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.

def Lean.Meta.Grind.Arith.CommRing.instInhabitedSemiring.default : Semiring

Equations

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

instance Lean.Meta.Grind.Arith.CommRing.instInhabitedSemiring : Inhabited Semiring

Equations

• Lean.Meta.Grind.Arith.CommRing.instInhabitedSemiring = { default := Lean.Meta.Grind.Arith.CommRing.instInhabitedSemiring.default }

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

State for all CommRing types detected by grind.

• rings : Array CommRing

  Commutative rings. We expect to find a small number of rings in a given goal. Thus, using Array is fine here.

• typeIdOf : PHashMap ExprPtr (Option Nat)

  Mapping from types to its "ring id". We cache failures using none. typeIdOf[type] is some id, then id < rings.size.

• exprToRingId : PHashMap ExprPtr Nat
• semirings : Array Semiring

  Commutative semirings. We support them using the envelope OfCommRing.Q

• stypeIdOf : PHashMap ExprPtr (Option Nat)

  Mapping from types to its "semiring id". We cache failures using none. stypeIdOf[type] is some id, then id < semirings.size. If a type is in this map, it is not in typeIdOf.

• exprToSemiringId : PHashMap ExprPtr Nat
• ncRings : Array Ring

  Non commutative rings.

• exprToNCRingId : PHashMap ExprPtr Nat
• nctypeIdOf : PHashMap ExprPtr (Option Nat)

  Mapping from types to its "ring id". We cache failures using none. nctypeIdOf[type] is some id, then id < ncRings.size.

• steps : Nat

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

Equations

• Lean.Meta.Grind.Arith.CommRing.instInhabitedState = { default := Lean.Meta.Grind.Arith.CommRing.instInhabitedState.default }

def Lean.Meta.Grind.Arith.CommRing.instInhabitedState.default : State

Equations

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

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

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

Equations

• Lean.Meta.Grind.Arith.CommRing.get' = Lean.Meta.Grind.Arith.CommRing.ringExt.getState

@[inline]

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

Equations

• Lean.Meta.Grind.Arith.CommRing.modify' f = Lean.Meta.Grind.Arith.CommRing.ringExt.modifyState f