-- Coefficients in one variable, as sparse polynomials in the remaining variables (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.VariableCoefficients
import Variables
import MonomialGeneration

defgraph monomialErasure (I j : Set) (m ∈ monomials(I)) : monomials(I) := coefficientErase(I, ℕ, 0, m, j)
proof
  exact monomialErase.member with *

theorem monomialErase.fixed (I m j : Set)
  requires member : m ∈ monomials(I)
  requires absent : m(j) = 0
  shows coefficientErase(I, ℕ, 0, m, j) = m
proof
  have zeroIn := nat.omega.forward with Naturals.constructor.zero
  have function := monomials.function with member
  have erased := coefficientErase.function at I, ℕ, 0, m, j with *
  apply FunctionBetween.ext with erased, function
  intros i hi
  have alternatives : i = j ∨ i ≠ j by tauto
  cases alternatives with same | different
  . rw same
    have index : j ∈ I by cc
    have value := coefficientErase.same with zeroIn, function, index
    cc
  . exact coefficientErase.other with *

theorem monomialErase.insert (I m j : Set, n : Nat)
  requires member : m ∈ monomials(I)
  requires absent : m(j) = 0
  shows coefficientErase(I, ℕ, 0, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m), j) = m
proof
  have zeroIn := nat.omega.forward with Naturals.constructor.zero
  have nIn := nat.omega.forward at n with *
  have single := monomialSingle.member at I, j, n with *
  have product := monomialProduct.member at I, coefficientSingle(I, ℕ, 0, n, j), m with *
  have function := monomials.function with product
  have erased := coefficientErase.function at I, ℕ, 0, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m), j with *
  have original := monomials.function with member
  apply FunctionBetween.ext with erased, original
  intros i hi
  have alternatives : i = j ∨ i ≠ j by tauto
  cases alternatives with same | different
  . rw same
    have index : j ∈ I by cc
    have value := coefficientErase.same at I, ℕ, 0, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m), j with *
    cc
  . have value := coefficientErase.other at I, ℕ, 0, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m), j, i with *
    have productValue := monomialProduct.value at I, coefficientSingle(I, ℕ, 0, n, j), m, i with *
    have singleValue := coefficientSingle.other at I, ℕ, 0, n, j, i with *
    have natural := monomials.exponent at I, m, i with *
    rw [value, productValue, singleValue]
    exact add.left_unit at m(i) with *

-- At a monomial with zero j-exponent, read the coefficient after inserting n copies of j.
-- At every other monomial the result is zero, so the coefficient polynomial omits j.
defgraph polynomialVariableCoefficient (I A z p j : Set, n : Nat) (m ∈ monomials(I)) : A :=
  singleValue(A, z, p(monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m)), 0, m(j))
requires zeroIn : z ∈ A
requires polynomial : p ∈ polynomials(I, A, z)
proof
  have single := monomialSingle.member at I, j, n with *
  have product := monomialProduct.member at I, coefficientSingle(I, ℕ, 0, n, j), m with *
  have coefficient := polynomials.coefficient at I, A, z, p, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m) with *
  exact singleValue.closed with *

notation scoped polynomialVariableCoefficient(I, R, p, j, n) => polynomialVariableCoefficient(I, R.carrier, R.zero, p, j, n)

section Coefficients
variable (I A z p j : Set)
hypothesis zeroIn : z ∈ A
hypothesis polynomial : p ∈ polynomials(I, A, z)

theorem polynomialVariableCoefficient.at_zero (n : Nat, m : Set)
  requires member : m ∈ monomials(I)
  requires absent : m(j) = 0
  shows polynomialVariableCoefficient(I, A, z, p, j, n)(m) = p(monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m))
proof
  have single := monomialSingle.member at I, j, n with *
  have product := monomialProduct.member at I, coefficientSingle(I, ℕ, 0, n, j), m with *
  have coefficient := polynomials.coefficient at I, A, z, p, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m) with *
  have value := polynomialVariableCoefficient.value at I, A, z, p, j, n, m with *
  have selected := singleValue.same at A, z, p(monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m)), 0, m(j) with *
  cc

theorem polynomialVariableCoefficient.at_nonzero (n : Nat, m : Set)
  requires member : m ∈ monomials(I)
  requires present : m(j) ≠ 0
  shows polynomialVariableCoefficient(I, A, z, p, j, n)(m) = z
proof
  have single := monomialSingle.member at I, j, n with *
  have product := monomialProduct.member at I, coefficientSingle(I, ℕ, 0, n, j), m with *
  have coefficient := polynomials.coefficient at I, A, z, p, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m) with *
  have value := polynomialVariableCoefficient.value at I, A, z, p, j, n, m with *
  have selected := singleValue.other at A, z, p(monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m)), 0, m(j) with *
  cc

theorem polynomialVariableCoefficient.support (n : Nat)
  shows functionSupport(polynomialVariableCoefficient(I, A, z, p, j, n), monomials(I), z) ⊆ functionImage(monomialErasure(I, j), functionSupport(p, monomials(I), z), monomials(I))
proof
  intros m hm
  have data := functionSupport.membership.forward with hm
  have absent : m(j) = 0
    by_contra present
    have vanishes := polynomialVariableCoefficient.at_nonzero at I, A, z, p, j, n, m with *
    exact data.right with vanishes
  have single := monomialSingle.member at I, j, n with *
  have product := monomialProduct.member at I, coefficientSingle(I, ℕ, 0, n, j), m with *
  have value := polynomialVariableCoefficient.at_zero at I, A, z, p, j, n, m with *
  have nonzero : p(monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m)) ≠ z
    rw ← value
    exact data.right
  have supported : monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m) ∈ functionSupport(p, monomials(I), z)
    exact functionSupport.membership.backward with ⟨product, nonzero⟩
  have erased := monomialErase.insert at I, m, j, n with *
  have imageValue := monomialErasure.value at I, j, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m) with *
  apply functionImage.membership.backward
  refine ⟨data.left, monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m), supported, ?_⟩
  cc

theorem polynomialVariableCoefficient.member (n : Nat)
  shows polynomialVariableCoefficient(I, A, z, p, j, n) ∈ polynomials(I, A, z)
proof
  have function := polynomialVariableCoefficient.function at I, A, z, p, j, n with *
  have support := polynomialVariableCoefficient.support at I, A, z, p, j, n with *
  have finite := polynomials.finite_support with polynomial
  have domain := functionSupport.subset at p, monomials(I), z
  have erasure := monomialErasure.function at I, j
  have imageFinite := Finite.function_image with erasure, finite, domain
  have finiteSupport := Finite.subset with imageFinite, support
  apply polynomials.contains
  unfold CoefficientMap
  refine ⟨function, finiteSupport⟩

theorem polynomialVariableCoefficient.recover (m : Set)
  requires member : m ∈ monomials(I)
  requires index : j ∈ I
  shows polynomialVariableCoefficient(I, A, z, p, j, m(j))(coefficientErase(I, ℕ, 0, m, j)) = p(m)
proof
  have naturalZero := nat.omega.forward with Naturals.constructor.zero
  have function := monomials.function with member
  have exponent := monomials.exponent at I, m, j with *
  have erased := monomialErase.member at I, m, j with *
  have absent := coefficientErase.same at I, ℕ, 0, m, j with *
  have value := polynomialVariableCoefficient.at_zero at I, A, z, p, j, m(j), coefficientErase(I, ℕ, 0, m, j) with *
  have restore := monomialErase.restore at I, m, j with *
  cc

theorem polynomialVariableCoefficient.variables (n : Nat)
  shows polynomialVariablesUsed(I, A, z, polynomialVariableCoefficient(I, A, z, p, j, n)) ⊆ polynomialVariablesUsed(I, A, z, p) ∖ {j}
proof
  have bound := polynomialVariableCoefficient.support at I, A, z, p, j, n with *
  intros i hi
  obtain ⟨m, support, used⟩ := polynomialVariablesUsed.membership.forward with hi
  have image := bound with m, support
  obtain ⟨member, t, supported, equal⟩ := functionImage.membership.forward with image
  have data := functionSupport.membership.forward with supported
  have value := monomialErasure.value at I, j, t with data.left
  have same : m = coefficientErase(I, ℕ, 0, t, j) by cc
  have naturalZero := nat.omega.forward with Naturals.constructor.zero
  have function := monomials.function with data.left
  have erasedSupport := coefficientErase.support at I, ℕ, 0, t, j with *
  rw same at used
  have inDifference := erasedSupport with i, used
  have old := difference.membership.forward with inDifference
  have original : i ∈ polynomialVariablesUsed(I, A, z, p)
    exact polynomialVariablesUsed.membership.backward with ⟨t, supported, old.left⟩
  exact difference.membership.backward with ⟨original, old.right⟩

theorem polynomialVariableCoefficient.ext (q : Set)
  requires other : q ∈ polynomials(I, A, z)
  requires index : j ∈ I
  requires coefficients : ∀ n ∈ ℕ, polynomialVariableCoefficient(I, A, z, p, j, n) = polynomialVariableCoefficient(I, A, z, q, j, n)
  shows p = q
proof
  apply polynomials.ext with polynomial, other
  intros m hm
  have exponent := monomials.exponent with *
  have exponentIn := nat.omega.forward at m(j) with *
  have equal := coefficients with m(j), exponentIn
  have left := polynomialVariableCoefficient.recover at I, A, z, p, j, m with *
  have right := polynomialVariableCoefficient.recover at I, A, z, q, j, m with *
  cc

theorem polynomialVariableCoefficient.exists_nonzero
  requires index : j ∈ I
  requires nonzero : p ≠ constantFunction(monomials(I), A, z)
  shows ∃ n ∈ ℕ, polynomialVariableCoefficient(I, A, z, p, j, n) ≠ constantFunction(monomials(I), A, z)
proof
  by_contra none
  apply nonzero
  have function := polynomials.function with polynomial
  have zeroFunction := constantFunction.function at monomials(I), A, z with *
  apply FunctionBetween.ext with function, zeroFunction
  intros m hm
  have exponent := monomials.exponent with *
  have exponentIn := nat.omega.forward at m(j) with *
  have equal : polynomialVariableCoefficient(I, A, z, p, j, m(j)) = constantFunction(monomials(I), A, z)
    by_contra different
    apply none
    refine ⟨m(j), exponentIn, different⟩
  have erased := monomialErase.member at I, m, j with *
  have recovery := polynomialVariableCoefficient.recover at I, A, z, p, j, m with *
  have erasedZero := constantFunction.apply at monomials(I), A, coefficientErase(I, ℕ, 0, m, j), z with *
  have originalZero := constantFunction.apply at monomials(I), A, m, z with *
  cc

end Coefficients