3 Univariate System

3.1 Inference Rules

We define type classes that declare groups of inference rules. These classes may be extended to construct specifications for inference procedures requiring assumptions of varying strenghts (e.g. from nonsensitive to very sensitive). An implementation of an inference procudure must meet its specificaitions by implementing its inference rules.

Because we differentiate between inference rules for bases cases and inference rules for recursive cases of polynomials, inference procedures may be sensitive to varying degrees. To demonstrate:

• Nonsensitive: greedy degree upper bound inference is nonsensitive as it never requires additional assumptions beyond the input instances

• Somewhat sensitive: leading coefficient inference is sensitive in recursive cases but nonsensitive in base cases

• Very sensitive: exact degree inference is sensitive as it always requires additional assumptions beyond the input instances

It should also be emphasized that when we assert that we require some type in the following definitions, we mean that we must be provided a way to compute a member of that type, not just that such a member exists, given the current assumptions as input.

Many useful representations have a simplified or normal form when different members of that representation are equivalent up to the target property. For instance, lists of polynomial coefficients are equivalent up to trailing zeros and can typically be simplified to an equivalent normal form with no trailing zeros. In this case, degrees and leading coefficients are easily computed from a normal form, which is reflected in Definition 3.6.

It is also often useful to rewrite a polynomial in a standard form defined by the representation, such as with expanded and ordered terms for example.

3.2 Reflection Classes

TODO (see Polynomial/Defs.lean)

3.3 Representations

TODO (see Polynomial/CoeffList.lean)

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.

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

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.

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

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.

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

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

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