-- Associativity of convolution by induction on finite sums of monomial terms.
-- 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.Associativity
import Terms

predicate PolynomialAssociates (I A add zero neg mul one p q r : Set) :=
  polynomialProduct(I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), r) = polynomialProduct(I, A, add, zero, neg, mul, one, p, polynomialProduct(I, A, add, zero, neg, mul, one, q, r))

def associatingFirsts (I A add zero neg mul one q r : Set) : Set :=
  {p ∈ polynomials(I, A, zero) | PolynomialAssociates(I, A, add, zero, neg, mul, one, p, q, r)}

def associatingMiddles (I A add zero neg mul one p r : Set) : Set :=
  {q ∈ polynomials(I, A, zero) | PolynomialAssociates(I, A, add, zero, neg, mul, one, p, q, r)}

def associatingThirds (I A add zero neg mul one p q : Set) : Set :=
  {r ∈ polynomials(I, A, zero) | PolynomialAssociates(I, A, add, zero, neg, mul, one, p, q, r)}

section Rings
variable (I A add zero neg mul one : Set)
hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)

theorem PolynomialAssociates.zero_first (q r : Set)
  requires memberQ : q ∈ polynomials(I, A, zero)
  requires memberR : r ∈ polynomials(I, A, zero)
  shows PolynomialAssociates(I, A, add, zero, neg, mul, one, constantFunction(monomials(I), A, zero), q, r)
proof
  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *
  have pair0 := polynomialProduct.member at I, A, add, zero, neg, mul, one, constantFunction(monomials(I), A, zero), q with *
  have pair1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, r with *
  have left0 := polynomialProduct.zero_left at I, A, add, zero, neg, mul, one, q with *
  have right0 := polynomialProduct.zero_right at I, A, add, zero, neg, mul, one, q with *
  have left1 := polynomialProduct.zero_left at I, A, add, zero, neg, mul, one, r with *
  have right1 := polynomialProduct.zero_right at I, A, add, zero, neg, mul, one, r with *
  have product := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, r with *
  have left2 := polynomialProduct.zero_left at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, q, r) with *
  have right2 := polynomialProduct.zero_right at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, q, r) with *
  unfold PolynomialAssociates
  cc

theorem PolynomialAssociates.zero_middle (p r : Set)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberR : r ∈ polynomials(I, A, zero)
  shows PolynomialAssociates(I, A, add, zero, neg, mul, one, p, constantFunction(monomials(I), A, zero), r)
proof
  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *
  have pair0 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, constantFunction(monomials(I), A, zero) with *
  have pair1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, constantFunction(monomials(I), A, zero), r with *
  have left0 := polynomialProduct.zero_left at I, A, add, zero, neg, mul, one, p with *
  have right0 := polynomialProduct.zero_right at I, A, add, zero, neg, mul, one, p with *
  have left1 := polynomialProduct.zero_left at I, A, add, zero, neg, mul, one, r with *
  have right1 := polynomialProduct.zero_right at I, A, add, zero, neg, mul, one, r with *
  have product := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, r with *
  have left2 := polynomialProduct.zero_left at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, r) with *
  have right2 := polynomialProduct.zero_right at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, r) with *
  unfold PolynomialAssociates
  cc

theorem PolynomialAssociates.zero_third (p q : Set)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  shows PolynomialAssociates(I, A, add, zero, neg, mul, one, p, q, constantFunction(monomials(I), A, zero))
proof
  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *
  have pair0 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *
  have pair1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, constantFunction(monomials(I), A, zero) with *
  have left0 := polynomialProduct.zero_left at I, A, add, zero, neg, mul, one, p with *
  have right0 := polynomialProduct.zero_right at I, A, add, zero, neg, mul, one, p with *
  have left1 := polynomialProduct.zero_left at I, A, add, zero, neg, mul, one, q with *
  have right1 := polynomialProduct.zero_right at I, A, add, zero, neg, mul, one, q with *
  have product := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *
  have left2 := polynomialProduct.zero_left at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q) with *
  have right2 := polynomialProduct.zero_right at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q) with *
  unfold PolynomialAssociates
  cc

theorem PolynomialAssociates.add_first (p q r s : Set)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  requires memberR : r ∈ polynomials(I, A, zero)
  requires memberS : s ∈ polynomials(I, A, zero)
  requires first : PolynomialAssociates(I, A, add, zero, neg, mul, one, p, q, r)
  requires second : PolynomialAssociates(I, A, add, zero, neg, mul, one, s, q, r)
  shows PolynomialAssociates(I, A, add, zero, neg, mul, one, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, s), q, r)
proof
  have pair0 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *
  have pair1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, r with *
  have pair2 := polynomialProduct.member at I, A, add, zero, neg, mul, one, s, q with *
  have distribute0 := polynomialProduct.add_left at I, A, add, zero, neg, mul, one, p, s, q with *
  have distribute1 := polynomialProduct.add_left at 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, s, q), r with *
  have distribute2 := polynomialProduct.add_left at I, A, add, zero, neg, mul, one, p, s, polynomialProduct(I, A, add, zero, neg, mul, one, q, r) with *
  unfold PolynomialAssociates at first
  unfold PolynomialAssociates at second
  unfold PolynomialAssociates
  cc

theorem PolynomialAssociates.add_middle (p q r s : Set)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  requires memberR : r ∈ polynomials(I, A, zero)
  requires memberS : s ∈ polynomials(I, A, zero)
  requires first : PolynomialAssociates(I, A, add, zero, neg, mul, one, p, q, r)
  requires second : PolynomialAssociates(I, A, add, zero, neg, mul, one, p, s, r)
  shows PolynomialAssociates(I, A, add, zero, neg, mul, one, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, s), r)
proof
  have pair0 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *
  have pair1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, s with *
  have pair2 := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, r with *
  have pair3 := polynomialProduct.member at I, A, add, zero, neg, mul, one, s, r with *
  have distribute0 := polynomialProduct.add_right at I, A, add, zero, neg, mul, one, p, q, s with *
  have distribute1 := polynomialProduct.add_left at 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, s), r with *
  have distribute2 := polynomialProduct.add_left at I, A, add, zero, neg, mul, one, q, s, r with *
  have distribute3 := polynomialProduct.add_right at I, A, add, zero, neg, mul, one, p, polynomialProduct(I, A, add, zero, neg, mul, one, q, r), polynomialProduct(I, A, add, zero, neg, mul, one, s, r) with *
  unfold PolynomialAssociates at first
  unfold PolynomialAssociates at second
  unfold PolynomialAssociates
  cc

theorem PolynomialAssociates.add_third (p q r s : Set)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  requires memberR : r ∈ polynomials(I, A, zero)
  requires memberS : s ∈ polynomials(I, A, zero)
  requires first : PolynomialAssociates(I, A, add, zero, neg, mul, one, p, q, r)
  requires second : PolynomialAssociates(I, A, add, zero, neg, mul, one, p, q, s)
  shows PolynomialAssociates(I, A, add, zero, neg, mul, one, p, q, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, r, s))
proof
  have pair0 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *
  have pair1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, r with *
  have pair2 := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, s with *
  have distribute0 := polynomialProduct.add_right at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), r, s with *
  have distribute1 := polynomialProduct.add_right at I, A, add, zero, neg, mul, one, q, r, s with *
  have distribute2 := polynomialProduct.add_right at I, A, add, zero, neg, mul, one, p, polynomialProduct(I, A, add, zero, neg, mul, one, q, r), polynomialProduct(I, A, add, zero, neg, mul, one, q, s) with *
  unfold PolynomialAssociates at first
  unfold PolynomialAssociates at second
  unfold PolynomialAssociates
  cc

theorem PolynomialAssociates.terms (a b c m n k : Set)
  requires coefficientA : a ∈ A
  requires coefficientB : b ∈ A
  requires coefficientC : c ∈ A
  requires monomialM : m ∈ monomials(I)
  requires monomialN : n ∈ monomials(I)
  requires monomialK : k ∈ monomials(I)
  shows PolynomialAssociates(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n), polynomialTerm(I, A, zero, c, k))
proof
  have ordinary := IsCommRing.ring with ring
  have ab := IsRing.mul_closed at A, add, zero, neg, mul, one, a, b with *
  have bc := IsRing.mul_closed at A, add, zero, neg, mul, one, b, c with *
  have mn := monomialProduct.member at I, m, n with *
  have nk := monomialProduct.member at I, n, k with *
  have product0 := polynomialProduct.terms at I, A, add, zero, neg, mul, one, a, b, m, n with *
  have product1 := polynomialProduct.terms at I, A, add, zero, neg, mul, one, b, c, n, k with *
  have product2 := polynomialProduct.terms at I, A, add, zero, neg, mul, one, call2(mul, a, b), c, monomialProduct(I, m, n), k with *
  have product3 := polynomialProduct.terms at I, A, add, zero, neg, mul, one, a, call2(mul, b, c), m, monomialProduct(I, n, k) with *
  have coefficients : call2(mul, call2(mul, a, b), c) = call2(mul, a, call2(mul, b, c)) by ring
  have monomials := monomialProduct.associative at I, m, n, k with *
  unfold PolynomialAssociates
  cc

theorem PolynomialAssociates.two_terms (a b m n r : Set)
  requires coefficientA : a ∈ A
  requires coefficientB : b ∈ A
  requires monomialM : m ∈ monomials(I)
  requires monomialN : n ∈ monomials(I)
  requires memberR : r ∈ polynomials(I, A, zero)
  shows PolynomialAssociates(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n), r)
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *
  have termA := polynomialTerm.member at I, A, zero, a, m with *
  have termB := polynomialTerm.member at I, A, zero, b, n with *
  have base : constantFunction(monomials(I), A, zero) ∈ associatingThirds(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n))
    apply associatingThirds.membership.backward
    constructor
    . exact zeroPolynomial
    . exact PolynomialAssociates.zero_third with *
  have terms : ∀ d ∈ A, ∀ j ∈ monomials(I), polynomialTerm(I, A, zero, d, j) ∈ associatingThirds(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n))
    intros d hd j hj
    have member := polynomialTerm.member at I, A, zero, d, j with *
    apply associatingThirds.membership.backward
    constructor
    . exact member
    . exact PolynomialAssociates.terms with *
  have sums : ∀ f ∈ associatingThirds(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n)), ∀ g ∈ associatingThirds(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n)), coefficientAdd(monomials(I), A, add, zero, neg, mul, one, f, g) ∈ associatingThirds(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n))
    intros f hf g hg
    have first := associatingThirds.membership.forward with hf
    have second := associatingThirds.membership.forward with hg
    have member := polynomials.add at I, A, add, zero, neg, mul, one, f, g with *
    apply associatingThirds.membership.backward
    constructor
    . exact member
    . exact PolynomialAssociates.add_third with *
  have generated := polynomials.induction at I, A, add, zero, neg, mul, one, associatingThirds(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n)), r with *
  have result := associatingThirds.membership.forward with generated
  exact result.right

theorem PolynomialAssociates.one_term (a m q r : Set)
  requires coefficientA : a ∈ A
  requires monomialM : m ∈ monomials(I)
  requires memberQ : q ∈ polynomials(I, A, zero)
  requires memberR : r ∈ polynomials(I, A, zero)
  shows PolynomialAssociates(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), q, r)
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *
  have termA := polynomialTerm.member at I, A, zero, a, m with *
  have base : constantFunction(monomials(I), A, zero) ∈ associatingMiddles(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), r)
    apply associatingMiddles.membership.backward
    constructor
    . exact zeroPolynomial
    . exact PolynomialAssociates.zero_middle with *
  have terms : ∀ d ∈ A, ∀ j ∈ monomials(I), polynomialTerm(I, A, zero, d, j) ∈ associatingMiddles(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), r)
    intros d hd j hj
    have member := polynomialTerm.member at I, A, zero, d, j with *
    apply associatingMiddles.membership.backward
    constructor
    . exact member
    . exact PolynomialAssociates.two_terms with *
  have sums : ∀ f ∈ associatingMiddles(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), r), ∀ g ∈ associatingMiddles(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), r), coefficientAdd(monomials(I), A, add, zero, neg, mul, one, f, g) ∈ associatingMiddles(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), r)
    intros f hf g hg
    have first := associatingMiddles.membership.forward with hf
    have second := associatingMiddles.membership.forward with hg
    have member := polynomials.add at I, A, add, zero, neg, mul, one, f, g with *
    apply associatingMiddles.membership.backward
    constructor
    . exact member
    . exact PolynomialAssociates.add_middle with *
  have generated := polynomials.induction at I, A, add, zero, neg, mul, one, associatingMiddles(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), r), q with *
  have result := associatingMiddles.membership.forward with generated
  exact result.right

theorem polynomialProduct.associative (p q r : Set)
  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, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), r) = polynomialProduct(I, A, add, zero, neg, mul, one, p, polynomialProduct(I, A, add, zero, neg, mul, one, q, r))
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *
  have base : constantFunction(monomials(I), A, zero) ∈ associatingFirsts(I, A, add, zero, neg, mul, one, q, r)
    apply associatingFirsts.membership.backward
    constructor
    . exact zeroPolynomial
    . exact PolynomialAssociates.zero_first with *
  have terms : ∀ d ∈ A, ∀ j ∈ monomials(I), polynomialTerm(I, A, zero, d, j) ∈ associatingFirsts(I, A, add, zero, neg, mul, one, q, r)
    intros d hd j hj
    have member := polynomialTerm.member at I, A, zero, d, j with *
    apply associatingFirsts.membership.backward
    constructor
    . exact member
    . exact PolynomialAssociates.one_term with *
  have sums : ∀ f ∈ associatingFirsts(I, A, add, zero, neg, mul, one, q, r), ∀ g ∈ associatingFirsts(I, A, add, zero, neg, mul, one, q, r), coefficientAdd(monomials(I), A, add, zero, neg, mul, one, f, g) ∈ associatingFirsts(I, A, add, zero, neg, mul, one, q, r)
    intros f hf g hg
    have first := associatingFirsts.membership.forward with hf
    have second := associatingFirsts.membership.forward with hg
    have member := polynomials.add at I, A, add, zero, neg, mul, one, f, g with *
    apply associatingFirsts.membership.backward
    constructor
    . exact member
    . exact PolynomialAssociates.add_first with *
  have generated := polynomials.induction at I, A, add, zero, neg, mul, one, associatingFirsts(I, A, add, zero, neg, mul, one, q, r), p with *
  have result := associatingFirsts.membership.forward with generated
  exact result.right

end Rings