PolynomialCoefficientLists

Finite lists of polynomial coefficients and their evaluation in Horner form

Open in Workbench View on GitHub

1-- Finite lists of polynomial coefficients and their evaluation in Horner form.2-- Part of the Grace17 examples.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module PolynomialCoefficientLists8import Grace.Cumulus.Algebra.Polynomial.CoefficientHorner910section Polynomials11variable (I A add z neg mul one j : Set)12notation ring R := (A, add, z, neg, mul, one)13notation ring P := R[I]14hypothesis ring : IsCommRing(R)1516theorem coefficient_list (p : Set)17  requires polynomial : p ∈ P18  requires index : j ∈ I19  shows ∃ cs, List(P, cs) ∧ (∀ n, Nat(n) → listCoefficient{P}(P[0], cs, n) = polynomialVariableCoefficient(I, R, p, j, n))20proof21  have zeroIn : R[0] ∈ R by typecheck22  exact polynomialCoefficientFamily.list_representation with *2324theorem horner_is_polynomial (cs : List(P))25  shows polynomialFromCoefficients(I, R, j, cs) ∈ P26proof27  exact polynomialFromCoefficients.member with *2829theorem evaluate_horner (v : Set) (cs : List(P))30  requires assignment : v : I → R31  requires index : j ∈ I32  shows polynomialAt(I, R, v)(polynomialFromCoefficients(I, R, j, cs)) = hornerAt{A}(add, mul, z, v(j), listMap{P}(polynomialAt(I, R, v), cs))33proof34  exact polynomialAt.coefficient_horner with *3536end Polynomials37