-- Algebraic laws for the constructed finite convolution (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.ConvolutionLaws
import Convolution
import Ring.PushforwardTransport

theorem polynomialProduct.commutative (I A add zero neg mul one p q : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  shows polynomialProduct(I, A, add, zero, neg, mul, one, p, q) = polynomialProduct(I, A, add, zero, neg, mul, one, q, p)
proof
  have finite := convolutionPairs.finite at I, A, zero, p, q with *
  have weightsPQ := convolutionWeights.function at I, A, add, zero, neg, mul, one, p, q with *
  have weightsQP := convolutionWeights.function at I, A, add, zero, neg, mul, one, q, p with *
  have swap : BijectiveBetween(productSwap(functionSupport(p, monomials(I), zero), functionSupport(q, monomials(I), zero)), convolutionPairs(I, zero, p, q), convolutionPairs(I, zero, q, p))
    unfold convolutionPairs
    exact productSwap.bijective
  have indices : ∀ t ∈ convolutionPairs(I, zero, p, q), monomialMul(I)(t) = monomialMul(I)(productSwap(functionSupport(p, monomials(I), zero), functionSupport(q, monomials(I), zero))(t))
    intros t ht
    unfold convolutionPairs at ht
    obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with ht
    have dataU := functionSupport.membership.forward with hu
    have dataV := functionSupport.membership.forward with hv
    have swapped := productSwap.pair with hu, hv
    have first := monomialMul.apply at I, u, v with *
    have second := monomialMul.apply at I, v, u with *
    have comm := monomialProduct.commutative at I, u, v with *
    unfold call2 at first
    unfold call2 at second
    cc
  have weights : ∀ t ∈ convolutionPairs(I, zero, p, q), convolutionWeights(I, A, add, zero, neg, mul, one, p, q)(t) = convolutionWeights(I, A, add, zero, neg, mul, one, q, p)(productSwap(functionSupport(p, monomials(I), zero), functionSupport(q, monomials(I), zero))(t))
    intros t ht
    unfold convolutionPairs at ht
    obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with ht
    have dataU := functionSupport.membership.forward with hu
    have dataV := functionSupport.membership.forward with hv
    have coefficientP := polynomials.coefficient at I, A, zero, p, u with *
    have coefficientQ := polynomials.coefficient at I, A, zero, q, v with *
    have swapped := productSwap.pair with hu, hv
    have first := convolutionWeights.pair with hu, hv
    have second := convolutionWeights.pair with hv, hu
    have comm : call2(mul, p(u), q(v)) = call2(mul, q(v), p(u)) by ring
    cc
  unfold polynomialProduct
  exact finitePushforward.reindex with *