-- Linear evaluation of finite-support polynomials from monomial values (ZF).
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Polynomial.Evaluation
import Origin

defgraph polynomialEvaluationWeights (I D A add zero neg mul one h p : Set) (m ∈ D) : A := call2(mul, p(m), h(m))
requires ring : IsCommRing(A, add, zero, neg, mul, one)
requires values : h : monomials(I) → A
requires polynomial : p ∈ polynomials(I, A, zero)
requires domain : D ⊆ monomials(I)
proof
  unfold Subset at domain
  have monomial := domain with m, member
  have coefficient := polynomials.coefficient at I, A, zero, p, m with *
  have image := FunctionBetween.apply_closed at h, monomials(I), A, m with *
  have ordinary := IsCommRing.ring with ring
  exact IsRing.mul_closed at A, add, zero, neg, mul, one, p(m), h(m) with *

defgraph polynomialEvaluate (I A add zero neg mul one h : Set) (p ∈ polynomials(I, A, zero)) : A :=
  finiteRingSum(functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, polynomialEvaluationWeights(I, functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, h, p))
requires ring : IsCommRing(A, add, zero, neg, mul, one)
requires values : h : monomials(I) → A
proof
  have domain := functionSupport.subset at p, monomials(I), zero
  have finite := polynomials.finite_support with member
  have weights := polynomialEvaluationWeights.function at I, functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, h, p with *
  exact finiteRingSum.closed at functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, polynomialEvaluationWeights(I, functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, h, p) with *

section Values
variable (I A add zero neg mul one h : Set)
hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)
hypothesis values : h : monomials(I) → A
notation ring R := (A, add, zero, neg, mul, one)

theorem polynomialEvaluate.on_domain (p D : Set)
  requires polynomial : p ∈ polynomials(I, A, zero)
  requires domain : D ⊆ monomials(I)
  requires finite : Finite(D)
  requires covers : functionSupport(p, monomials(I), zero) ⊆ D
  shows polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) = finiteRingSum(D, A, add, zero, neg, mul, one, polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, p))
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have supportDomain := functionSupport.subset at p, monomials(I), zero
  have weights := polynomialEvaluationWeights.function at I, D, A, add, zero, neg, mul, one, h, p with *
  have supported := polynomialEvaluationWeights.function at I, functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, h, p with *
  have agreement : ∀ m ∈ functionSupport(p, monomials(I), zero), polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, p)(m) = polynomialEvaluationWeights(I, functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, h, p)(m)
    intros m hm
    have included := covers
    have inD := included with m, hm
    have left := polynomialEvaluationWeights.value at I, D, A, add, zero, neg, mul, one, h, p, m with *
    have right := polynomialEvaluationWeights.value at I, functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, h, p, m with *
    cc
  have vanishes : ∀ m ∈ D, ¬(m ∈ functionSupport(p, monomials(I), zero)) → polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, p)(m) = zero
    intros m hm outside
    have included := domain
    have monomial := included with m, hm
    have image := FunctionBetween.apply_closed at h, monomials(I), A, m with *
    have coefficient := functionSupport.outside at p, monomials(I), zero, m with *
    have weight := polynomialEvaluationWeights.value at I, D, A, add, zero, neg, mul, one, h, p, m with *
    rw [weight, coefficient]
    ring
  have extended := finiteRingSum.zero_extension at D, functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, p), polynomialEvaluationWeights(I, functionSupport(p, monomials(I), zero), A, add, zero, neg, mul, one, h, p) with *
  have value := polynomialEvaluate.value at I, A, add, zero, neg, mul, one, h, p with *
  cc

theorem polynomialEvaluate.term (a m : Set)
  requires coefficient : a ∈ A
  requires monomial : m ∈ monomials(I)
  shows polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(polynomialTerm(I, A, zero, a, m)) = a * h(m)
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have polynomial := polynomialTerm.member at I, A, zero, a, m with *
  have covers := polynomialTerm.support at I, A, zero, a, m with *
  have domain : {m} ⊆ monomials(I) by simp [Subset, singleton.membership]
  have finite := Finite.singleton at m
  have member := singleton.self at m
  have bounded := polynomialEvaluate.on_domain with *
  have weights := polynomialEvaluationWeights.function at I, {m}, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m) with *
  have sum := finiteRingSum.singleton with *
  have weight := polynomialEvaluationWeights.value at I, {m}, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m), m with *
  have point := polynomialTerm.same at I, A, zero, a, m with *
  cc

theorem polynomialEvaluate.zero
  shows polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(constantFunction(monomials(I), A, zero)) = zero
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have unit := monomialOne.member at I
  have image := FunctionBetween.apply_closed with *
  have selected := polynomialEvaluate.term at I, A, add, zero, neg, mul, one, h, zero, monomialOne(I) with *
  have constant := polynomialConstant.zero at I, A, zero with *
  unfold polynomialConstant at constant
  have zeroProduct : zero * h(monomialOne(I)) = zero by ring
  cc

theorem polynomialEvaluationWeights.add (p q D : Set)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  requires domain : D ⊆ monomials(I)
  shows polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q)) = coefficientAdd(D, A, add, zero, neg, mul, one, polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, p), polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, q))
proof
  have memberSum := polynomials.add at I, A, add, zero, neg, mul, one, p, q with *
  have functionP := polynomials.function with memberP
  have functionQ := polynomials.function with memberQ
  have weightsP := polynomialEvaluationWeights.function at I, D, A, add, zero, neg, mul, one, h, p with *
  have weightsQ := polynomialEvaluationWeights.function at I, D, A, add, zero, neg, mul, one, h, q with *
  have leftFunction := polynomialEvaluationWeights.function at I, D, A, add, zero, neg, mul, one, h, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q) with *
  have rightFunction := coefficientAdd.function at D, A, add, zero, neg, mul, one, polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, p), polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, q) with *
  apply FunctionBetween.ext with leftFunction, rightFunction
  intros m hm
  have included := domain
  have monomial := included with m, hm
  have coefficientP := polynomials.coefficient at I, A, zero, p, m with *
  have coefficientQ := polynomials.coefficient at I, A, zero, q, m with *
  have image := FunctionBetween.apply_closed at h, monomials(I), A, m with *
  have source := coefficientAdd.value at monomials(I), A, add, zero, neg, mul, one, p, q, m with *
  have left := polynomialEvaluationWeights.value at I, D, A, add, zero, neg, mul, one, h, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q), m with *
  have first := polynomialEvaluationWeights.value at I, D, A, add, zero, neg, mul, one, h, p, m with *
  have second := polynomialEvaluationWeights.value at I, D, A, add, zero, neg, mul, one, h, q, m with *
  have right := coefficientAdd.value at D, A, add, zero, neg, mul, one, polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, p), polynomialEvaluationWeights(I, D, A, add, zero, neg, mul, one, h, q), m with *
  have distribute : (p(m) + q(m)) * h(m) = p(m) * h(m) + q(m) * h(m) by ring
  cc

theorem polynomialEvaluate.add (p q : Set)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  shows polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q)) = polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) + polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(q)
proof
  have memberSum := polynomials.add at I, A, add, zero, neg, mul, one, p, q with *
  have functionP := polynomials.function with memberP
  have functionQ := polynomials.function with memberQ
  have finiteP := polynomials.finite_support with memberP
  have finiteQ := polynomials.finite_support with memberQ
  have finite := Finite.union with finiteP, finiteQ
  have domainP := functionSupport.subset at p, monomials(I), zero
  have domainQ := functionSupport.subset at q, monomials(I), zero
  have domain : functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero) ⊆ monomials(I)
    simp [Subset, union2.membership]
  have coversP : functionSupport(p, monomials(I), zero) ⊆ functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero)
    simp [Subset, union2.membership]
  have coversQ : functionSupport(q, monomials(I), zero) ⊆ functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero)
    simp [Subset, union2.membership]
  have coversSum := coefficientAdd.support at monomials(I), A, add, zero, neg, mul, one, p, q with *
  have sumValue := polynomialEvaluate.on_domain with ring, values, memberSum, domain, finite, coversSum
  have firstValue := polynomialEvaluate.on_domain with ring, values, memberP, domain, finite, coversP
  have secondValue := polynomialEvaluate.on_domain with ring, values, memberQ, domain, finite, coversQ
  have weightsP := polynomialEvaluationWeights.function at I, functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero), A, add, zero, neg, mul, one, h, p with *
  have weightsQ := polynomialEvaluationWeights.function at I, functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero), A, add, zero, neg, mul, one, h, q with *
  have weightsSum := polynomialEvaluationWeights.add at I, A, add, zero, neg, mul, one, h, p, q, functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero) with *
  have distribute := finiteRingSum.add at functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero), A, add, zero, neg, mul, one, polynomialEvaluationWeights(I, functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero), A, add, zero, neg, mul, one, h, p), polynomialEvaluationWeights(I, functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero), A, add, zero, neg, mul, one, h, q) with *
  cc

theorem polynomialEvaluate.in_carrier (p : Set)
  requires polynomial : p ∈ polynomials(I, A, zero)
  shows polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) ∈ A
proof
  have function := polynomialEvaluate.function at I, A, add, zero, neg, mul, one, h with *
  exact FunctionBetween.apply_closed with function, polynomial

theorem polynomialEvaluate.neg (p : Set)
  requires polynomial : p ∈ polynomials(I, A, zero)
  shows polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p)) = -polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p)
proof
  have negative := polynomials.neg with *
  have valueP := polynomialEvaluate.in_carrier at I, A, add, zero, neg, mul, one, h, p with *
  have valueNeg := polynomialEvaluate.in_carrier at I, A, add, zero, neg, mul, one, h, coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p) with *
  have functionP := polynomials.function with polynomial
  have inverse := coefficientAdd.inverse at monomials(I), A, add, zero, neg, mul, one, p with *
  have sum := polynomialEvaluate.add at I, A, add, zero, neg, mul, one, h, p, coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p) with *
  have zeroValue := polynomialEvaluate.zero at I, A, add, zero, neg, mul, one, h with *
  have equation : polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) + polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p)) = zero
    cc
  linear_combination equation

end Values