-- Distributivity of finite polynomial convolution via common support bounds (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.Distributivity
import ConvolutionBounds

theorem boundedConvolutionWeights.add (I D A add zero neg mul one p q r : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  requires memberR : r ∈ polynomials(I, A, zero)
  requires domain : D ⊆ monomials(I) × monomials(I)
  shows boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r)) =
    coefficientAdd(D, A, add, zero, neg, mul, one, boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, q), boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, r))
proof
  have memberSum := polynomials.add at I, A, add, zero, neg, mul, one, q, r with *
  have functionQ := polynomials.function with memberQ
  have functionR := polynomials.function with memberR
  have leftFunction := boundedConvolutionWeights.function at I, D, A, add, zero, neg, mul, one, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r) with *
  have weightsQ := boundedConvolutionWeights.function at I, D, A, add, zero, neg, mul, one, p, q with *
  have weightsR := boundedConvolutionWeights.function at I, D, A, add, zero, neg, mul, one, p, r with *
  have rightFunction := coefficientAdd.function at D, A, add, zero, neg, mul, one, boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, q), boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, r) with *
  apply FunctionBetween.ext with leftFunction, rightFunction
  intros t ht
  have included := domain
  have pair := included with t, ht
  obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with pair
  have inD : (u, v) ∈ D by rwa ← shape
  have pValue := polynomials.coefficient at I, A, zero, p, u with *
  have qValue := polynomials.coefficient at I, A, zero, q, v with *
  have rValue := polynomials.coefficient at I, A, zero, r, v with *
  have sumValue := coefficientAdd.value at monomials(I), A, add, zero, neg, mul, one, q, r, v with *
  have left := boundedConvolutionWeights.pair at I, D, A, add, zero, neg, mul, one, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r), u, v with *
  have first := boundedConvolutionWeights.pair at I, D, A, add, zero, neg, mul, one, p, q, u, v with *
  have second := boundedConvolutionWeights.pair at I, D, A, add, zero, neg, mul, one, p, r, u, v with *
  have right := coefficientAdd.value at D, A, add, zero, neg, mul, one, boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, q), boundedConvolutionWeights(I, D, A, add, zero, neg, mul, one, p, r), (u, v) with *
  have distribute : call2(mul, p(u), call2(add, q(v), r(v))) = call2(add, call2(mul, p(u), q(v)), call2(mul, p(u), r(v)))
    ring
  cc

theorem convolutionPairs.add_subset (I A add zero neg mul one p q r : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires memberQ : q ∈ polynomials(I, A, zero)
  requires memberR : r ∈ polynomials(I, A, zero)
  shows convolutionPairs(I, zero, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r)) ⊆ convolutionPairs(I, zero, p, q) ∪ convolutionPairs(I, zero, p, r)
proof
  have functionQ := polynomials.function with memberQ
  have functionR := polynomials.function with memberR
  have support := coefficientAdd.support at monomials(I), A, add, zero, neg, mul, one, q, r with *
  intros t ht
  unfold convolutionPairs at ht
  obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with ht
  have inUnion := support with v, hv
  have alternatives := union2.membership.forward with inUnion
  apply union2.membership.backward
  cases alternatives with inQ | inR
  . left
    unfold convolutionPairs
    rw shape
    exact product.pair with hu, inQ
  . right
    unfold convolutionPairs
    rw shape
    exact product.pair with hu, inR

theorem polynomialProduct.add_right (I A add zero neg mul one p q r : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  requires memberR : r ∈ polynomials(I, A, zero)
  shows polynomialProduct(I, A, add, zero, neg, mul, one, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r)) =
    coefficientAdd(monomials(I), A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), polynomialProduct(I, A, add, zero, neg, mul, one, p, r))
proof
  have finiteQ := convolutionPairs.finite with memberP, memberQ
  have finiteR := convolutionPairs.finite with memberP, memberR
  have finite := Finite.union with finiteQ, finiteR
  have domainQ := convolutionPairs.subset at I, zero, p, q
  have domainR := convolutionPairs.subset at I, zero, p, r
  have domain : convolutionPairs(I, zero, p, q) ∪ convolutionPairs(I, zero, p, r) ⊆ monomials(I) × monomials(I)
    simp [Subset, union2.membership]
  have coversQ : convolutionPairs(I, zero, p, q) ⊆ convolutionPairs(I, zero, p, q) ∪ convolutionPairs(I, zero, p, r)
    simp [Subset, union2.membership]
  have coversR : convolutionPairs(I, zero, p, r) ⊆ convolutionPairs(I, zero, p, q) ∪ convolutionPairs(I, zero, p, r)
    simp [Subset, union2.membership]
  have memberSum := polynomials.add at I, A, add, zero, neg, mul, one, q, r with *
  have coversSum := convolutionPairs.add_subset at I, A, add, zero, neg, mul, one, p, q, r with *
  have boundQ := polynomialProduct.on_domain with ring, memberP, memberQ, domain, finite, coversQ
  have boundR := polynomialProduct.on_domain with ring, memberP, memberR, domain, finite, coversR
  have boundSum := polynomialProduct.on_domain with ring, memberP, memberSum, domain, finite, coversSum
  have weightSum := boundedConvolutionWeights.add with ring, memberP, memberQ, memberR, domain
  have weightsQ := boundedConvolutionWeights.function at I, convolutionPairs(I, zero, p, q) ∪ convolutionPairs(I, zero, p, r), A, add, zero, neg, mul, one, p, q with *
  have weightsR := boundedConvolutionWeights.function at I, convolutionPairs(I, zero, p, q) ∪ convolutionPairs(I, zero, p, r), A, add, zero, neg, mul, one, p, r with *
  have distribute := finitePushforward.add at A, add, zero, neg, mul, one, convolutionPairs(I, zero, p, q) ∪ convolutionPairs(I, zero, p, r), monomials(I), monomialMul(I), boundedConvolutionWeights(I, convolutionPairs(I, zero, p, q) ∪ convolutionPairs(I, zero, p, r), A, add, zero, neg, mul, one, p, q), boundedConvolutionWeights(I, convolutionPairs(I, zero, p, q) ∪ convolutionPairs(I, zero, p, r), A, add, zero, neg, mul, one, p, r) with *
  cc

theorem polynomialProduct.add_left (I A add zero neg mul one p q r : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  requires memberR : r ∈ polynomials(I, A, zero)
  shows polynomialProduct(I, A, add, zero, neg, mul, one, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q), r) =
    coefficientAdd(monomials(I), A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, r), polynomialProduct(I, A, add, zero, neg, mul, one, q, r))
proof
  have memberSum := polynomials.add at I, A, add, zero, neg, mul, one, p, q with *
  have exchange := polynomialProduct.commutative at I, A, add, zero, neg, mul, one, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q), r with *
  have distribute := polynomialProduct.add_right at I, A, add, zero, neg, mul, one, r, p, q with *
  have first := polynomialProduct.commutative at I, A, add, zero, neg, mul, one, r, p with *
  have second := polynomialProduct.commutative at I, A, add, zero, neg, mul, one, r, q with *
  cc