Polynomial

An extensible tactic for proving equality of polynomial expressions implemented using algebra. To add support for a new polynomial-like type, one needs to do three things:

• Implement a polynomial extension that lets polynomial infer the base ring from the algebraic type. For example:

@[polynomial_infer_base]
def polynomialInferBase : PolynomialExt where
  infer e := do
  match_expr e with
  | Polynomial R _ => pure R
  | _ => failure

• Tag any preprocessing lemmas with @[polynomial_pre]. This would include a lemma saying that C = algebraMap _ _ so that algebra knows how to normalize it.
• Tag any postprocessing lemmas with @[polynomial_post], so that polynomial_nf produces a pretty expression.

def Mathlib.Tactic.Polynomial.polynomialInferBase : PolynomialExt

Infer base ring for Polynomial R

Equations

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

theorem Mathlib.Tactic.Polynomial.monomial_eq_smul {R : Type u_2} [CommSemiring R] (a : R) (n : ℕ) : (Polynomial.monomial n) a = a • Polynomial.X ^ n

theorem Mathlib.Tactic.Polynomial.map_algebraMap {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] (r : R) : Polynomial.map (algebraMap R A) ((algebraMap R (Polynomial R)) r) = (algebraMap A (Polynomial A)) ((algebraMap R A) r)

def Mathlib.Tactic.Polynomial.preprocess (e : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

Run the polynomial_pre simpset to turn nonstandard spellings of algebraMap such as Polynomial.C into algebraMap

Equations

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

def Mathlib.Tactic.Polynomial.polynomial : Lean.ParserDescr

polynomial solves equalities of Polynomials and similar types.

Given a goal which is an equality in Polynomial R with a commutative ring R, polynomial turns both sides of the equation into a normal form by expanding out the brackets. It then closes the goal if both sides contain the same terms and fails otherwise. polynomial_nf normalizes all subexpressions at a given location.

Variants of polynomial include:

• polynomial: normalize both sides of an equation and close the goal if they are equal
• polynomial!: run polynomial at default transparency
• polynomial_nf: normalize all subexpression of the goal
• polynomial_nf at h₁ h₂ ⊢: normalize all subexpressions at hypotheses h₁ h₁ and the goal
• polynomial_nf at *: normalize all subexpressions of all local hypotheses and the goal
• polynomial_nf!: run polynomial_nf at default transparency

The polynomial tactic can be extended to work with algebras other than Polynomial using the attributes polynomial_infer_base, polynomial_pre and polynomial_post. This is only possible if the base ring can be inferred from the structure of the type.

Examples:

example (a : ℚ) : (X + C a) * (X - C a) = X^2 + C (a^2) := by polynomial

example {P : ℚ[X] → Prop} (h : P (X ^ 2 + X + C 4⁻¹)) : P ((X + C 2⁻¹) ^ 2) := by
  polynomial_nf at h ⊢
  exact h

Equations

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

def Mathlib.Tactic.Polynomial.tacticPolynomial! : Lean.ParserDescr

polynomial solves equalities of Polynomials and similar types.

Given a goal which is an equality in Polynomial R with a commutative ring R, polynomial turns both sides of the equation into a normal form by expanding out the brackets. It then closes the goal if both sides contain the same terms and fails otherwise. polynomial_nf normalizes all subexpressions at a given location.

Variants of polynomial include:

• polynomial: normalize both sides of an equation and close the goal if they are equal
• polynomial!: run polynomial at default transparency
• polynomial_nf: normalize all subexpression of the goal
• polynomial_nf at h₁ h₂ ⊢: normalize all subexpressions at hypotheses h₁ h₁ and the goal
• polynomial_nf at *: normalize all subexpressions of all local hypotheses and the goal
• polynomial_nf!: run polynomial_nf at default transparency

The polynomial tactic can be extended to work with algebras other than Polynomial using the attributes polynomial_infer_base, polynomial_pre and polynomial_post. This is only possible if the base ring can be inferred from the structure of the type.

Examples:

example (a : ℚ) : (X + C a) * (X - C a) = X^2 + C (a^2) := by polynomial

example {P : ℚ[X] → Prop} (h : P (X ^ 2 + X + C 4⁻¹)) : P ((X + C 2⁻¹) ^ 2) := by
  polynomial_nf at h ⊢
  exact h

Equations

• Mathlib.Tactic.Polynomial.tacticPolynomial! = Lean.ParserDescr.node `Mathlib.Tactic.Polynomial.tacticPolynomial! 1024 (Lean.ParserDescr.nonReservedSymbol "polynomial!" false)

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

A cleanup routine, which simplifies normalized expressions to a more human-friendly format. This is the algebra_nf cleanup routine with a little extra work to turn scalar multiplication into (MV)Polynomial.C

Equations

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

def Mathlib.Tactic.Polynomial.evalExprPoly (e : Lean.Expr) : AtomM Lean.Meta.Simp.Result

Normalize a polynomial expression into standard form. Used by polynomial_nf.

Equations

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

def Mathlib.Tactic.Polynomial.polynomialNF : Lean.ParserDescr

polynomial solves equalities of Polynomials and similar types.

Given a goal which is an equality in Polynomial R with a commutative ring R, polynomial turns both sides of the equation into a normal form by expanding out the brackets. It then closes the goal if both sides contain the same terms and fails otherwise. polynomial_nf normalizes all subexpressions at a given location.

Variants of polynomial include:

• polynomial: normalize both sides of an equation and close the goal if they are equal
• polynomial!: run polynomial at default transparency
• polynomial_nf: normalize all subexpression of the goal
• polynomial_nf at h₁ h₂ ⊢: normalize all subexpressions at hypotheses h₁ h₁ and the goal
• polynomial_nf at *: normalize all subexpressions of all local hypotheses and the goal
• polynomial_nf!: run polynomial_nf at default transparency

The polynomial tactic can be extended to work with algebras other than Polynomial using the attributes polynomial_infer_base, polynomial_pre and polynomial_post. This is only possible if the base ring can be inferred from the structure of the type.

Examples:

example (a : ℚ) : (X + C a) * (X - C a) = X^2 + C (a^2) := by polynomial

example {P : ℚ[X] → Prop} (h : P (X ^ 2 + X + C 4⁻¹)) : P ((X + C 2⁻¹) ^ 2) := by
  polynomial_nf at h ⊢
  exact h

Equations

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

def Mathlib.Tactic.Polynomial.tacticPolynomial_nf!_ : Lean.ParserDescr

polynomial solves equalities of Polynomials and similar types.

Given a goal which is an equality in Polynomial R with a commutative ring R, polynomial turns both sides of the equation into a normal form by expanding out the brackets. It then closes the goal if both sides contain the same terms and fails otherwise. polynomial_nf normalizes all subexpressions at a given location.

Variants of polynomial include:

• polynomial: normalize both sides of an equation and close the goal if they are equal
• polynomial!: run polynomial at default transparency
• polynomial_nf: normalize all subexpression of the goal
• polynomial_nf at h₁ h₂ ⊢: normalize all subexpressions at hypotheses h₁ h₁ and the goal
• polynomial_nf at *: normalize all subexpressions of all local hypotheses and the goal
• polynomial_nf!: run polynomial_nf at default transparency

The polynomial tactic can be extended to work with algebras other than Polynomial using the attributes polynomial_infer_base, polynomial_pre and polynomial_post. This is only possible if the base ring can be inferred from the structure of the type.

Examples:

example (a : ℚ) : (X + C a) * (X - C a) = X^2 + C (a^2) := by polynomial

example {P : ℚ[X] → Prop} (h : P (X ^ 2 + X + C 4⁻¹)) : P ((X + C 2⁻¹) ^ 2) := by
  polynomial_nf at h ⊢
  exact h

Equations

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