Grace/Cumulus/Algebra/Polynomial/HornerForms.g17

Open in Workbench Download source

Imports

HornerArithmetic

Declarations

Source

1-- Fixed-length polynomial representations and their tracked top 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.HornerForms8import HornerArithmetic910-- The terminal coefficient may be zero: n is a bound, not necessarily the degree.11predicate HornerForm (I A add zero neg mul one j p n a : Set) :=12  a ∈ A ∧ ∃ cs, List(A, cs) ∧ length{A}(cs) = n ∧ p = polynomialFromHorner(I, A, add, zero, neg, mul, one, j, a, cs)1314notation scoped HornerForm(I, R, j, p, n, a) => HornerForm(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, j, p, n, a)1516section Rings17variable (I A add zero neg mul one j : Set)18notation ring R := (A, add, zero, neg, mul, one)19notation ring P := R[I]20hypothesis ring : IsCommRing(R)2122theorem HornerForm.of_list (a : Set) (cs : List(A))23  requires initial : a ∈ R24  shows HornerForm(I, R, j, polynomialFromHorner(I, R, j, a, cs), length{A}(cs), a)25proof26  unfold HornerForm27  refine ⟨initial, cs, assumption, rfl, rfl⟩2829theorem HornerForm.member (p n a : Set)30  requires form : HornerForm(I, R, j, p, n, a)31  shows p ∈ P32proof33  obtain ⟨initial, cs, list, size, equal⟩ := form34  rw equal35  exact polynomialFromHorner.member with *3637theorem HornerForm.constant (a : Set)38  requires initial : a ∈ R39  shows HornerForm(I, R, j, polynomialCoefficients(I, R)(a), (0 : Nat), a)40proof41  have zeroIn : R[0] ∈ R by typecheck42  have empty : List(A, []) by typecheck43  have value := polynomialCoefficients.value at I, A, zero, a with *44  have horner := polynomialFromHorner.nil at I, A, add, zero, neg, mul, one, j, a45  unfold HornerForm46  refine ⟨initial, [], empty, ?_⟩47  constructor48  . exact length.nil with *49  . cc5051theorem HornerForm.add (p q n a b : Set)52  requires first : HornerForm(I, R, j, p, n, a)53  requires second : HornerForm(I, R, j, q, n, b)54  shows HornerForm(I, R, j, P[p + q], n, R[a + b])55proof56  obtain ⟨left, cs, csList, csSize, csEqual⟩ := first57  obtain ⟨right, ds, dsList, dsSize, dsEqual⟩ := second58  have ordinary := IsCommRing.ring with ring59  have initial := IsRing.add_closed with ordinary, left, right60  have sizes : length{A}(cs) = length{A}(ds) by cc61  have data := hornerAdd.data at A, add, zero, neg, mul, one, cs, ds with *62  have equation := polynomialFromHorner.add at I, A, add, zero, neg, mul, one, j, a, b, cs, ds with *63  unfold HornerForm64  refine ⟨initial, hornerAdd{A}(add, zero, cs, ds), data.left, ?_⟩65  constructor66  . cc67  . cc6869theorem HornerForm.affine_product (p n a b d : Set)70  requires form : HornerForm(I, R, j, p, n, a)71  requires constant : b ∈ R72  requires slope : d ∈ R73  shows HornerForm(I, R, j, P[(polynomialCoefficients(I, R)(b) + polynomialCoefficients(I, R)(d) * polynomialVariable(I, R, j)) * p], succ(n), R[d * a])74proof75  have member := HornerForm.member with *76  obtain ⟨initial, cs, list, size, equal⟩ := form77  have ordinary := IsCommRing.ring with ring78  have zeroIn := IsRing.zero_in_carrier with ordinary79  have oneIn : R[1] ∈ R by typecheck80  have leading := IsRing.mul_closed with ordinary, slope, initial81  have data := hornerAffineProduct.data at A, add, zero, neg, mul, one, a, b, d, zero, cs with *82  have equation := polynomialFromHorner.affine_product at I, A, add, zero, neg, mul, one, j, a, b, d, zero, cs with *83  have target := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *84  have targetRing := IsCommRing.ring with target85  have hom := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *86  have mapsZero := IsRingHom.zero with hom87  have constantIn := IsRingHom.closed with hom, constant88  have slopeIn := IsRingHom.closed with hom, slope89  have variableIn := polynomialVariable.member at I, A, zero, one, j with *90  have linear := IsRing.mul_closed with targetRing, slopeIn, variableIn91  have affine := IsRing.add_closed with targetRing, constantIn, linear92  have product := IsRing.mul_closed with targetRing, affine, member93  have identity := IsRing.add_left_identity with targetRing, product94  unfold HornerForm95  refine ⟨leading, hornerAffineProduct{A}(add, mul, a, b, d, zero, cs), data.left, ?_⟩96  constructor97  . cc98  . cc99100theorem HornerForm.scale (p n a b : Set)101  requires form : HornerForm(I, R, j, p, n, b)102  requires scalar : a ∈ R103  shows HornerForm(I, R, j, P[polynomialCoefficients(I, R)(a) * p], n, R[a * b])104proof105  obtain ⟨initial, cs, list, size, equal⟩ := form106  have ordinary := IsCommRing.ring with ring107  have leading := IsRing.mul_closed with ordinary, scalar, initial108  have data := hornerScale.data with scalar109  have equation := polynomialFromHorner.scale at I, A, add, zero, neg, mul, one, j, a, b, cs with *110  unfold HornerForm111  refine ⟨leading, hornerScale{A}(mul, a, cs), data.left, ?_⟩112  constructor113  . cc114  . cc115116theorem HornerForm.zero (n : Nat)117  shows HornerForm(I, R, j, P[0], n, R[0])118proof119  induction n120  | zero =>121    have zeroIn : R[0] ∈ R by typecheck122    have hom := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *123    have mapsZero := IsRingHom.zero with hom124    have form := HornerForm.constant at I, A, add, zero, neg, mul, one, j, zero with *125    rwa ← mapsZero126  | succ(k) using ih =>127    have zeroIn : R[0] ∈ R by typecheck128    have oneIn : R[1] ∈ R by typecheck129    have target := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *130    have targetRing := IsCommRing.ring with target131    have hom := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *132    have mapsZero := IsRingHom.zero with hom133    have mapsOne := IsRingHom.one with hom134    have variableIn := polynomialVariable.member at I, A, zero, one, j with *135    have equation : P[(polynomialCoefficients(I, R)(zero) + polynomialCoefficients(I, R)(one) * polynomialVariable(I, R, j)) * 0] = P[0]136      rw [mapsZero, mapsOne]137      ring138    have leading : R[one * zero] = R[0] by ring139    have form := HornerForm.affine_product at I, A, add, zero, neg, mul, one, j, P[0], k, zero, zero, one with *140    rwa [equation, leading] at form141142theorem HornerForm.leading_coefficient (p n a : Set)143  requires index : j ∈ I144  requires form : HornerForm(I, R, j, p, n, a)145  shows p(monomialShift(I, j, monomialOne(I), n)) = a146proof147  obtain ⟨initial, cs, list, size, equal⟩ := form148  have leading := polynomialFromHorner.leading_coefficient at I, A, add, zero, neg, mul, one, j, a, cs with *149  cc150151theorem HornerForm.indexed_sum (n k : Nat) (w c f : Set)152  shows (∀ i ∈ k, HornerForm(I, R, j, w(f(i)), n, c(f(i)))) →153    HornerForm(I, R, j, indexedRingSum(w, f, polynomialAdd(I, R), P[0], k), n, indexedRingSum(c, f, add, zero, k))154proof155  induction k156  | zero =>157    intro forms158    rw [indexedRingSum, indexedRingSum]159    exact HornerForm.zero with *160  | succ(r) using ih =>161    intro forms162    have prefix : ∀ i ∈ r, HornerForm(I, R, j, w(f(i)), n, c(f(i)))163      intros i hi164      have next := membership.into_successor at i, r with *165      exact forms with i, next166    have previous := ih with prefix167    have last := forms with r, membership.self_successor at r with *168    rw [indexedRingSum, indexedRingSum]169    exact HornerForm.add with *170171theorem HornerForm.finite_sum (n : Nat) (V w c : Set)172  requires finite : Finite(V)173  requires polynomials : w : V → P174  requires coefficients : c : V → R175  requires forms : ∀ i ∈ V, HornerForm(I, R, j, w(i), n, c(i))176  shows HornerForm(I, R, j, finiteRingSum(V, P, w), n, finiteRingSum(V, R, c))177proof178  have target := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *179  have chosen := finiteRingSum.selected at V, A, add, zero, neg, mul, one, c with *180  obtain ⟨k, natural, f, enumeration, coefficientSum⟩ := chosen.right181  have injective := Bijective.injective with enumeration182  have function := Injective.function with injective183  have polynomialSum : finiteRingSum(V, P, w) = indexedRingSum(w, f, polynomialAdd(I, R), P[0], k)184    exact finiteRingSum.enumeration with *185  have entries : ∀ i ∈ k, HornerForm(I, R, j, w(f(i)), n, c(f(i)))186    intros i hi187    have image := FunctionBetween.apply_closed with *188    exact forms with f(i), image189  have result : HornerForm(I, R, j, indexedRingSum(w, f, polynomialAdd(I, R), P[0], k), n, indexedRingSum(c, f, add, zero, k))190    have closure := HornerForm.indexed_sum at I, A, add, zero, neg, mul, one, j, n, k, w, c, f with *191    exact closure with entries192  rwa [polynomialSum, coefficientSum]193194theorem HornerForm.indexed_affine_product (k : Nat) (w b d f : Set)195  shows (∀ i ∈ k, b(f(i)) ∈ R ∧ d(f(i)) ∈ R ∧ w(f(i)) = P[polynomialCoefficients(I, R)(b(f(i))) + polynomialCoefficients(I, R)(d(f(i))) * polynomialVariable(I, R, j)]) →196    HornerForm(I, R, j, indexedRingProduct(w, f, polynomialMul(I, R), P[1], k), k, indexedRingProduct(d, f, mul, one, k))197proof198  induction k199  | zero =>200    intro entries201    have oneIn : R[1] ∈ R by typecheck202    have hom := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *203    have mapsOne := IsRingHom.one with hom204    have form := HornerForm.constant at I, A, add, zero, neg, mul, one, j, one with *205    rwa [indexedRingProduct, indexedRingProduct, ← mapsOne]206  | succ(r) using ih =>207    intro entries208    have prefix : ∀ i ∈ r, b(f(i)) ∈ R ∧ d(f(i)) ∈ R ∧ w(f(i)) = P[polynomialCoefficients(I, R)(b(f(i))) + polynomialCoefficients(I, R)(d(f(i))) * polynomialVariable(I, R, j)]209      intros i hi210      have next := membership.into_successor at i, r with *211      exact entries with i, next212    have previous := ih with prefix213    have last := entries with r, membership.self_successor at r with *214    obtain ⟨constant, slope, equation⟩ := last215    have polynomial := HornerForm.member at I, A, add, zero, neg, mul, one, j, indexedRingProduct(w, f, polynomialMul(I, R), P[1], r), r, indexedRingProduct(d, f, mul, one, r) with *216    have data := previous217    have topIn := data.left218    have result := HornerForm.affine_product at I, A, add, zero, neg, mul, one, j, indexedRingProduct(w, f, polynomialMul(I, R), P[1], r), r, indexedRingProduct(d, f, mul, one, r), b(f(r)), d(f(r)) with *219    have target := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *220    have hom := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *221    have constantIn := IsRingHom.closed with hom, constant222    have slopeIn := IsRingHom.closed with hom, slope223    have zeroIn : R[0] ∈ R by typecheck224    have oneIn : R[1] ∈ R by typecheck225    have variableIn := polynomialVariable.member at I, A, zero, one, j with *226    have commute : P[(polynomialCoefficients(I, R)(b(f(r))) + polynomialCoefficients(I, R)(d(f(r))) * polynomialVariable(I, R, j)) * indexedRingProduct(w, f, polynomialMul(I, R), P[1], r)] =227      P[indexedRingProduct(w, f, polynomialMul(I, R), P[1], r) * w(f(r))]228      rw equation229      ring230    have leadingCommutes : R[d(f(r)) * indexedRingProduct(d, f, mul, one, r)] = R[indexedRingProduct(d, f, mul, one, r) * d(f(r))]231      ring232    rw [commute, leadingCommutes] at result233    rwa [indexedRingProduct, indexedRingProduct]234235theorem HornerForm.finite_affine_product (V w b d : Set)236  requires finite : Finite(V)237  requires polynomials : w : V → P238  requires constants : b : V → R239  requires slopes : d : V → R240  requires entries : ∀ i ∈ V, w(i) = P[polynomialCoefficients(I, R)(b(i)) + polynomialCoefficients(I, R)(d(i)) * polynomialVariable(I, R, j)]241  shows HornerForm(I, R, j, finiteRingProduct(V, P, w), cardinality(V), finiteRingProduct(V, R, d))242proof243  have target := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *244  have chosen := finiteRingProduct.selected at V, A, add, zero, neg, mul, one, d with *245  obtain ⟨k, natural, f, enumeration, coefficientProduct⟩ := chosen.right246  have injective := Bijective.injective with enumeration247  have function := Injective.function with injective248  have reverse := converse.bijective at f, k, V with *249  have cardinal : HasCardinality(V, k)250    unfold HasCardinality251    refine ⟨natural, ?_⟩252    unfold Equipotent253    refine ⟨converse(f, k, V), reverse⟩254  have size := cardinality.eq_of_has at V, k with *255  have polynomialProduct : finiteRingProduct(V, P, w) = indexedRingProduct(w, f, polynomialMul(I, R), P[1], k)256    exact finiteRingProduct.enumeration with *257  have affine : ∀ i ∈ k, b(f(i)) ∈ R ∧ d(f(i)) ∈ R ∧ w(f(i)) = P[polynomialCoefficients(I, R)(b(f(i))) + polynomialCoefficients(I, R)(d(f(i))) * polynomialVariable(I, R, j)]258    intros i hi259    have image := FunctionBetween.apply_closed at f, k, V, i with *260    have constant := FunctionBetween.apply_closed at b, V, A, f(i) with *261    have slope := FunctionBetween.apply_closed at d, V, A, f(i) with *262    have equation := entries with f(i), image263    refine ⟨constant, slope, equation⟩264  have result : HornerForm(I, R, j, indexedRingProduct(w, f, polynomialMul(I, R), P[1], k), k, indexedRingProduct(d, f, mul, one, k))265    have closure := HornerForm.indexed_affine_product at I, A, add, zero, neg, mul, one, j, k, w, b, d, f with *266    exact closure with affine267  rwa [polynomialProduct, coefficientProduct, size]268269end Rings270