Grace/Cumulus/Algebra/Polynomial/Horner.g17

Open in Workbench Download source

Imports

Field.Algebraic

Declarations

Source

1-- Synthetic division for ascending coefficient lists over commutative rings.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.Horner8import Field.Algebraic910-- cs stores the lower coefficients; leading is the coefficient of X^length(cs).11def hornerAt {A : Set} (add mul leading x : Set) (cs : List(A)) : Set :=12  monicValue{A}(identity(A), add, mul, leading, x, cs)1314-- For c :: cs, division by X-a has lower coefficients given by this list.15def hornerQuotient {A : Set} (add mul leading a : Set) (cs : List(A)) → Set16  | add, mul, leading, a, List.nil => []17  | add, mul, leading, a, List.cons(c, tail) => hornerAt{A}(add, mul, leading, a, c :: tail) :: hornerQuotient(add, mul, leading, a, tail)18  descends cs1920theorem hornerAt.nil (A add mul leading x : Set)21  shows hornerAt{A}(add, mul, leading, x, []) = leading22proof23  unfold hornerAt24  rw monicValue25  rfl2627theorem hornerAt.cons (A add mul leading x c : Set) (cs : List(A))28  requires coefficient : c ∈ A29  shows hornerAt{A}(add, mul, leading, x, c :: cs) = call2(add, c, call2(mul, x, hornerAt{A}(add, mul, leading, x, cs)))30proof31  have value := identity.apply with coefficient32  unfold hornerAt33  rw [monicValue, value]34  rfl3536section Rings37variable (A add zero neg mul one leading : Set)38notation ring R := (A, add, zero, neg, mul, one)39hypothesis ring : IsCommRing(R)40hypothesis initial : leading ∈ R4142theorem hornerAt.closed (x : Set) (cs : List(A))43  requires element : x ∈ R44  shows hornerAt{A}(add, mul, leading, x, cs) ∈ R45proof46  have hom := IsRingHom.identity with ring47  unfold hornerAt48  exact hornerValue.closed with *4950theorem hornerQuotient.closed (a : Set) (cs : List(A))51  requires center : a ∈ R52  shows List(A, hornerQuotient{A}(add, mul, leading, a, cs))53proof54  induction cs55  | List.nil =>56    rw hornerQuotient57    typecheck58  | List.cons(c, tail) using ih =>59    have coefficient : c ∈ R by assumption60    have value := hornerAt.closed at A, add, zero, neg, mul, one, leading, a, c :: tail with *61    rw hornerQuotient62    typecheck6364theorem hornerQuotient.length (a : Set) (cs : List(A))65  requires center : a ∈ R66  shows length{A}(hornerQuotient{A}(add, mul, leading, a, cs)) = length{A}(cs)67proof68  induction cs69  | List.nil =>70    rw hornerQuotient71    rfl72  | List.cons(c, tail) using ih =>73    have coefficient : c ∈ R by assumption74    have value := hornerAt.closed at A, add, zero, neg, mul, one, leading, a, c :: tail with *75    have quotient := hornerQuotient.closed at A, add, zero, neg, mul, one, leading, a, tail with *76    rw [hornerQuotient, length.cons, length.cons, ih]77    rfl7879theorem hornerAt.synthetic_division (a x c : Set) (cs : List(A))80  requires center : a ∈ R81  requires element : x ∈ R82  requires coefficient : c ∈ R83  shows hornerAt{A}(add, mul, leading, x, c :: cs) = R[hornerAt{A}(add, mul, leading, a, c :: cs) + (x - a) * hornerAt{A}(add, mul, leading, x, hornerQuotient{A}(add, mul, leading, a, cs))]84proof85  induction cs generalizing c86  | List.nil =>87    intros c coefficient88    have empty : List(A, []) by typecheck89    rw [hornerQuotient, hornerAt.cons, hornerAt.cons, hornerAt.nil, hornerAt.nil]90    ring91  | List.cons(d, tail) using ih =>92    intros c coefficient93    have dIn : d ∈ R by assumption94    have quotient := hornerQuotient.closed at A, add, zero, neg, mul, one, leading, a, tail with *95    have valueA := hornerAt.closed at A, add, zero, neg, mul, one, leading, a, d :: tail with *96    have valueQ := hornerAt.closed at A, add, zero, neg, mul, one, leading, x, hornerQuotient{A}(add, mul, leading, a, tail) with *97    have previous := ih with d, dIn98    have outerX := hornerAt.cons at A, add, mul, leading, x, c, d :: tail with *99    have outerA := hornerAt.cons at A, add, mul, leading, a, c, d :: tail with *100    have quotientValue := hornerAt.cons at A, add, mul, leading, x, hornerAt{A}(add, mul, leading, a, d :: tail), hornerQuotient{A}(add, mul, leading, a, tail) with *101    rw [outerX, outerA, hornerQuotient, quotientValue, previous]102    ring103104end Rings105