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
normEq0 (p : Poly) (d : PolyDerivation) (c : EqCnstr) : PolyDerivation
Given c.p == .num k
```
p = d.getPoly.normEq0 k
```

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
(Lean.Meta.Grind.Arith.CommRing.PolyDerivation.normEq0 p d 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 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.

Instances For

source

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

Type

State for each CommRing processed by this module.

id : Nat
semiringId? : Option Nat
If this is a OfSemiring.Q α ring, this field contain the semiringId for α.
type : Expr
u : Level
Cached getDecLevel type
semiringInst : Expr
Semiring instance for type
ringInst : Expr
Ring instance for type
commSemiringInst : Expr
CommSemiring instance for 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.
fieldInst? : Option Expr
Field instance for type if available.
addFn : Expr
mulFn : Expr
subFn : Expr
negFn : Expr
powFn : Expr
intCastFn : Expr
natCastFn : Expr
invFn? : Option Expr
Inverse if fieldInst? is some inst
one : 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
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.

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.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 Expr
AddRightCancel instance for type if available.
toQFn : Expr
addFn : Expr
mulFn : Expr
powFn : Expr
natCastFn : 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.

Instances For

source

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

Inhabited Semiring

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 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
steps : Nat

Instances For

source

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

Inhabited State

Equations

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