Grace/Cumulus/Algebra/Polynomial/CoefficientHorner.g17

Open in Workbench Download source

Imports

VariableExpansion · HornerHom

Declarations

• polynomialCoefficientFamily.list_representation theorem derivation
• polynomialVariableCoefficient.list_recover theorem derivation
• polynomialFromCoefficients def
• polynomialFromCoefficients.member theorem derivation
• polynomialFromCoefficients.nil theorem derivation
• polynomialFromCoefficients.cons theorem derivation
• polynomialAt.coefficient_horner theorem derivation

Source

1-- Finite coefficient lists and Horner evaluation with polynomial coefficients (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Polynomial.CoefficientHorner8import VariableExpansion9import HornerHom1011theorem polynomialCoefficientFamily.list_representation (I A z p j : Set)12  requires zeroIn : z ∈ A13  requires polynomial : p ∈ polynomials(I, A, z)14  requires index : j ∈ I15  shows ∃ cs, List(polynomials(I, A, z), cs) ∧ (∀ n, Nat(n) → listCoefficient{polynomials(I, A, z)}(constantFunction(monomials(I), A, z), cs, n) = polynomialVariableCoefficient(I, A, z, p, j, n))16proof17  have map := polynomialCoefficientFamily.map with *18  obtain ⟨cs, list, values⟩ := CoefficientMap.list_representation with map19  refine ⟨cs, list, ?_⟩20  intros n nNat21  have value := values with n, nNat22  have family := polynomialCoefficientFamily.value at I, A, z, p, j, n with *23  cc2425theorem polynomialVariableCoefficient.list_recover (I A z p j : Set)26  requires zeroIn : z ∈ A27  requires polynomial : p ∈ polynomials(I, A, z)28  requires index : j ∈ I29  shows ∃ cs, List(polynomials(I, A, z), cs) ∧ (∀ m ∈ monomials(I), listCoefficient{polynomials(I, A, z)}(constantFunction(monomials(I), A, z), cs, m(j))(coefficientErase(I, ℕ, 0, m, j)) = p(m))30proof31  obtain ⟨cs, list, values⟩ := polynomialCoefficientFamily.list_representation at I, A, z, p, j with *32  refine ⟨cs, list, ?_⟩33  intros m hm34  have natural := monomials.exponent with *35  have value := values with m(j), natural36  have recovery := polynomialVariableCoefficient.recover with *37  cc3839-- All coefficients, including the top one, occur in cs; the terminal value is zero.40def polynomialFromCoefficients (I A add z neg mul one j : Set) (cs : List(polynomials(I, A, z))) : Set :=41  hornerAt{polynomials(I, A, z)}(polynomialAdd(I, A, add, z, neg, mul, one), polynomialMul(I, A, add, z, neg, mul, one), constantFunction(monomials(I), A, z), polynomialVariable(I, A, z, one, j), cs)4243notation scoped polynomialFromCoefficients(I, R, j, cs) => polynomialFromCoefficients(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, j, cs)4445section Rings46variable (I A add z neg mul one j : Set)47notation ring R := (A, add, z, neg, mul, one)48notation ring P := R[I]49hypothesis ring : IsCommRing(R)5051theorem polynomialFromCoefficients.member (cs : List(polynomials(I, A, z)))52  shows polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, cs) ∈ P53proof54  have target : IsCommRing(P)55    exact polynomials.comm_ring with *56  have zeroIn : R[0] ∈ R by typecheck57  have oneIn : R[1] ∈ R by typecheck58  have initial : P[0] ∈ P by typecheck59  have variable := polynomialVariable.member at I, A, z, one, j with *60  unfold polynomialFromCoefficients61  exact hornerAt.closed with *6263theorem polynomialFromCoefficients.nil64  shows polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, []) = P[0]65proof66  unfold polynomialFromCoefficients67  exact hornerAt.nil with *6869theorem polynomialFromCoefficients.cons (c : Set) (cs : List(polynomials(I, A, z)))70  requires coefficient : c ∈ P71  shows polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, c :: cs) = P[c + polynomialVariable(I, R, j) * polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, cs)]72proof73  unfold polynomialFromCoefficients74  exact hornerAt.cons with *7576theorem polynomialAt.coefficient_horner (v : Set) (cs : List(polynomials(I, A, z)))77  requires assignment : v : I → R78  requires index : j ∈ I79  shows polynomialAt(I, R, v)(polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, cs)) = hornerAt{A}(add, mul, z, v(j), listMap{polynomials(I, A, z)}(polynomialAt(I, R, v), cs))80proof81  have source : IsCommRing(P)82    exact polynomials.comm_ring with *83  have hom : IsRingHom(polynomialAt(I, R, v), P, R)84    exact polynomialAt.hom with *85  have zeroIn : R[0] ∈ R by typecheck86  have oneIn : R[1] ∈ R by typecheck87  have initial : P[0] ∈ P by typecheck88  have variable := polynomialVariable.member at I, A, z, one, j with *89  have mapped := hornerAt.map at polynomials(I, A, z), polynomialAdd(I, A, add, z, neg, mul, one), constantFunction(monomials(I), A, z), polynomialNeg(I, A, add, z, neg, mul, one), polynomialMul(I, A, add, z, neg, mul, one), polynomialConstant(I, A, z, one), A, add, z, neg, mul, one, polynomialAt(I, R, v), constantFunction(monomials(I), A, z), polynomialVariable(I, R, j), cs with *90  have zeroValue := IsRingHom.zero with hom91  have variableValue := polynomialAt.variable with *92  unfold polynomialFromCoefficients93  rw [zeroValue, variableValue] at mapped94  cc9596end Rings97