Dependencies

Given a semiring \(R\) and a property of polynomials \(T:R[x] \to \mathtt{Type}\), nonsensitive inference of \(T\) for base cases of \(R[x]\) requires that we have the following.

• \(T(0)\)

• \(T(c)\) for \(c \in R\)

• \(T(x)\)

• \(T(x ^n)\) for \(n \in \mathbb {N}\)

The \(T(x ^n)\) case is not strictly necessary here and could have been analyzed as a result of recursive cases. However, \(T(x ^n)\) often has a nice closed form so it is included here for efficiency.

Given a semiring \(R\) and a property of polynomials \(T:R[x] \to \mathtt{Type}\), nonsensitive inference of \(T\) for recursive cases of \(R[x]\) requires that we have the following.

• \(T(p^n)\) given \(T(p)\) for \(p \in R[x]\) and \(n \in \mathbb {N}\)

• \(T(pq)\) given \(T(p)\) and \(T(q)\) for \(p,q \in R[x]\)

• \(T(p+q)\) given \(T(p)\) and \(T(q)\) for \(p,q \in R[x]\)

Given a semiring \(R[x]\) and a property of polynomials \(T:R[x] \to \mathtt{Type}\), inference of \(T\) for representations that support rewriting to a standard form requires the following.

• \(q \in R[x]\) given \(T(p)\) for \(p \in R[x]\) such that \(q = p\)

We say that a type \(t\) has a normal form if there is a set \(N \subseteq \{ m:t\} \) and an idempotent function \(f:t \to N\). Let \(m : t\). \(m\) is called normal if \(m \in N\). \(f(m)\) is called the normalization of \(m\).

Given a semiring \(R\) and a property of polynomials \(T:R[x] \to \mathtt{Type}\), inference of \(T\) for representations with a normal form requires that we have the following when equality in \(R\) is decidable.

• a normal form for \(T(p)\) for \(p \in R[x]\)

• DegreeEq\((p)\) given a normal \(T(p)\) for \(p \in R[x]\)

• LeadingCoeff\((p)\) given a normal \(T(p)\) for \(p \in R[x]\)

Given a semiring \(R\) and a property of polynomials \(T:R[x] \to \mathtt{Type}\), sensitive inference of \(T\) for base cases of \(R[x]\) requires that we have the following.

• \(T(0)\)

• \(T(c)\) for \(c \in R \setminus \{ 0\} \)

• \(T(x)\) when \(R\) is nontrivial

• and \(T(x ^n)\) for \(n \in \mathbb {N}\) when \(R\) is nontrivial

The \(T(x ^n)\) case is not strictly necessary here and could have been analyzed as a result of recursive cases. However, \(T(x ^n)\) often has a nice closed form so so it is included here for efficiency.

Given a semiring \(R\) and a property of polynomials \(T:R[x] \to \mathtt{Type}\), sensitive inference of \(T\) for recursive cases of \(R[x]\) requires that we have the following.

• \(T(p^n)\) given \(T(p)\) for \(p \in R[x]\) and \(n \in \mathbb {N}\) when \(\mathtt{leadingCoefficient}(p^n) \neq 0\)

• \(T(pq)\) given \(T(p)\) and \(T(q)\) for \(p,q \in R[x]\) when \(\mathtt{leadingCoefficient}(p)\mathtt{leadingCoefficient}(q) \neq 0\)

• \(T(p+q)\) given \(T(p)\) for \(p,q \in R[x]\) when \(\mathtt{degree}(p) {\gt} \mathtt{degree}(q)\)

• \(T(p+q)\) given \(T(q)\) for \(p,q \in R[x]\) when \(\mathtt{degree}(p) {\lt} \mathtt{degree}(q)\)

• \(T(p+q)\) given \(T(p)\) and \(T(q)\) for \(p,q \in R[x]\) when \(\mathtt{degree}(p) = \mathtt{degree}(q)\) and \(\mathtt{leadingCoefficient}(p) + \mathtt{leadingCoefficient}(q) \neq 0\)

Performs a depth-first search which, at each step, applies a provided helper tactic t then checks all instance declarations that match the current goal. Unlike Lean’s type-class inference, this procedure supports instance declarations that require assumptions that cannot be resolved by type-class instances, handling them with the helper tactic instead. The syntax is infer_instance_trying <:> t.

open Nat

class IsDouble (n : ℕ) where
  m : ℕ
  h : n = 2 * m

instance (h : n % 2 = 0) : IsDouble n :=
  ⟨n / 2, (Nat.mul_div_cancel' (dvd_of_mod_eq_zero h)).symm⟩

example : IsDouble 4 := by infer_instance_trying <:> decide

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.

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 \(\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{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

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.

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

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

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

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.