Grace/Cumulus/Algebra/Polynomial/HornerDegree.g17

Open in Workbench Download source

Imports

HornerPolynomial · HornerReconstruction

Declarations

Source

1-- Leading coefficients of Horner polynomials over commutative rings (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.HornerDegree8import HornerPolynomial9import HornerReconstruction1011section Constants12variable (I A add z neg mul one j : Set)13notation ring R := (A, add, z, neg, mul, one)14notation ring P := R[I]15hypothesis ring : IsCommRing(R)16hypothesis index : j ∈ I1718theorem polynomialConstant.shift_zero (a : Set) (n : Nat)19  requires coefficient : a ∈ R20  shows polynomialConstant(I, R, a)(monomialShift(I, j, monomialOne(I), succ(n))) = R[0]21proof22  have zeroIn : R[0] ∈ R by typecheck23  have unit := monomialOne.member at I24  have zeroNat := nat.omega.forward with Naturals.constructor.zero25  have absent : monomialOne(I)(j) = (0 : Nat)26    unfold monomialOne27    exact constantFunction.apply with *28  have shifted := monomialShift.member at I, j, monomialOne(I), succ(n) with *29  have exponent := monomialShift.exponent at I, j, monomialOne(I), succ(n) with *30  have distinct : monomialShift(I, j, monomialOne(I), succ(n)) ≠ monomialOne(I)31    intro equal32    have impossible : (0 : Nat) = succ(n) by cc33    exact Naturals.disjoint.zero.succ at n with impossible34  have value := polynomialConstant.value at I, A, z, a, monomialShift(I, j, monomialOne(I), succ(n)) with *35  have selected := singleValue.other at A, z, a, monomialOne(I), monomialShift(I, j, monomialOne(I), succ(n)) with *36  cc3738end Constants3940section Rings41variable (I A add z neg mul one j leading : Set)42notation ring R := (A, add, z, neg, mul, one)43notation ring P := R[I]44hypothesis ring : IsCommRing(R)45hypothesis index : j ∈ I46hypothesis initial : leading ∈ R4748theorem polynomialFromHorner.coefficient_succ (c : Set) (cs : List(A)) (n : Nat)49  requires coefficient : c ∈ R50  shows polynomialFromHorner(I, R, j, leading, c :: cs)(monomialShift(I, j, monomialOne(I), succ(n))) =51    polynomialFromHorner(I, R, j, leading, cs)(monomialShift(I, j, monomialOne(I), n))52proof53  have ordinary := IsCommRing.ring with ring54  have zeroIn := IsRing.zero_in_carrier with ordinary55  have oneIn : R[1] ∈ R by typecheck56  have unit := monomialOne.member at I57  have variable := monomialVariable.member at I, j58  have previous := monomialShift.member at I, j, monomialOne(I), n with *59  have shifted := monomialShift.member at I, j, monomialOne(I), succ(n) with *60  have constant := polynomialConstant.member at I, A, z, c with *61  have tail := polynomialFromHorner.member at I, A, add, z, neg, mul, one, j, leading, cs with *62  have variablePoly := polynomialVariable.member at I, A, z, one, j with *63  have product := polynomialProduct.member at I, A, add, z, neg, mul, one, polynomialVariable(I, R, j), polynomialFromHorner(I, R, j, leading, cs) with *64  have productOperation := polynomialMul.apply at I, A, add, z, neg, mul, one, polynomialVariable(I, R, j), polynomialFromHorner(I, R, j, leading, cs) with *65  have sumOperation := polynomialAdd.apply at I, A, add, z, neg, mul, one, polynomialConstant(I, R, c), polynomialProduct(I, A, add, z, neg, mul, one, polynomialVariable(I, R, j), polynomialFromHorner(I, R, j, leading, cs)) with *66  have constantFunction := polynomials.function with constant67  have productFunction := polynomials.function with product68  have sumValue := coefficientAdd.value at monomials(I), A, add, z, neg, mul, one, polynomialConstant(I, R, c), polynomialProduct(I, A, add, z, neg, mul, one, polynomialVariable(I, R, j), polynomialFromHorner(I, R, j, leading, cs)), monomialShift(I, j, monomialOne(I), succ(n)) with *69  have constantZero := polynomialConstant.shift_zero at I, A, add, z, neg, mul, one, j, c, n with *70  have step := monomialShift.succ at I, j, monomialOne(I), n with *71  have shiftedValue := polynomialProduct.monomial_shift at I, A, add, z, neg, mul, one, monomialVariable(I, j), monomialShift(I, j, monomialOne(I), n), polynomialFromHorner(I, R, j, leading, cs) with *72  have valueIn := polynomials.coefficient at I, A, z, polynomialFromHorner(I, R, j, leading, cs), monomialShift(I, j, monomialOne(I), n) with *73  have identity := IsRing.add_left_identity with ordinary, valueIn74  have equation := polynomialFromHorner.cons at I, A, add, z, neg, mul, one, j, leading, c, cs with *75  have shiftedProduct : polynomialProduct(I, A, add, z, neg, mul, one, polynomialVariable(I, R, j), polynomialFromHorner(I, R, j, leading, cs))(monomialProduct(I, monomialVariable(I, j), monomialShift(I, j, monomialOne(I), n))) = polynomialFromHorner(I, R, j, leading, cs)(monomialShift(I, j, monomialOne(I), n))76    simp [polynomialVariable]77  rw [productOperation, sumOperation] at equation78  cc7980theorem polynomialFromHorner.leading_coefficient (cs : List(A))81  shows polynomialFromHorner(I, R, j, leading, cs)(monomialShift(I, j, monomialOne(I), length{A}(cs))) = leading82proof83  induction cs84  | List.nil =>85    have zeroIn : R[0] ∈ R by typecheck86    have unit := monomialOne.member at I87    have value := polynomialConstant.value at I, A, z, leading, monomialOne(I) with *88    have reflexive : monomialOne(I) = monomialOne(I) by rfl89    have selected := singleValue.same at A, z, leading, monomialOne(I), monomialOne(I) with *90    rw [length.nil, monomialShift.zero, polynomialFromHorner.nil]91    cc92  | List.cons(c, tail) using ih =>93    have coefficient : c ∈ R by assumption94    have shifted := polynomialFromHorner.coefficient_succ at I, A, add, z, neg, mul, one, j, leading, c, tail, length{A}(tail) with *95    rw length.cons96    cc9798-- Along the chosen variable, every coefficient beyond the declared length vanishes.99theorem polynomialFromHorner.coefficient_above_length (cs : List(A)) (n : Nat)100  requires bound : length{A}(cs) < n101  shows polynomialFromHorner(I, R, j, leading, cs)(monomialShift(I, j, monomialOne(I), n)) = R[0]102proof103  induction cs generalizing n104  | List.nil =>105    intros n nNat bound106    rw length.nil at bound107    have shape := natural.zero_or_successor with *108    cases shape with zero | successor109    . have impossible : (0 : Nat) < (0 : Nat)110        arith111      exfalso112      have irreflexive := Less.irreflexive with Naturals.constructor.zero113      exact irreflexive with impossible114    . obtain ⟨k, kNat, equal⟩ := successor115      rw [equal, polynomialFromHorner.nil]116      exact polynomialConstant.shift_zero with *117  | List.cons(c, tail) using ih =>118    intros n nNat bound119    have coefficient : c ∈ R by assumption120    rw length.cons at bound121    have shape := natural.zero_or_successor with *122    cases shape with zero | successor123    . have impossible : (0 : Nat) < (0 : Nat)124        arith125      exfalso126      have irreflexive := Less.irreflexive with Naturals.constructor.zero127      exact irreflexive with impossible128    . obtain ⟨k, kNat, equal⟩ := successor129      have smaller : length{A}(tail) < k by arith130      have previous := ih with k, kNat, smaller131      have shifted := polynomialFromHorner.coefficient_succ at I, A, add, z, neg, mul, one, j, leading, c, tail, k with *132      rw equal133      cc134135theorem polynomialFromHorner.leading_unique (other : Set) (cs ds : List(A))136  requires otherIn : other ∈ R137  requires sameLength : length{A}(cs) = length{A}(ds)138  requires equal : polynomialFromHorner(I, R, j, leading, cs) = polynomialFromHorner(I, R, j, other, ds)139  shows leading = other140proof141  have first := polynomialFromHorner.leading_coefficient at I, A, add, z, neg, mul, one, j, leading, cs with *142  have second := polynomialFromHorner.leading_coefficient at I, A, add, z, neg, mul, one, j, other, ds with *143  cc144145theorem polynomialFromHorner.length_unique (other : Set) (cs ds : List(A))146  requires otherIn : other ∈ R147  requires leadingNonzero : leading ≠ R[0]148  requires otherNonzero : other ≠ R[0]149  requires equal : polynomialFromHorner(I, R, j, leading, cs) = polynomialFromHorner(I, R, j, other, ds)150  shows length{A}(cs) = length{A}(ds)151proof152  have comparison := Less.trichotomy at length{A}(cs), length{A}(ds) with *153  have alternatives : length{A}(cs) < length{A}(ds) ∨ length{A}(cs) = length{A}(ds) ∨ length{A}(ds) < length{A}(cs)154    tauto155  cases alternatives with smaller | rest156  . have above := polynomialFromHorner.coefficient_above_length at I, A, add, z, neg, mul, one, j, leading, cs, length{A}(ds) with *157    have top := polynomialFromHorner.leading_coefficient at I, A, add, z, neg, mul, one, j, other, ds with *158    exfalso159    apply otherNonzero160    cc161  . cases rest with same | larger162    . exact same163    . have above := polynomialFromHorner.coefficient_above_length at I, A, add, z, neg, mul, one, j, other, ds, length{A}(cs) with *164      have top := polynomialFromHorner.leading_coefficient at I, A, add, z, neg, mul, one, j, leading, cs with *165      exfalso166      apply leadingNonzero167      cc168169theorem polynomialFromHorner.nonzero_of_leading (cs : List(A))170  requires nonzero : leading ≠ R[0]171  shows polynomialFromHorner(I, R, j, leading, cs) ≠ P[0]172proof173  have zeroIn : R[0] ∈ R by typecheck174  have unit := monomialOne.member at I175  have shifted := monomialShift.member at I, j, monomialOne(I), length{A}(cs) with *176  have coefficient := polynomialFromHorner.leading_coefficient at I, A, add, z, neg, mul, one, j, leading, cs with *177  have zeroValue := constantFunction.apply at monomials(I), A, monomialShift(I, j, monomialOne(I), length{A}(cs)), z with *178  intro equal179  apply nonzero180  cc181182end Rings183