Lean.Meta.Tactic.Grind.Arith.CommRing.Types

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

Instances For

source

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

Instances For

source

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 simplication chain. If it becomes 0 we have an inconsistency.

Instances For

source

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

Type

State for each CommRing processed by this module.

id : Nat
type : Expr
u : Level
Cached getDecLevel type
commRingInst : Expr
CommRing instance for type
charInst? : Option (Expr × Nat)
IsCharP instance for type if available.
noZeroDivInst? : Option Expr
NoNatZeroDivisors instance for type if available.
addFn : Expr
mulFn : Expr
subFn : Expr
negFn : Expr
powFn : Expr
intCastFn : Expr
natCastFn : Expr
vars : PArray Expr
Mapping from variables to their denotations. Remark each variable can be in only one ring.
varMap : PHashMap ENodeKey Var
Mapping from Expr to a variable representing it.
denote : PHashMap ENodeKey RingExpr
Mapping from Lean expressions to their representations as RingExpr
nextId : Nat
Next unique id for EqCnstrs.
steps : Nat
Number of "steps": simplification and superposition.
queue : Queue
Equations to process.
varToBasis : PArray (List EqCnstr)
Mapping from variables x to equations such that the smallest variable in the leading monomial is x.
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.

Instances For

source

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

Inhabited Ring

Equations

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

source

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

Type

State for all CommRing types detected by grind.

rings : Array Ring
Commutative rings. We expect to find a small number of rings in a given goal. Thus, using Array is fine here.
typeIdOf : PHashMap ENodeKey (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 ENodeKey Nat
steps : Nat

Instances For

source

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

Inhabited State

Equations

Lean.Meta.Grind.Arith.CommRing.instInhabitedState = { default := { rings := default, typeIdOf := default, exprToRingId := default, steps := default } }