-- Multiplication by a monomial shifts coefficients without collisions (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.MonomialShift
import Ring
import Terms

def monomialShiftCorrect (I A add z neg mul one t m : Set) : Set :=
  {p ∈ polynomials(I, A, z) | polynomialProduct(I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), p)(monomialProduct(I, t, m)) = p(m)}

section Shift
variable (I A add z neg mul one t m : Set)
notation ring R := (A, add, z, neg, mul, one)
notation ring P := R[I]
hypothesis ring : IsCommRing(R)
hypothesis monomial : t ∈ monomials(I)
hypothesis target : m ∈ monomials(I)

theorem monomialShiftCorrect.zero
  shows P[0] ∈ monomialShiftCorrect(I, A, add, z, neg, mul, one, t, m)
proof
  have zeroIn : R[0] ∈ R by typecheck
  have oneIn : R[1] ∈ R by typecheck
  have zeroPoly := polynomials.zero at I, A, add, z, neg, mul, one with *
  have term := polynomialTerm.member at I, A, z, one, t with *
  have shifted := monomialProduct.member at I, t, m with *
  have product := polynomialProduct.zero_right at I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t) with *
  have left := constantFunction.apply at monomials(I), A, monomialProduct(I, t, m), z with *
  have right := constantFunction.apply at monomials(I), A, m, z with *
  apply monomialShiftCorrect.membership.backward
  refine ⟨zeroPoly, ?_⟩
  cc

theorem monomialShiftCorrect.term (a n : Set)
  requires coefficient : a ∈ R
  requires index : n ∈ monomials(I)
  shows polynomialTerm(I, A, z, a, n) ∈ monomialShiftCorrect(I, A, add, z, neg, mul, one, t, m)
proof
  have zeroIn : R[0] ∈ R by typecheck
  have oneIn : R[1] ∈ R by typecheck
  have member := polynomialTerm.member at I, A, z, a, n with *
  have shifted := monomialProduct.member at I, t, m with *
  have product := polynomialProduct.terms at I, A, add, z, neg, mul, one, one, a, t, n with *
  have unit : R[1 * a] = a by ring
  rw unit at product
  apply monomialShiftCorrect.membership.backward
  refine ⟨member, ?_⟩
  rw product
  have alternatives : m = n ∨ m ≠ n by tauto
  cases alternatives with equal | different
  . rw equal
    have shiftedN := monomialProduct.member at I, t, n with *
    have left := polynomialTerm.same at I, A, z, a, monomialProduct(I, t, n) with *
    have right := polynomialTerm.same at I, A, z, a, n with *
    cc
  . have distinct : monomialProduct(I, t, m) ≠ monomialProduct(I, t, n)
      intro equal
      have cancelled := monomialProduct.cancel with *
      exact different with cancelled
    have left := polynomialTerm.other at I, A, z, a, monomialProduct(I, t, n), monomialProduct(I, t, m) with *
    have right := polynomialTerm.other at I, A, z, a, n, m with *
    cc

theorem monomialShiftCorrect.add (p q : Set)
  requires first : p ∈ monomialShiftCorrect(I, A, add, z, neg, mul, one, t, m)
  requires second : q ∈ monomialShiftCorrect(I, A, add, z, neg, mul, one, t, m)
  shows coefficientAdd(monomials(I), A, add, z, neg, mul, one, p, q) ∈ monomialShiftCorrect(I, A, add, z, neg, mul, one, t, m)
proof
  have left := monomialShiftCorrect.membership.forward with first
  have right := monomialShiftCorrect.membership.forward with second
  have zeroIn : R[0] ∈ R by typecheck
  have oneIn : R[1] ∈ R by typecheck
  have term := polynomialTerm.member at I, A, z, one, t with *
  have shifted := monomialProduct.member at I, t, m with *
  have sum := polynomials.add at I, A, add, z, neg, mul, one, p, q with *
  have productP := polynomialProduct.member at I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), p with *
  have productQ := polynomialProduct.member at I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), q with *
  have functionP := polynomials.function with left.left
  have functionQ := polynomials.function with right.left
  have functionProductP := polynomials.function with productP
  have functionProductQ := polynomials.function with productQ
  have distributes := polynomialProduct.add_right at I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), p, q with *
  have value := coefficientAdd.value at monomials(I), A, add, z, neg, mul, one, p, q, m with *
  have productValue := coefficientAdd.value at monomials(I), A, add, z, neg, mul, one, polynomialProduct(I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), p), polynomialProduct(I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), q), monomialProduct(I, t, m) with *
  apply monomialShiftCorrect.membership.backward
  refine ⟨sum, ?_⟩
  cc

theorem polynomialProduct.monomial_shift (p : Set)
  requires polynomial : p ∈ P
  shows polynomialProduct(I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), p)(monomialProduct(I, t, m)) = p(m)
proof
  have base := monomialShiftCorrect.zero at I, A, add, z, neg, mul, one, t, m with *
  have terms : ∀ a ∈ A, ∀ n ∈ monomials(I), polynomialTerm(I, A, z, a, n) ∈ monomialShiftCorrect(I, A, add, z, neg, mul, one, t, m)
    intros a ha n hn
    exact monomialShiftCorrect.term with *
  have sums : ∀ u ∈ monomialShiftCorrect(I, A, add, z, neg, mul, one, t, m), ∀ v ∈ monomialShiftCorrect(I, A, add, z, neg, mul, one, t, m), coefficientAdd(monomials(I), A, add, z, neg, mul, one, u, v) ∈ monomialShiftCorrect(I, A, add, z, neg, mul, one, t, m)
    intros u hu v hv
    exact monomialShiftCorrect.add with *
  have member := polynomials.induction with *
  have data := monomialShiftCorrect.membership.forward with member
  exact data.right

end Shift
theorem polynomialProduct.monomial_outside (I A add z neg mul one t m p : Set)
  requires ring : IsCommRing(A, add, z, neg, mul, one)
  requires monomial : t ∈ monomials(I)
  requires target : m ∈ monomials(I)
  requires polynomial : p ∈ polynomials(I, A, z)
  requires absent : ∀ n ∈ monomials(I), m ≠ monomialProduct(I, t, n)
  shows polynomialProduct(I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), p)(m) = z
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have multiplicative := IsRing.multiplicative with ordinary
  have oneIn := IsMonoid.unit_in_carrier with multiplicative
  have term := polynomialTerm.member at I, A, z, one, t with *
  have bound := polynomialTerm.support at I, A, z, one, t with *
  by_contra nonzero
  have supported : m ∈ functionSupport(polynomialProduct(I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), p), monomials(I), z)
    exact functionSupport.membership.backward with ⟨target, nonzero⟩
  obtain ⟨u, hu, n, hn, equal⟩ := polynomialProduct.support_factor at I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), p, m with *
  have singleton := bound with u, hu
  have same := singleton.membership.forward with singleton
  have data := functionSupport.membership.forward with hn
  have different := absent with n, data.left
  apply different
  cc

-- A variable multiple has no term with zero exponent in that variable.
theorem polynomialProduct.variable_zero (I A add z neg mul one j m p : Set)
  requires ring : IsCommRing(A, add, z, neg, mul, one)
  requires index : j ∈ I
  requires target : m ∈ monomials(I)
  requires polynomial : p ∈ polynomials(I, A, z)
  requires exponent : m(j) = 0
  shows polynomialProduct(I, A, add, z, neg, mul, one, polynomialVariable(I, A, z, one, j), p)(m) = z
proof
  have variable := monomialVariable.member at I, j
  have absent : ∀ n ∈ monomials(I), m ≠ monomialProduct(I, monomialVariable(I, j), n)
    intros n hn equal
    have nNat := monomials.exponent with hn
    have variableValue := monomialVariable.same at I, j with *
    have productValue := monomialProduct.value at I, monomialVariable(I, j), n, j with *
    have impossible : 0 = succ(n(j))
      have sum : 0 = 1 + n(j) by cc
      rwa [add, add] at sum
    exact Naturals.disjoint.zero.succ at n(j) with impossible
  unfold polynomialVariable
  exact polynomialProduct.monomial_outside with *