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.
Performs trivial rewrites to transform polynomials into the form expected by the inference procedure. For instance, 0 is rewritten as C 0.
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.
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
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.
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
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
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