The algebra tactic

A suite of three tactics for solving equations in commutative algebras over commutative (semi)rings, where the exponents can also contain variables.

Based largely on the implementation of ring. The algebra normal form mirrors that of ring except that the constants are expressions in the base ring that are kept in ring normal form.

Organization

This tactic is implemented using the machinery of Ring.Common

• Normalized expressions are stored as an Common.ExSum, with a custom type for representing coefficients in R.
• While ring stores coefficients as rational numbers normalized by norm_num, algebra stores coefficients as experssions in the base ring R, normalized by ring.
• These coefficients are sums, not products. The normal form of a • x + b • x is (a + b) • x.

This tactic is used internally to implement the polynomial tactic.

Limitations

The main limitation of the current implementation is that it does not handle rational constants when the algebra A is a field but the base ring R is not. This is never an issue when working with polynomials, but would be an issue when working with a number field over its ring of integers.

When inferring the base ring, we assum that any two rings R and S that appear are comparable, in the sense that either R is an S-algebra or S is an R-algebra.

structure Mathlib.Tactic.Algebra.Cache {u : Lean.Level} {A : Q(Type u)} (sA : Q(CommSemiring «$A»)) extends Mathlib.Tactic.Ring.Common.Cache sA : Type

This cache contains typeclasses required during algebra's execution. These assumptions are stronger than ring because algebra occasionally requires commutativity to move between the base ring and the algebra.

• rα : Option Q(CommRing «$A»)
• dsα : Option Q(Semifield «$A»)
• czα : Option Q(CharZero «$A»)
• field : Option Q(Field «$A»)

  A Field instance on A, if available.

def Mathlib.Tactic.Algebra.mkCache {u : Lean.Level} {A : Q(Type u)} (sA : Q(CommSemiring «$A»)) : Lean.MetaM (Cache sA)

Create a new cache for A by doing the necessary instance searches.

inductive Mathlib.Tactic.Algebra.BaseType {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)} (sAlg : Q(Algebra «$R» «$A»)) (a : Q(«$A»)) : Type

The type used to store the coefficients of the algebra tactic, which are expressions in R kept in ring normal form and mapped into A by the algebraMap.

Note that these are sums, not products!

• mk {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)} {sAlg : Q(Algebra «$R» «$A»)} (r : Q(«$R»)) : Ring.ExSum q(«$sR») r → BaseType sAlg q((algebraMap «$R» «$A») «$r»)

def Mathlib.Tactic.Algebra.ExBase {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)} (sAlg : Q(Algebra «$R» «$A»)) (e : Q(«$A»)) : Type

ExBase BaseType sα e stores the structure of a normalized expression e, which appears as the base of an exponent expression e^n. The sum constructor is only used when the exponent n is not a constant.

def Mathlib.Tactic.Algebra.ExProd {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)} (sAlg : Q(Algebra «$R» «$A»)) (e : Q(«$A»)) : Type

ExProd BaseType sα e stores the structure of a normalized monomial expression e. A monomial here is a product of powers of ExBase expressions, terminated by a (nonzero) constant coefficient. The data of the constant coefficient is stored in the BaseType.

def Mathlib.Tactic.Algebra.ExSum {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)} (sAlg : Q(Algebra «$R» «$A»)) (e : Q(«$A»)) : Type

ExSum BaseType sα e stores the structure of a normalized polynomial expression e, which is a sum of monomials.

def Mathlib.Tactic.Algebra.evalCast {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)} (sAlg : Q(Algebra «$R» «$A»)) {a : Q(«$A»)} (cR : Cache q(«$sR»)) (cA : Cache q(«$sA»)) : Meta.NormNum.Result a → Option (Ring.Common.Result (ExSum sAlg) q(«$a»))

Evaluates a numeric literal in the algebra A by lifting it through the base ring R.

def Mathlib.Tactic.Algebra.pushCast (e : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

Push algebraMaps into sums and products and convert algebraMaps from ℕ, ℤ and ℚ into casts.

def Mathlib.Tactic.Algebra.evalSMulCast {u u' v : Lean.Level} {R : Q(Type u)} {R' : Q(Type u')} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)} (sAlg : Q(Algebra «$R» «$A»)) (smul : Q(SMul «$R'» «$A»)) (r' : Q(«$R'»)) : Lean.MetaM ((r : Q(«$R»)) × Q(∀ (a : «$A»), «$r» • a = «$r'» • a))

Handle scalar multiplication when the scalar ring R' doesn't match the base ring R. Assumes R is an R'-algebra (i.e., R' is smaller), and casts the scalar using algebraMap.

def Mathlib.Tactic.Algebra.RingCompute.add {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)} (sAlg : Q(Algebra «$R» «$A»)) (cR : Ring.Common.Cache sR) {a b : Q(«$A»)} (za : BaseType sAlg a) (zb : BaseType sAlg b) : Lean.MetaM (Ring.Common.Result (BaseType sAlg) q(«$a» + «$b») × Option Q(Meta.NormNum.IsNat («$a» + «$b») 0))

Evaluate the sum of two normalized expressions in R using ring.

def Mathlib.Tactic.Algebra.RingCompute.mul {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)} (sAlg : Q(Algebra «$R» «$A»)) (cR : Ring.Common.Cache sR) {a b : Q(«$A»)} (za : BaseType sAlg a) (zb : BaseType sAlg b) : Lean.MetaM (Ring.Common.Result (BaseType sAlg) q(«$a» * «$b»))

Evaluate the product of two normalized expressions in R using ring.

def Mathlib.Tactic.Algebra.RingCompute.cast {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)} (sAlg : Q(Algebra «$R» «$A»)) (cR : Cache sR) (u' : Lean.Level) (R' : Q(Type u')) : Q(CommSemiring «$R'») → (_smul : Q(SMul «$R'» «$A»)) → (r' : Q(«$R'»)) → AtomM ((y : Q(«$A»)) × Ring.Common.ExSum (BaseType sAlg) sA q(«$y») × Q(∀ (a : «$A»), «$r'» • a = «$y» * a))

Take an expression r' in a ring R' such that R is an R'-algebra and cast r' to R using algebraMap R' R, so that the scalar multiplication action on A is preserved.

def Mathlib.Tactic.Algebra.RingCompute.neg {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)} (sAlg : Q(Algebra «$R» «$A»)) (cR : Cache sR) {a : Q(«$A»)} (_rA : Q(CommRing «$A»)) (za : BaseType sAlg a) : Lean.MetaM (Ring.Common.Result (BaseType sAlg) q(-«$a»))

Evaluate the product of two normalized expressions in R using ring.

def Mathlib.Tactic.Algebra.RingCompute.pow {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)} (sAlg : Q(Algebra «$R» «$A»)) (cR : Ring.Common.Cache sR) {a : Q(«$A»)} {b : Q(ℕ)} (za : BaseType sAlg a) (vb : Ring.Common.ExProdNat q(«$b»)) : OptionT Lean.MetaM (Ring.Common.Result (BaseType sAlg) q(«$a» ^ «$b»))

Raise a normalized expression in R to the power of a normalized natural number expression using ring.

def Mathlib.Tactic.Algebra.RingCompute.inv {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)} (sAlg : Q(Algebra «$R» «$A»)) (cR : Cache sR) {a : Q(«$A»)} : Option Q(CharZero «$A») → (fA : Q(Semifield «$A»)) → (za : BaseType sAlg a) → AtomM (Option (Ring.Common.Result (BaseType sAlg) q(«$a»⁻¹)))

Evaluate the inverse of two normalized expressions in R using ring.

def Mathlib.Tactic.Algebra.RingCompute.derive {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)} (sAlg : Q(Algebra «$R» «$A»)) (cR : Cache sR) (cA : Cache sA) (x : Q(«$A»)) : Lean.MetaM (Ring.Common.Result (Ring.Common.ExSum (BaseType sAlg) sA) q(«$x»))

Evaluate constants in A using norm_num.

def Mathlib.Tactic.Algebra.RingCompute.isOne {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)} (sAlg : Q(Algebra «$R» «$A»)) (cR : Ring.Common.Cache sR) {x : Q(«$A»)} (zx : BaseType sAlg x) : Option Q(Meta.NormNum.IsNat «$x» 1)

Decide if a coefficient is 1.

def Mathlib.Tactic.Algebra.ringCompare {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)} (sAlg : Q(Algebra «$R» «$A»)) : Ring.Common.RingCompare (BaseType sAlg)

The data used by the algebra tactic to normalize the constant coefficients, which are expressions in R normalized by ring.

def Mathlib.Tactic.Algebra.ringCompute {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)} (sAlg : Q(Algebra «$R» «$A»)) (cR : Cache sR) (cA : Cache sA) : Ring.Common.RingCompute (BaseType sAlg) sA

The data used by the algebra tactic to normalize the constant coefficients, which are expressions in R normalized by ring.

theorem Mathlib.Tactic.Algebra.Nat.cast_eq_algebraMap (A : Type u_1) [CommSemiring A] (n : ℕ) : ↑n = (algebraMap ℕ A) n

theorem Mathlib.Tactic.Algebra.Nat.algebraMap_eq_cast (A : Type u_1) [CommSemiring A] (n : ℕ) : (algebraMap ℕ A) n = ↑n

theorem Mathlib.Tactic.Algebra.Int.cast_eq_algebraMap (A : Type u_1) [CommRing A] (n : ℤ) : ↑n = (algebraMap ℤ A) n

theorem Mathlib.Tactic.Algebra.Int.algebraMap_eq_cast (A : Type u_1) [CommRing A] (n : ℤ) : (algebraMap ℤ A) n = ↑n

def Mathlib.Tactic.Algebra.preprocess (mvarId : Lean.MVarId) : Lean.MetaM Lean.MVarId

Remove some nonstandard spellings of algebraMap such as Nat.cast

def Mathlib.Tactic.Algebra.cleanupSMul (cfg : RingNF.Config) (r : Lean.Meta.Simp.Result) : Lean.MetaM Lean.Meta.Simp.Result

Clean up the normal form into a more human-friendly format. This does everything RingNF.cleanup does and also pulls the scalar multiplication from the end of of each term to the start. i.e. x * y * (r • 1) → r • (x * y) Used by cleanup.

def Mathlib.Tactic.Algebra.cleanupConsts (cfg : RingNF.Config) (r : Lean.Meta.Simp.Result) : Lean.MetaM Lean.Meta.Simp.Result

Turn scalar multiplication by an explicit constant in R into multiplication in A.

e.g. (4 : ℚ) • x becomes 4 * x but ↑n • x stays ↑n • x.

partial def Mathlib.Tactic.Algebra.collectScalarRingsAux (e : Lean.Expr) : StateT (List Lean.Expr) Lean.MetaM Unit

Collect all scalar rings from scalar multiplications using a state monad for performance.

Note: The match in this definition should be kept up to date with the Common.eval function.

def Mathlib.Tactic.Algebra.collectScalarRings (e : Lean.Expr) : Lean.MetaM (List Lean.Expr)

Collect all scalar rings from scalar multiplications and algebraMap applications in the expression.

def Mathlib.Tactic.Algebra.pickLargerRing (r1 r2 : (u : Lean.Level) × Q(Type u)) : Lean.MetaM ((u : Lean.Level) × Q(Type u))

Given two rings, determine which is 'larger' in the sense that the larger is an algebra over the smaller. Returns the first ring if they're the same or incompatible.

def Mathlib.Tactic.Algebra.inferBase {v : Lean.Level} {A : Q(Type v)} {sA : Q(CommSemiring «$A»)} (ca : Cache q(«$sA»)) (e : Lean.Expr) : Lean.MetaM ((u : Lean.Level) × Q(Type u))

Infer from the expression what base ring the normalization should use. Finds all scalar rings in the expression and picks the 'larger' one in the sense that it is an algebra over the smaller rings.

def Mathlib.Tactic.Algebra.proveEq (base : Option ((u : Lean.Level) × Q(Type u))) (g : Lean.MVarId) : AtomM Unit

Frontend of algebra: attempt to close a goal g, assuming it is an equation of semirings.

def Mathlib.Tactic.Algebra.algebra : Lean.ParserDescr

algebra solves equalities in the language of algebras: ring operations and scalar multiplications.

Given a goal which is an equality in a commutative R-algebra A, algebra parses the LHS and RHS of the goal as polynomial expressions of A-atoms with coefficients in some semiring R, and closes the goal if the two expressions are the same. The R-coefficients are put into ring normal form.

By default, the scalar ring R is inferred automatically by looking for scalar multiplications and algebraMaps present in the expressions. The inference procedure assumes that any two rings R and S that appear are comparable, in the sense that either R is an S-algebra or S is an R-algebra.

• algebra with R uses the term R as the scalar ring, instead of attempting to infer it automatically.

def Mathlib.Tactic.Algebra.algebraWith : Lean.ParserDescr

algebra solves equalities in the language of algebras: ring operations and scalar multiplications.

Given a goal which is an equality in a commutative R-algebra A, algebra parses the LHS and RHS of the goal as polynomial expressions of A-atoms with coefficients in some semiring R, and closes the goal if the two expressions are the same. The R-coefficients are put into ring normal form.

By default, the scalar ring R is inferred automatically by looking for scalar multiplications and algebraMaps present in the expressions. The inference procedure assumes that any two rings R and S that appear are comparable, in the sense that either R is an S-algebra or S is an R-algebra.

• algebra with R uses the term R as the scalar ring, instead of attempting to infer it automatically.