Grace/Cumulus/Algebra/Polynomial/HornerArithmetic.g17

Open in Workbench Download source

Imports

HornerExtension

Declarations

Source

1-- Fixed-length Horner arithmetic with tracked terminal 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.HornerArithmetic8import HornerExtension910-- carry + (b+dX)H(leading,cs); the terminal coefficient becomes d*leading.11def hornerAffineProduct {A : Set} (add mul leading b d carry : Set) (cs : List(A)) → Set12  | add, mul, leading, b, d, carry, List.nil => [call2(add, carry, call2(mul, b, leading))]13  | add, mul, leading, b, d, carry, List.cons(c, tail) => call2(add, carry, call2(mul, b, c)) :: hornerAffineProduct(add, mul, leading, b, d, call2(mul, d, c), tail)14  descends cs1516-- Equal-length inputs add without padding or changing the declared degree.17def hornerAdd {A : Set} (add z : Set) (cs ds : List(A)) → Set18  | add, z, List.nil, ds => []19  | add, z, List.cons(c, tail), ds => call2(add, c, listHeadOr{A}(z, ds)) :: hornerAdd(add, z, tail, listTail{A}(ds))20  descends cs2122def hornerScale {A : Set} (mul a : Set) (cs : List(A)) → Set23  | mul, a, List.nil => []24  | mul, a, List.cons(c, tail) => call2(mul, a, c) :: hornerScale(mul, a, tail)25  descends cs2627theorem listHeadOr.closed (A z : Set) (xs : List(A))28  requires zeroIn : z ∈ A29  shows listHeadOr{A}(z, xs) ∈ A30proof31  induction xs32  | List.nil =>33    rwa listHeadOr34  | List.cons(c, tail) using ih =>35    rwa listHeadOr3637section Lists38variable (A add zero neg mul one : Set)39notation ring R := (A, add, zero, neg, mul, one)40hypothesis ring : IsCommRing(R)4142theorem hornerAffineProduct.data (leading b d carry : Set) (cs : List(A))43  requires initial : leading ∈ R44  requires constant : b ∈ R45  requires slope : d ∈ R46  requires carried : carry ∈ R47  shows List(A, hornerAffineProduct{A}(add, mul, leading, b, d, carry, cs)) ∧48    length{A}(hornerAffineProduct{A}(add, mul, leading, b, d, carry, cs)) = succ(length{A}(cs))49proof50  induction cs generalizing carry51  | List.nil =>52    intros carry carried53    have ordinary := IsCommRing.ring with ring54    have product := IsRing.mul_closed with ordinary, constant, initial55    have head := IsRing.add_closed with ordinary, carried, product56    have empty : List(A, []) by typecheck57    rw hornerAffineProduct58    constructor59    . typecheck60    . rw [length.cons, length.nil]61      rfl62  | List.cons(c, tail) using ih =>63    intros carry carried64    have coefficient : c ∈ R by assumption65    have ordinary := IsCommRing.ring with ring66    have product := IsRing.mul_closed with ordinary, constant, coefficient67    have head := IsRing.add_closed with ordinary, carried, product68    have next := IsRing.mul_closed with ordinary, slope, coefficient69    have previous := ih with R[d * c], next70    rw hornerAffineProduct71    constructor72    . typecheck73    . rw [length.cons, previous.right, length.cons]74      rfl7576theorem hornerAdd.data (cs ds : List(A))77  shows List(A, hornerAdd{A}(add, zero, cs, ds)) ∧ length{A}(hornerAdd{A}(add, zero, cs, ds)) = length{A}(cs)78proof79  induction cs generalizing ds80  | List.nil =>81    intros ds dsList82    rw hornerAdd83    constructor84    . typecheck85    . rfl86  | List.cons(c, tail) using ih =>87    intros ds dsList88    have coefficient : c ∈ R by assumption89    have ordinary := IsCommRing.ring with ring90    have zeroIn := IsRing.zero_in_carrier with ordinary91    have other := listHeadOr.closed at A, zero, ds with *92    have head := IsRing.add_closed with ordinary, coefficient, other93    have rest := listTail.closed at A, ds with *94    have previous := ih with listTail{A}(ds), rest95    rw hornerAdd96    constructor97    . typecheck98    . rw [length.cons, previous.right, length.cons]99      rfl100101theorem hornerScale.data (a : Set) (cs : List(A))102  requires scalar : a ∈ R103  shows List(A, hornerScale{A}(mul, a, cs)) ∧ length{A}(hornerScale{A}(mul, a, cs)) = length{A}(cs)104proof105  induction cs106  | List.nil =>107    rw hornerScale108    constructor109    . typecheck110    . rfl111  | List.cons(c, tail) using ih =>112    have coefficient : c ∈ R by assumption113    have ordinary := IsCommRing.ring with ring114    have head := IsRing.mul_closed with ordinary, scalar, coefficient115    rw hornerScale116    constructor117    . typecheck118    . rw [length.cons, ih.right, length.cons]119      rfl120121end Lists122123section Extensions124variable (A add zero neg mul one B plus z minus times unit f x : Set)125notation ring R := (A, add, zero, neg, mul, one)126notation ring S := (B, plus, z, minus, times, unit)127hypothesis source : IsCommRing(R)128hypothesis target : IsCommRing(S)129hypothesis hom : IsRingHom(f, R, S)130hypothesis element : x ∈ S131132theorem hornerAffineProduct.map_value (leading b d carry : Set) (cs : List(A))133  requires initial : leading ∈ R134  requires constant : b ∈ R135  requires slope : d ∈ R136  requires carried : carry ∈ R137  shows monicValue{A}(f, plus, times, f(R[d * leading]), x, hornerAffineProduct{A}(add, mul, leading, b, d, carry, cs)) =138    S[f(carry) + (f(b) + f(d) * x) * monicValue{A}(f, plus, times, f(leading), x, cs)]139proof140  induction cs generalizing carry141  | List.nil =>142    intros carry carried143    have ordinary := IsCommRing.ring with source144    have product := IsRing.mul_closed with ordinary, constant, initial145    have head := IsRing.add_closed with ordinary, carried, product146    have fcarry := IsRingHom.closed with hom, carried147    have fb := IsRingHom.closed with hom, constant148    have fd := IsRingHom.closed with hom, slope149    have fl := IsRingHom.closed with hom, initial150    have sum := IsRingHom.add with hom, carried, product151    have productB := IsRingHom.mul with hom, constant, initial152    have productD := IsRingHom.mul with hom, slope, initial153    rw [hornerAffineProduct, monicValue, monicValue, monicValue, sum, productB, productD]154    ring155  | List.cons(c, tail) using ih =>156    intros carry carried157    have coefficient : c ∈ R by assumption158    have ordinary := IsCommRing.ring with source159    have product := IsRing.mul_closed with ordinary, constant, coefficient160    have head := IsRing.add_closed with ordinary, carried, product161    have next := IsRing.mul_closed with ordinary, slope, coefficient162    have previous := ih with R[d * c], next163    have rest := hornerAffineProduct.data at A, add, zero, neg, mul, one, leading, b, d, R[d * c], tail with *164    have initialImage := IsRingHom.closed with hom, initial165    have tailValue := hornerValue.closed at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, f(leading), tail with *166    have fcarry := IsRingHom.closed with hom, carried167    have fb := IsRingHom.closed with hom, constant168    have fd := IsRingHom.closed with hom, slope169    have fc := IsRingHom.closed with hom, coefficient170    have sum := IsRingHom.add with hom, carried, product171    have productB := IsRingHom.mul with hom, constant, coefficient172    have productD := IsRingHom.mul with hom, slope, coefficient173    have outer := hornerValue.cons at A, f, plus, times, f(R[d * leading]), x, R[carry + b * c], hornerAffineProduct{A}(add, mul, leading, b, d, R[d * c], tail) with *174    have original := hornerValue.cons at A, f, plus, times, f(leading), x, c, tail with *175    rw [hornerAffineProduct, outer, original, previous, sum, productB, productD]176    ring177178theorem hornerAdd.map_value (a b : Set) (cs ds : List(A))179  requires left : a ∈ R180  requires right : b ∈ R181  requires sameLength : length{A}(cs) = length{A}(ds)182  shows monicValue{A}(f, plus, times, f(R[a + b]), x, hornerAdd{A}(add, zero, cs, ds)) =183    S[monicValue{A}(f, plus, times, f(a), x, cs) + monicValue{A}(f, plus, times, f(b), x, ds)]184proof185  induction cs generalizing ds186  | List.nil =>187    intros ds dsList sameLength188    have shape := List.cases with *189    cases shape with empty | nonempty190    . rw [empty, hornerAdd, monicValue, monicValue, monicValue]191      exact IsRingHom.add with hom, left, right192    . obtain ⟨e, he, rest, restList, equal⟩ := nonempty193      rw [equal, length.nil, length.cons] at sameLength194      exfalso195      exact Naturals.disjoint.zero.succ at length{A}(rest) with sameLength196  | List.cons(c, tail) using ih =>197    intros ds dsList sameLength198    have coefficient : c ∈ R by assumption199    have shape := List.cases at A, ds with *200    cases shape with empty | nonempty201    . rw [empty, length.cons, length.nil] at sameLength202      have impossible : (0 : Nat) = succ(length{A}(tail)) by cc203      exfalso204      exact Naturals.disjoint.zero.succ at length{A}(tail) with impossible205    . obtain ⟨e, he, rest, restList, equal⟩ := nonempty206      rw [equal, length.cons, length.cons] at sameLength207      have sizes := Naturals.injective.succ with sameLength208      have previous := ih with rest, restList, sizes209      have ordinary := IsCommRing.ring with source210      have head := IsRing.add_closed with ordinary, coefficient, he211      have added := hornerAdd.data at A, add, zero, neg, mul, one, tail, rest with *212      have fa := IsRingHom.closed with hom, left213      have fb := IsRingHom.closed with hom, right214      have fc := IsRingHom.closed with hom, coefficient215      have fe := IsRingHom.closed with hom, he216      have tailValue := hornerValue.closed at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, f(a), tail with *217      have restValue := hornerValue.closed at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, f(b), rest with *218      have mapped := IsRingHom.add with hom, coefficient, he219      have outer := hornerValue.cons at A, f, plus, times, f(R[a + b]), x, R[c + e], hornerAdd{A}(add, zero, tail, rest) with *220      have first := hornerValue.cons at A, f, plus, times, f(a), x, c, tail with *221      have second := hornerValue.cons at A, f, plus, times, f(b), x, e, rest with *222      rw [equal, hornerAdd, listHeadOr, listTail, outer, first, second, previous, mapped]223      ring224225theorem hornerScale.map_value (a b : Set) (cs : List(A))226  requires scalar : a ∈ R227  requires initial : b ∈ R228  shows monicValue{A}(f, plus, times, f(R[a * b]), x, hornerScale{A}(mul, a, cs)) =229    S[f(a) * monicValue{A}(f, plus, times, f(b), x, cs)]230proof231  induction cs232  | List.nil =>233    rw [hornerScale, monicValue, monicValue]234    exact IsRingHom.mul with hom, scalar, initial235  | List.cons(c, tail) using ih =>236    have coefficient : c ∈ R by assumption237    have ordinary := IsCommRing.ring with source238    have head := IsRing.mul_closed with ordinary, scalar, coefficient239    have rest := hornerScale.data with scalar240    have fa := IsRingHom.closed with hom, scalar241    have fb := IsRingHom.closed with hom, initial242    have fc := IsRingHom.closed with hom, coefficient243    have tailValue := hornerValue.closed at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, f(b), tail with *244    have mapped := IsRingHom.mul with hom, scalar, coefficient245    have outer := hornerValue.cons at A, f, plus, times, f(R[a * b]), x, R[a * c], hornerScale{A}(mul, a, tail) with *246    have original := hornerValue.cons at A, f, plus, times, f(b), x, c, tail with *247    rw [hornerScale, outer, original, ih, mapped]248    ring249250end Extensions251section Polynomials252variable (I A add zero neg mul one j : Set)253notation ring R := (A, add, zero, neg, mul, one)254notation ring P := R[I]255hypothesis ring : IsCommRing(R)256257theorem polynomialFromHorner.add (a b : Set) (cs ds : List(A))258  requires left : a ∈ R259  requires right : b ∈ R260  requires sameLength : length{A}(cs) = length{A}(ds)261  shows polynomialFromHorner(I, R, j, R[a + b], hornerAdd{A}(add, zero, cs, ds)) =262    P[polynomialFromHorner(I, R, j, a, cs) + polynomialFromHorner(I, R, j, b, ds)]263proof264  have target := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *265  have hom := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *266  have ordinary := IsCommRing.ring with ring267  have zeroIn := IsRing.zero_in_carrier with ordinary268  have oneIn : R[1] ∈ R by typecheck269  have sum := IsRing.add_closed with ordinary, left, right270  have variable := polynomialVariable.member at I, A, zero, one, j with *271  have first := polynomialCoefficients.value at I, A, zero, a with *272  have second := polynomialCoefficients.value at I, A, zero, b with *273  have combined := polynomialCoefficients.value at I, A, zero, R[a + b] with *274  have result := hornerAdd.map_value at A, add, zero, neg, mul, one, P, polynomialAdd(I, R), P[0], polynomialNeg(I, R), polynomialMul(I, R), P[1], polynomialCoefficients(I, R), polynomialVariable(I, R, j), a, b, cs, ds with *275  unfold polynomialFromHorner276  cc277278theorem polynomialFromHorner.affine_product (a b d carry : Set) (cs : List(A))279  requires initial : a ∈ R280  requires constant : b ∈ R281  requires slope : d ∈ R282  requires carried : carry ∈ R283  shows polynomialFromHorner(I, R, j, R[d * a], hornerAffineProduct{A}(add, mul, a, b, d, carry, cs)) =284    P[polynomialCoefficients(I, R)(carry) + (polynomialCoefficients(I, R)(b) + polynomialCoefficients(I, R)(d) * polynomialVariable(I, R, j)) * polynomialFromHorner(I, R, j, a, cs)]285proof286  have target := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *287  have hom := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *288  have ordinary := IsCommRing.ring with ring289  have zeroIn := IsRing.zero_in_carrier with ordinary290  have oneIn : R[1] ∈ R by typecheck291  have product := IsRing.mul_closed with ordinary, slope, initial292  have variable := polynomialVariable.member at I, A, zero, one, j with *293  have first := polynomialCoefficients.value at I, A, zero, a with *294  have combined := polynomialCoefficients.value at I, A, zero, R[d * a] with *295  have result := hornerAffineProduct.map_value at A, add, zero, neg, mul, one, P, polynomialAdd(I, R), P[0], polynomialNeg(I, R), polynomialMul(I, R), P[1], polynomialCoefficients(I, R), polynomialVariable(I, R, j), a, b, d, carry, cs with *296  unfold polynomialFromHorner297  cc298299theorem polynomialFromHorner.scale (a b : Set) (cs : List(A))300  requires scalar : a ∈ R301  requires initial : b ∈ R302  shows polynomialFromHorner(I, R, j, R[a * b], hornerScale{A}(mul, a, cs)) =303    P[polynomialCoefficients(I, R)(a) * polynomialFromHorner(I, R, j, b, cs)]304proof305  have target := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *306  have hom := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *307  have ordinary := IsCommRing.ring with ring308  have zeroIn := IsRing.zero_in_carrier with ordinary309  have oneIn : R[1] ∈ R by typecheck310  have product := IsRing.mul_closed with ordinary, scalar, initial311  have variable := polynomialVariable.member at I, A, zero, one, j with *312  have first := polynomialCoefficients.value at I, A, zero, b with *313  have combined := polynomialCoefficients.value at I, A, zero, R[a * b] with *314  have result := hornerScale.map_value at A, add, zero, neg, mul, one, P, polynomialAdd(I, R), P[0], polynomialNeg(I, R), polynomialMul(I, R), P[1], polynomialCoefficients(I, R), polynomialVariable(I, R, j), a, b, cs with *315  unfold polynomialFromHorner316  cc317318end Polynomials319