-- Multiplication of monomial terms and structural polynomial induction (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.Terms
import Unit
import CoefficientInduction

theorem polynomialTerm.support (I A zero a m : Set)
  requires zeroIn : zero ∈ A
  requires coefficient : a ∈ A
  shows functionSupport(polynomialTerm(I, A, zero, a, m), monomials(I), zero) ⊆ {m}
proof
  unfold polynomialTerm
  exact coefficientSingle.support with *

theorem polynomialProduct.terms (I A add zero neg mul one a b m n : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires coefficientA : a ∈ A
  requires coefficientB : b ∈ A
  requires monomialM : m ∈ monomials(I)
  requires monomialN : n ∈ monomials(I)
  shows polynomialProduct(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n)) = polynomialTerm(I, A, zero, call2(mul, a, b), monomialProduct(I, m, n))
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have memberP := polynomialTerm.member at I, A, zero, a, m with *
  have memberQ := polynomialTerm.member at I, A, zero, b, n with *
  have supportP := polynomialTerm.support at I, A, zero, a, m with *
  have supportQ := polynomialTerm.support at I, A, zero, b, n with *
  have singletons : {m} × {n} = {(m, n)}
    ext t
    constructor
    . intro ht
      obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with ht
      have equalU := singleton.membership.forward with hu
      have equalV := singleton.membership.forward with hv
      apply singleton.membership.backward
      cc
    . intro ht
      have shape := singleton.membership.forward with ht
      rw shape
      have hm := singleton.self at m
      have hn := singleton.self at n
      exact product.pair with hm, hn
  have covers : convolutionPairs(I, zero, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n)) ⊆ {(m, n)}
    unfold convolutionPairs
    rw ← singletons
    exact product.monotone with supportP, supportQ
  have pair := product.pair at m, n, monomials(I), monomials(I) with *
  have domain : {(m, n)} ⊆ monomials(I) × monomials(I) by simp [Subset, singleton.membership]
  have finite := Finite.singleton at (m, n)
  have weights := boundedConvolutionWeights.function at I, {(m, n)}, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n) with *
  have bounded := polynomialProduct.on_domain with ring, memberP, memberQ, domain, finite, covers
  have pushed := finitePushforward.singleton at monomials(I), A, add, zero, neg, mul, one, monomialMul(I), boundedConvolutionWeights(I, {(m, n)}, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n)), (m, n) with *
  have singleton := singleton.self at (m, n)
  have weight := boundedConvolutionWeights.pair at I, {(m, n)}, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n), m, n with *
  have valueP := polynomialTerm.same at I, A, zero, a, m with *
  have valueQ := polynomialTerm.same at I, A, zero, b, n with *
  have index := monomialMul.apply at I, m, n with *
  unfold call2 at index
  rw [← bounded, pushed, weight, valueP, valueQ, index]
  unfold polynomialTerm
  rfl

-- The property is represented by a set S; no extra induction axiom is used.
theorem polynomials.induction (I A add zero neg mul one S p : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires member : p ∈ polynomials(I, A, zero)
  requires base : constantFunction(monomials(I), A, zero) ∈ S
  requires terms : ∀ a ∈ A, ∀ m ∈ monomials(I), polynomialTerm(I, A, zero, a, m) ∈ S
  requires sums : ∀ f ∈ S, ∀ g ∈ S, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, f, g) ∈ S
  shows p ∈ S
proof
  have map := polynomials.map with member
  have step : ∀ a ∈ A, ∀ m ∈ monomials(I), ∀ f ∈ S, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, coefficientSingle(monomials(I), A, zero, a, m), f) ∈ S
    intros a ha m hm f hf
    have term := terms with a, ha, m, hm
    have result := sums with polynomialTerm(I, A, zero, a, m), term, f, hf
    unfold polynomialTerm at result
    exact result
  exact coefficientMaps.induction with *