Grace/Cumulus/Algebra/Polynomial/HornerReconstruction.g17

Open in Workbench Download source

Imports

CoefficientHorner · MonomialShift

Declarations

Source

1-- Reconstructing sparse polynomials from coefficients in a chosen variable (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.HornerReconstruction8import CoefficientHorner9import MonomialShift1011def monomialShift (I j m : Set, n : Nat) : Set := monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m)1213theorem monomialShift.member (I j m : Set, n : Nat)14  requires monomial : m ∈ monomials(I)15  shows monomialShift(I, j, m, n) ∈ monomials(I)16proof17  have single := monomialSingle.member at I, j, n with *18  unfold monomialShift19  exact monomialProduct.member with *2021theorem monomialShift.zero (I j m : Set)22  requires monomial : m ∈ monomials(I)23  shows monomialShift(I, j, m, 0) = m24proof25  have unit := monomialOne.member at I26  have commute := monomialProduct.commutative at I, monomialOne(I), m with *27  have identity := monomialProduct.one at I, m with *28  unfold monomialShift29  rw monomialSingle.zero30  cc3132theorem monomialShift.succ (I j m : Set, n : Nat)33  requires monomial : m ∈ monomials(I)34  requires index : j ∈ I35  shows monomialShift(I, j, m, succ(n)) = monomialProduct(I, monomialVariable(I, j), monomialShift(I, j, m, n))36proof37  have single := monomialSingle.member at I, j, n with *38  have variable := monomialVariable.member at I, j39  have step := monomialSingle.succ at I, j, n with *40  have successor := add.right_one with *41  rw successor at step42  have associative := monomialProduct.associative at I, monomialVariable(I, j), coefficientSingle(I, ℕ, 0, n, j), m with *43  unfold monomialShift44  cc4546theorem monomialShift.exponent (I j m : Set, n : Nat)47  requires monomial : m ∈ monomials(I)48  requires index : j ∈ I49  requires absent : m(j) = 050  shows monomialShift(I, j, m, n)(j) = n51proof52  have zeroIn := nat.omega.forward with Naturals.constructor.zero53  have nIn := nat.omega.forward at n with *54  have single := monomialSingle.member at I, j, n with *55  have value := monomialProduct.value at I, coefficientSingle(I, ℕ, 0, n, j), m, j with *56  have head := coefficientSingle.same at I, ℕ, 0, n, j with *57  have identity := add.right_unit with *58  unfold monomialShift59  cc6061predicate coefficientsOmitVariable (I A z j cs : Set) :=62  ∀ n ∈ ℕ, ∀ m ∈ monomials(I), m(j) ≠ 0 → listCoefficient{polynomials(I, A, z)}(constantFunction(monomials(I), A, z), cs, n)(m) = z6364section Coefficients65variable (I A add z neg mul one j m : Set)66hypothesis ring : IsCommRing(A, add, z, neg, mul, one)67hypothesis index : j ∈ I68hypothesis monomial : m ∈ monomials(I)69hypothesis absent : m(j) = 07071theorem polynomialFromCoefficients.coefficient (cs : List(polynomials(I, A, z))) (n : Nat)72  requires omitted : coefficientsOmitVariable(I, A, z, j, cs)73  shows polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, cs)(monomialShift(I, j, m, n)) = listCoefficient{polynomials(I, A, z)}(constantFunction(monomials(I), A, z), cs, n)(m)74proof75  induction cs generalizing n76  | List.nil =>77    intros n nNat omitted78    have ordinary := IsCommRing.ring with ring79    have zeroIn := IsRing.zero_in_carrier with ordinary80    have shifted := monomialShift.member at I, j, m, n with *81    have left := constantFunction.apply at monomials(I), A, monomialShift(I, j, m, n), z with *82    have right := constantFunction.apply at monomials(I), A, m, z with *83    rw [polynomialFromCoefficients.nil, listCoefficient.nil]84    cc85  | List.cons(c, tail) using ih =>86    intros n nNat omitted87    have coefficient : c ∈ polynomials(I, A, z) by assumption88    have ordinary := IsCommRing.ring with ring89    have zeroIn := IsRing.zero_in_carrier with ordinary90    have multiplicative := IsRing.multiplicative with ordinary91    have oneIn := IsMonoid.unit_in_carrier with multiplicative92    have tailPolynomial := polynomialFromCoefficients.member at I, A, add, z, neg, mul, one, j, tail with *93    have variable := polynomialVariable.member at I, A, z, one, j with *94    have product := polynomialProduct.member at I, A, add, z, neg, mul, one, polynomialVariable(I, A, z, one, j), polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, tail) with *95    have productOperation := polynomialMul.apply at I, A, add, z, neg, mul, one, polynomialVariable(I, A, z, one, j), polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, tail) with *96    have sumOperation := polynomialAdd.apply at I, A, add, z, neg, mul, one, c, polynomialProduct(I, A, add, z, neg, mul, one, polynomialVariable(I, A, z, one, j), polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, tail)) with *97    have coefficientFunction := polynomials.function with coefficient98    have productFunction := polynomials.function with product99    have shifted := monomialShift.member at I, j, m, n with *100    have sumValue := coefficientAdd.value at monomials(I), A, add, z, neg, mul, one, c, polynomialProduct(I, A, add, z, neg, mul, one, polynomialVariable(I, A, z, one, j), polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, tail)), monomialShift(I, j, m, n) with *101    have equation := polynomialFromCoefficients.cons at I, A, add, z, neg, mul, one, j, c, tail with *102    rw [productOperation, sumOperation] at equation103    rw [equation, sumValue]104    have shape := natural.zero_or_successor with *105    cases shape with zero | successor106    . rw [zero, monomialShift.zero, listCoefficient.zero]107      have vanishes := polynomialProduct.variable_zero at I, A, add, z, neg, mul, one, j, m, polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, tail) with *108      have value := polynomials.coefficient at I, A, z, c, m with *109      rw vanishes110      exact IsRing.add_right_identity with ordinary, value111    . obtain ⟨k, kNat, equal⟩ := successor112      have nextShift := monomialShift.member at I, j, m, succ(k) with *113      have degree := monomialShift.exponent at I, j, m, succ(k) with *114      have positive : monomialShift(I, j, m, succ(k))(j) ≠ 0115        intro vanishes116        have impossible : 0 = succ(k) by cc117        exact Naturals.disjoint.zero.succ at k with impossible118      have zeroNatIn := nat.omega.forward with Naturals.constructor.zero119      have headZero := omitted with 0, zeroNatIn, monomialShift(I, j, m, succ(k)), nextShift, positive120      rw listCoefficient.zero at headZero121      have tailOmitted : coefficientsOmitVariable(I, A, z, j, tail)122        intros r rIn t ht present123        have rNat := nat.omega.backward with rIn124        have successorIn := nat.omega.forward at succ(r) with *125        have value := omitted with succ(r), successorIn, t, ht, present126        rwa listCoefficient.succ at value127      have rest := ih with k, kNat, tailOmitted128      have previous := monomialShift.member at I, j, m, k with *129      have variableMonomial := monomialVariable.member at I, j130      have shift := polynomialProduct.monomial_shift at I, A, add, z, neg, mul, one, monomialVariable(I, j), monomialShift(I, j, m, k), polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, tail) with *131      have step := monomialShift.succ at I, j, m, k with *132      have value := polynomials.coefficient at I, A, z, polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, tail), monomialShift(I, j, m, k) with *133      have identity := IsRing.add_left_identity with ordinary, value134      have shiftAt : polynomialProduct(I, A, add, z, neg, mul, one, polynomialVariable(I, A, z, one, j), polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, tail))(monomialShift(I, j, m, succ(k))) = polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, tail)(monomialShift(I, j, m, k))135        rw step136        unfold polynomialVariable137        cc138      rwa [equal, listCoefficient.succ, headZero, shiftAt, identity]139140end Coefficients141theorem polynomialVariableCoefficient.list_omits (I A z p j : Set) (cs : List(polynomials(I, A, z)))142  requires zeroIn : z ∈ A143  requires polynomial : p ∈ polynomials(I, A, z)144  requires coefficients : ∀ n, Nat(n) → listCoefficient{polynomials(I, A, z)}(constantFunction(monomials(I), A, z), cs, n) = polynomialVariableCoefficient(I, A, z, p, j, n)145  shows coefficientsOmitVariable(I, A, z, j, cs)146proof147  intros n nIn m hm present148  have natural := nat.omega.backward with nIn149  have value := coefficients with n, natural150  have vanishes := polynomialVariableCoefficient.at_nonzero with *151  cc152153section Reconstruction154variable (I A add z neg mul one p j : Set)155notation ring R := (A, add, z, neg, mul, one)156notation ring P := R[I]157hypothesis ring : IsCommRing(R)158hypothesis polynomial : p ∈ P159hypothesis index : j ∈ I160161theorem polynomialFromCoefficients.reconstruct (cs : List(P))162  requires coefficients : ∀ n, Nat(n) → listCoefficient{P}(P[0], cs, n) = polynomialVariableCoefficient(I, R, p, j, n)163  shows polynomialFromCoefficients(I, R, j, cs) = p164proof165  have zeroIn : R[0] ∈ R by typecheck166  have member := polynomialFromCoefficients.member at I, A, add, z, neg, mul, one, j, cs with *167  have omitted := polynomialVariableCoefficient.list_omits at I, A, z, p, j, cs with *168  apply polynomials.ext with member, polynomial169  intros m hm170  have exponent := monomials.exponent at I, m, j with *171  have erased := monomialErase.member at I, m, j with *172  have function := monomials.function with hm173  have naturalZero := nat.omega.forward with Naturals.constructor.zero174  have absent := coefficientErase.same at I, ℕ, (0:Nat), m, j with *175  have value := polynomialFromCoefficients.coefficient at I, A, add, z, neg, mul, one, j, coefficientErase(I, ℕ, (0:Nat), m, j), cs, m(j) with *176  have restore := monomialErase.restore at I, m, j with *177  have shape : monomialShift(I, j, coefficientErase(I, ℕ, (0:Nat), m, j), m(j)) = m178    unfold monomialShift179    cc180  have listValue := coefficients with m(j), exponent181  have recovery := polynomialVariableCoefficient.recover at I, A, z, p, j, m with *182  cc183184theorem polynomials.exists_coefficient_horner185  shows ∃ cs, List(P, cs) ∧ coefficientsOmitVariable(I, A, z, j, cs) ∧ polynomialFromCoefficients(I, R, j, cs) = p186proof187  have zeroIn : R[0] ∈ R by typecheck188  obtain ⟨cs, list, coefficients⟩ := polynomialCoefficientFamily.list_representation at I, A, z, p, j with *189  have omitted := polynomialVariableCoefficient.list_omits with *190  have reconstruct := polynomialFromCoefficients.reconstruct with *191  refine ⟨cs, list, omitted, reconstruct⟩192193theorem polynomials.exists_nonzero_coefficient_horner194  requires nonzero : p ≠ P[0]195  shows ∃ cs, List(P, cs) ∧ coefficientsOmitVariable(I, A, z, j, cs) ∧ polynomialFromCoefficients(I, R, j, cs) = p ∧ (∃ n ∈ ℕ, listCoefficient{P}(P[0], cs, n) ≠ P[0])196proof197  have zeroIn : R[0] ∈ R by typecheck198  obtain ⟨cs, list, coefficients⟩ := polynomialCoefficientFamily.list_representation at I, A, z, p, j with *199  have omitted := polynomialVariableCoefficient.list_omits with *200  have reconstruct := polynomialFromCoefficients.reconstruct with *201  obtain ⟨n, nIn, coefficient⟩ := polynomialVariableCoefficient.exists_nonzero at I, A, z, p, j with *202  have natural := nat.omega.backward with nIn203  have value := coefficients with n, natural204  refine ⟨cs, list, omitted, reconstruct, n, nIn, ?_⟩205  rwa value206207theorem polynomialAt.reconstruction (v : Set) (cs : List(P))208  requires assignment : v : I → R209  requires coefficients : ∀ n, Nat(n) → listCoefficient{P}(P[0], cs, n) = polynomialVariableCoefficient(I, R, p, j, n)210  shows polynomialAt(I, R, v)(p) = hornerAt{A}(add, mul, z, v(j), listMap{P}(polynomialAt(I, R, v), cs))211proof212  have reconstruct := polynomialFromCoefficients.reconstruct with *213  have evaluation := polynomialAt.coefficient_horner with *214  cc215216end Reconstruction217