Automate Polynomial: An Experiment in Reflection for Polynomials

3 Univariate System

3.1 Inference Rules

TODO

3.2 Reflection Classes

TODO

3.3 Representations

TODO

3.4 Tactics

3.4.1 Utility tactics

Utility tactics perform useful rewriting and last-mile simplification steps. They appear frequently in those reflection tactics that perform the inference procedure.

Tactic 3.1 poly_rfl_rw
#

Performs trivial rewrites to transform polynomials into the form expected by the inference procedure. For instance, 0 is rewritten as C 0.

Tactic 3.2 poly_rfl_dsimp
#

Simplifies the expression resulting from the inference procedure so that the computable representation is visible. This consists primarily of unfolding reflection class instances into the values they contain.

Tactic 3.3 poly_rfl_with
#

Frames a reflection tactic t with rewriting and last-mile simplification steps from Tactic 3.1 and Tactic 3.2. The syntax is poly_rfl_with <:> t.

Tactic 3.4 poly_infer_try
#

For use as a helper tactic in the sensitive inference procedure (see Tactic 2.1). Invokes Tactic 3.2 to unfold the expression resulting from the previous step of the sensitive inference procedure, preparing the goal for the next step.

3.4.2 Reflection tactics

Reflection tactics perform the inference procedure to resolve target goals by transforming them so that they can be resolved with last-mile automation tactics such as trivial, simp, and norm_num. The code samples are adapted from Demo/Polynomial.lean and rely on the following preamble.

import AutomatePolynomial.Reflection.Polynomial.Basic
open Polynomial Rfl
Tactic 3.5 poly_rfl_degree_le
#

Resolves goals of the form \(\mathtt{degree}(p) \leq n\) for univariate polynomials \(p\) and some \(n\) which is either a natural number or the bottom member \(\bot \).

section DegreeLe
variable [Semiring R]
example : (0     : R[X]).degree   := by poly_rfl_degree_le; trivial
example : (1     : R[X]).degree  0 := by poly_rfl_degree_le; trivial
example : (X     : R[X]).degree  1 := by poly_rfl_degree_le; trivial
example : (X ^ 2 : R[X]).degree  2 := by poly_rfl_degree_le; trivial
example : (X + 1 : R[X]).degree  1 := by poly_rfl_degree_le; trivial
end DegreeLe

Since the following tactics deal with properties that depend on whether leading terms cancel—degrees and leading coefficients—they will rely on the sensitive inference procedure (see Section 2.3) in cases where the polynomial contains recursive cases such as +, *, or ^ (disregarding X ^ n which is handled separately). Tactics with the suffix _trying perform the sensitive inference procedure to handle these cases. Alternatively, the sensitive inference procedure may be avoided by instead infering the coefficients of the polynomial and then deriving the target property from that. Tactics with the suffix _of_coeffs use this alternative when provided the the target representation of the coefficients, such as CoeffsList.

Resolves goals of the form \(\mathtt{degree}(p) = n\) for univariate polynomials \(p\) and some \(n\) which is either a natural number or the bottom member \(\bot \). In any case where we want \(\mathtt{degree}(p) \neq \bot \), we must admit that the the semiring is nontrivial, as in section DegreeEqNontrivial.

section DegreeEq
variable [Semiring R]
example : (0 : R[X]).degree =  := by poly_rfl_degree_eq
end DegreeEq

section DegreeEqNontrivial
variable [Semiring R] [Nontrivial R]
example : (1     : R[X]).degree = 0 := by poly_rfl_degree_eq
example : (X     : R[X]).degree = 1 := by poly_rfl_degree_eq
example : (X ^ 2 : R[X]).degree = 2 := by poly_rfl_degree_eq
example : (X + 1 : R[X]).degree = 1 := by poly_rfl_degree_eq_trying <:> poly_infer_try
end DegreeEqNontrivial

section DegreeEqOfCoeffs
example : (X + 1 : [X]).degree = 1 := by poly_rfl_degree_eq_of_coeffs VIA CoeffsList; simp; trivial
end DegreeEqOfCoeffs

Resolves goals of the form \(\mathtt{leadingCoefficient}(p) = c\) for univariate polynomials \(p\) and members of the relevant semiring \(c\). When the definition of \(p\) contains recursive cases such as +, *, or ^ (disregarding X ^ n which is handled separately), we must admit that the semiring is nontrivial, as in section LeadingCoeffNontrivial.

section LeadingCoeff
variable [Semiring R]
example : (0     : R[X]).leadingCoeff = 0 := by poly_rfl_leading_coeff
example : (1     : R[X]).leadingCoeff = 1 := by poly_rfl_leading_coeff
example : (X     : R[X]).leadingCoeff = 1 := by poly_rfl_leading_coeff
example : (X ^ 2 : R[X]).leadingCoeff = 1 := by poly_rfl_leading_coeff
end LeadingCoeff

section LeadingCoeffNontrivial
variable [Semiring R] [Nontrivial R]
example : (X + 1 : R[X]).leadingCoeff = 1 := by poly_rfl_leading_coeff_trying <:> poly_infer_try
end LeadingCoeffNontrivial

section LeadingCoeffEqOfCoeffs
example : (X + 1 : [X]).leadingCoeff = 1 := by poly_rfl_leading_coeff_of_coeffs VIA CoeffsList; simp
end LeadingCoeffEqOfCoeffs

The remaining tactics are generic to the representation of the target property and require the user to provide the target representation, such as CoeffsList or EvalArrow.

Tactic 3.8 poly_rfl_coeff
#

Resolves goals of the form \(\mathtt{nthCoefficient}_n(p) = c\) for univariate polynomials \(p\), natural numbers \(n\), and members of the relevant semiring \(c\). Note that we admit that the semiring is commutative.

section Coeffs
variable [CommSemiring R]
example : (0     : R[X]).coeff 1 = 0 := by poly_rfl_coeff VIA CoeffsList
example : (1     : R[X]).coeff 1 = 0 := by poly_rfl_coeff VIA CoeffsList; trivial
example : (X     : R[X]).coeff 1 = 1 := by poly_rfl_coeff VIA CoeffsList; trivial
example : (X ^ 2 : R[X]).coeff 1 = 0 := by poly_rfl_coeff VIA CoeffsList; trivial
example : (X + 1 : R[X]).coeff 1 = 1 := by poly_rfl_coeff VIA CoeffsList; simp
end Coeffs
Tactic 3.9 poly_rfl_eval
#

Resolves goals of the form \(p(c) = c'\) for univariate polynomials \(p\) and members of the relevant semiring \(c\) and \(c'\). Note that we admit that the semiring is commutative.

section Eval
variable [CommSemiring R]
example : (0     : R[X]).eval 1 = 0 := by poly_rfl_eval VIA EvalArrow
example : (1     : R[X]).eval 1 = 1 := by poly_rfl_eval VIA EvalArrow
example : (X     : R[X]).eval 1 = 1 := by poly_rfl_eval VIA EvalArrow
example : (X ^ 2 : R[X]).eval 1 = 1 := by poly_rfl_eval VIA EvalArrow; simp
example : (X + 1 : R[X]).eval 1 = 2 := by poly_rfl_eval VIA EvalArrow; norm_num
end Eval
Tactic 3.10 poly_rfl_expand
#

Resolves goals of the form \(p = q\) for a univariate polynomial \(p\) and an equivalent polynomial \(q\) in expanded form. Note that we admit that the semiring is commutative.

section Expand
variable [CommSemiring R]
example : (C 2 + X : R[X]) = X + C 2 := by poly_rfl_expand VIA CoeffsList; simp; poly_unfold_expand; simp
example : (X * C 2 : R[X]) = C 2 * X := by poly_rfl_expand VIA CoeffsList; simp; poly_unfold_expand; simp
example : (X + X   : R[X]) = C 2 * X := by poly_rfl_expand VIA CoeffsList; simp; poly_unfold_expand; norm_num
end Expand