Grace/Cumulus/Algebra/Polynomial/HornerTranslation.g17

Open in Workbench Download source

Imports

HornerArithmetic

Declarations

Source

1-- Constructive translation of coefficient lists, preserving their leading term (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.HornerTranslation8import HornerArithmetic910def hornerTranslate {A : Set} (add mul one leading a : Set) (cs : List(A)) → Set11  | add, mul, one, leading, a, List.nil => []12  | add, mul, one, leading, a, List.cons(c, tail) => hornerAffineProduct{A}(add, mul, leading, a, one, c, hornerTranslate(add, mul, one, leading, a, tail))13  descends cs1415section Rings16variable (A add zero neg mul one leading a : Set)17notation ring R := (A, add, zero, neg, mul, one)18hypothesis ring : IsCommRing(R)19hypothesis initial : leading ∈ R20hypothesis center : a ∈ R2122theorem hornerTranslate.data (cs : List(A))23  shows List(A, hornerTranslate{A}(add, mul, one, leading, a, cs)) ∧ length{A}(hornerTranslate{A}(add, mul, one, leading, a, cs)) = length{A}(cs)24proof25  induction cs26  | List.nil =>27    rw hornerTranslate28    constructor29    . typecheck30    . rfl31  | List.cons(c, tail) using ih =>32    have coefficient : c ∈ R by assumption33    have unit : R[1] ∈ R by typecheck34    have data := hornerAffineProduct.data at A, add, zero, neg, mul, one, leading, a, one, c, hornerTranslate{A}(add, mul, one, leading, a, tail) with *35    rw hornerTranslate36    constructor37    . exact data.left38    . rw [data.right, ih.right, length.cons]39      rfl4041theorem hornerTranslate.affine_value (x c : Set) (ds : List(A))42  requires element : x ∈ R43  requires coefficient : c ∈ R44  shows hornerAt{A}(add, mul, leading, x, hornerAffineProduct{A}(add, mul, leading, a, one, c, ds)) = R[c + (a + x) * hornerAt{A}(add, mul, leading, x, ds)]45proof46  have hom := IsRingHom.identity with ring47  have unit : R[1] ∈ R by typecheck48  have terminal : R[1 * leading] = leading by ring49  have leadingValue := identity.apply with initial50  have centerValue := identity.apply with center51  have unitValue := identity.apply with unit52  have coefficientValue := identity.apply with coefficient53  have expansion : monicValue{A}(identity(A), add, mul, identity(A)(R[1 * leading]), x, hornerAffineProduct{A}(add, mul, leading, a, one, c, ds)) = R[identity(A)(c) + (identity(A)(a) + identity(A)(one) * x) * monicValue{A}(identity(A), add, mul, identity(A)(leading), x, ds)]54    exact hornerAffineProduct.map_value with *55  rw [terminal, leadingValue, centerValue, unitValue, coefficientValue] at expansion56  have oneTimes : R[1 * x] = x by ring57  rw oneTimes at expansion58  simp [hornerAt]5960theorem hornerTranslate.value (x : Set) (cs : List(A))61  requires element : x ∈ R62  shows hornerAt{A}(add, mul, leading, x, hornerTranslate{A}(add, mul, one, leading, a, cs)) = hornerAt{A}(add, mul, leading, R[a + x], cs)63proof64  induction cs65  | List.nil =>66    rw [hornerTranslate, hornerAt.nil, hornerAt.nil]67    rfl68  | List.cons(c, tail) using ih =>69    have coefficient : c ∈ R by assumption70    have data := hornerTranslate.data at A, add, zero, neg, mul, one, leading, a, tail with *71    have expansion := hornerTranslate.affine_value at A, add, zero, neg, mul, one, leading, a, x, c, hornerTranslate{A}(add, mul, one, leading, a, tail) with *72    rw [hornerTranslate, expansion, ih, hornerAt.cons]73    rfl7475theorem hornerAt.at_zero (cs : List(A))76  shows hornerAt{A}(add, mul, leading, zero, cs) = listHeadOr{A}(leading, cs)77proof78  induction cs79  | List.nil =>80    rw [hornerAt.nil, listHeadOr]81    rfl82  | List.cons(c, tail) using ih =>83    have coefficient : c ∈ R by assumption84    have zeroIn : R[0] ∈ R by typecheck85    have rest := hornerAt.closed at A, add, zero, neg, mul, one, leading, zero, tail with *86    rw [hornerAt.cons, listHeadOr]87    ring8889theorem hornerTranslate.constant (cs : List(A))90  shows listHeadOr{A}(leading, hornerTranslate{A}(add, mul, one, leading, a, cs)) = hornerAt{A}(add, mul, leading, a, cs)91proof92  have zeroIn : R[0] ∈ R by typecheck93  have data := hornerTranslate.data at A, add, zero, neg, mul, one, leading, a, cs with *94  have translated := hornerTranslate.value at A, add, zero, neg, mul, one, leading, a, zero, cs with *95  have constant := hornerAt.at_zero at A, add, zero, neg, mul, one, leading, a, hornerTranslate{A}(add, mul, one, leading, a, cs) with *96  have centerAtZero : R[a + 0] = a by ring97  rwa [constant, centerAtZero] at translated9899end Rings100