-- Reconstructing sparse polynomials from coefficients in a chosen variable (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.HornerReconstruction
import CoefficientHorner
import MonomialShift

def monomialShift (I j m : Set, n : Nat) : Set := monomialProduct(I, coefficientSingle(I, ℕ, 0, n, j), m)

theorem monomialShift.member (I j m : Set, n : Nat)
  requires monomial : m ∈ monomials(I)
  shows monomialShift(I, j, m, n) ∈ monomials(I)
proof
  have single := monomialSingle.member at I, j, n with *
  unfold monomialShift
  exact monomialProduct.member with *

theorem monomialShift.zero (I j m : Set)
  requires monomial : m ∈ monomials(I)
  shows monomialShift(I, j, m, 0) = m
proof
  have unit := monomialOne.member at I
  have commute := monomialProduct.commutative at I, monomialOne(I), m with *
  have identity := monomialProduct.one at I, m with *
  unfold monomialShift
  rw monomialSingle.zero
  cc

theorem monomialShift.succ (I j m : Set, n : Nat)
  requires monomial : m ∈ monomials(I)
  requires index : j ∈ I
  shows monomialShift(I, j, m, succ(n)) = monomialProduct(I, monomialVariable(I, j), monomialShift(I, j, m, n))
proof
  have single := monomialSingle.member at I, j, n with *
  have variable := monomialVariable.member at I, j
  have step := monomialSingle.succ at I, j, n with *
  have successor := add.right_one with *
  rw successor at step
  have associative := monomialProduct.associative at I, monomialVariable(I, j), coefficientSingle(I, ℕ, 0, n, j), m with *
  unfold monomialShift
  cc

theorem monomialShift.exponent (I j m : Set, n : Nat)
  requires monomial : m ∈ monomials(I)
  requires index : j ∈ I
  requires absent : m(j) = 0
  shows monomialShift(I, j, m, n)(j) = n
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 value := monomialProduct.value at I, coefficientSingle(I, ℕ, 0, n, j), m, j with *
  have head := coefficientSingle.same at I, ℕ, 0, n, j with *
  have identity := add.right_unit with *
  unfold monomialShift
  cc

predicate coefficientsOmitVariable (I A z j cs : Set) :=
  ∀ n ∈ ℕ, ∀ m ∈ monomials(I), m(j) ≠ 0 → listCoefficient{polynomials(I, A, z)}(constantFunction(monomials(I), A, z), cs, n)(m) = z

section Coefficients
variable (I A add z neg mul one j m : Set)
hypothesis ring : IsCommRing(A, add, z, neg, mul, one)
hypothesis index : j ∈ I
hypothesis monomial : m ∈ monomials(I)
hypothesis absent : m(j) = 0

theorem polynomialFromCoefficients.coefficient (cs : List(polynomials(I, A, z))) (n : Nat)
  requires omitted : coefficientsOmitVariable(I, A, z, j, cs)
  shows polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, cs)(monomialShift(I, j, m, n)) = listCoefficient{polynomials(I, A, z)}(constantFunction(monomials(I), A, z), cs, n)(m)
proof
  induction cs generalizing n
  | List.nil =>
    intros n nNat omitted
    have ordinary := IsCommRing.ring with ring
    have zeroIn := IsRing.zero_in_carrier with ordinary
    have shifted := monomialShift.member at I, j, m, n with *
    have left := constantFunction.apply at monomials(I), A, monomialShift(I, j, m, n), z with *
    have right := constantFunction.apply at monomials(I), A, m, z with *
    rw [polynomialFromCoefficients.nil, listCoefficient.nil]
    cc
  | List.cons(c, tail) using ih =>
    intros n nNat omitted
    have coefficient : c ∈ polynomials(I, A, z) by assumption
    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 tailPolynomial := polynomialFromCoefficients.member at I, A, add, z, neg, mul, one, j, tail with *
    have variable := polynomialVariable.member at I, A, z, one, j with *
    have product := polynomialProduct.member at I, A, add, z, neg, mul, one, polynomialVariable(I, A, z, one, j), polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, tail) with *
    have productOperation := polynomialMul.apply at I, A, add, z, neg, mul, one, polynomialVariable(I, A, z, one, j), polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, tail) with *
    have sumOperation := polynomialAdd.apply at I, A, add, z, neg, mul, one, c, polynomialProduct(I, A, add, z, neg, mul, one, polynomialVariable(I, A, z, one, j), polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, tail)) with *
    have coefficientFunction := polynomials.function with coefficient
    have productFunction := polynomials.function with product
    have shifted := monomialShift.member at I, j, m, n with *
    have sumValue := coefficientAdd.value at monomials(I), A, add, z, neg, mul, one, c, polynomialProduct(I, A, add, z, neg, mul, one, polynomialVariable(I, A, z, one, j), polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, tail)), monomialShift(I, j, m, n) with *
    have equation := polynomialFromCoefficients.cons at I, A, add, z, neg, mul, one, j, c, tail with *
    rw [productOperation, sumOperation] at equation
    rw [equation, sumValue]
    have shape := natural.zero_or_successor with *
    cases shape with zero | successor
    . rw [zero, monomialShift.zero, listCoefficient.zero]
      have vanishes := polynomialProduct.variable_zero at I, A, add, z, neg, mul, one, j, m, polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, tail) with *
      have value := polynomials.coefficient at I, A, z, c, m with *
      rw vanishes
      exact IsRing.add_right_identity with ordinary, value
    . obtain ⟨k, kNat, equal⟩ := successor
      have nextShift := monomialShift.member at I, j, m, succ(k) with *
      have degree := monomialShift.exponent at I, j, m, succ(k) with *
      have positive : monomialShift(I, j, m, succ(k))(j) ≠ 0
        intro vanishes
        have impossible : 0 = succ(k) by cc
        exact Naturals.disjoint.zero.succ at k with impossible
      have zeroNatIn := nat.omega.forward with Naturals.constructor.zero
      have headZero := omitted with 0, zeroNatIn, monomialShift(I, j, m, succ(k)), nextShift, positive
      rw listCoefficient.zero at headZero
      have tailOmitted : coefficientsOmitVariable(I, A, z, j, tail)
        intros r rIn t ht present
        have rNat := nat.omega.backward with rIn
        have successorIn := nat.omega.forward at succ(r) with *
        have value := omitted with succ(r), successorIn, t, ht, present
        rwa listCoefficient.succ at value
      have rest := ih with k, kNat, tailOmitted
      have previous := monomialShift.member at I, j, m, k with *
      have variableMonomial := monomialVariable.member at I, j
      have shift := polynomialProduct.monomial_shift at I, A, add, z, neg, mul, one, monomialVariable(I, j), monomialShift(I, j, m, k), polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, tail) with *
      have step := monomialShift.succ at I, j, m, k with *
      have value := polynomials.coefficient at I, A, z, polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, tail), monomialShift(I, j, m, k) with *
      have identity := IsRing.add_left_identity with ordinary, value
      have shiftAt : polynomialProduct(I, A, add, z, neg, mul, one, polynomialVariable(I, A, z, one, j), polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, tail))(monomialShift(I, j, m, succ(k))) = polynomialFromCoefficients(I, A, add, z, neg, mul, one, j, tail)(monomialShift(I, j, m, k))
        rw step
        unfold polynomialVariable
        cc
      rwa [equal, listCoefficient.succ, headZero, shiftAt, identity]

end Coefficients
theorem polynomialVariableCoefficient.list_omits (I A z p j : Set) (cs : List(polynomials(I, A, z)))
  requires zeroIn : z ∈ A
  requires polynomial : p ∈ polynomials(I, A, z)
  requires coefficients : ∀ n, Nat(n) → listCoefficient{polynomials(I, A, z)}(constantFunction(monomials(I), A, z), cs, n) = polynomialVariableCoefficient(I, A, z, p, j, n)
  shows coefficientsOmitVariable(I, A, z, j, cs)
proof
  intros n nIn m hm present
  have natural := nat.omega.backward with nIn
  have value := coefficients with n, natural
  have vanishes := polynomialVariableCoefficient.at_nonzero with *
  cc

section Reconstruction
variable (I A add z neg mul one p j : Set)
notation ring R := (A, add, z, neg, mul, one)
notation ring P := R[I]
hypothesis ring : IsCommRing(R)
hypothesis polynomial : p ∈ P
hypothesis index : j ∈ I

theorem polynomialFromCoefficients.reconstruct (cs : List(P))
  requires coefficients : ∀ n, Nat(n) → listCoefficient{P}(P[0], cs, n) = polynomialVariableCoefficient(I, R, p, j, n)
  shows polynomialFromCoefficients(I, R, j, cs) = p
proof
  have zeroIn : R[0] ∈ R by typecheck
  have member := polynomialFromCoefficients.member at I, A, add, z, neg, mul, one, j, cs with *
  have omitted := polynomialVariableCoefficient.list_omits at I, A, z, p, j, cs with *
  apply polynomials.ext with member, polynomial
  intros m hm
  have exponent := monomials.exponent at I, m, j with *
  have erased := monomialErase.member at I, m, j with *
  have function := monomials.function with hm
  have naturalZero := nat.omega.forward with Naturals.constructor.zero
  have absent := coefficientErase.same at I, ℕ, (0:Nat), m, j with *
  have value := polynomialFromCoefficients.coefficient at I, A, add, z, neg, mul, one, j, coefficientErase(I, ℕ, (0:Nat), m, j), cs, m(j) with *
  have restore := monomialErase.restore at I, m, j with *
  have shape : monomialShift(I, j, coefficientErase(I, ℕ, (0:Nat), m, j), m(j)) = m
    unfold monomialShift
    cc
  have listValue := coefficients with m(j), exponent
  have recovery := polynomialVariableCoefficient.recover at I, A, z, p, j, m with *
  cc

theorem polynomials.exists_coefficient_horner
  shows ∃ cs, List(P, cs) ∧ coefficientsOmitVariable(I, A, z, j, cs) ∧ polynomialFromCoefficients(I, R, j, cs) = p
proof
  have zeroIn : R[0] ∈ R by typecheck
  obtain ⟨cs, list, coefficients⟩ := polynomialCoefficientFamily.list_representation at I, A, z, p, j with *
  have omitted := polynomialVariableCoefficient.list_omits with *
  have reconstruct := polynomialFromCoefficients.reconstruct with *
  refine ⟨cs, list, omitted, reconstruct⟩

theorem polynomials.exists_nonzero_coefficient_horner
  requires nonzero : p ≠ P[0]
  shows ∃ cs, List(P, cs) ∧ coefficientsOmitVariable(I, A, z, j, cs) ∧ polynomialFromCoefficients(I, R, j, cs) = p ∧ (∃ n ∈ ℕ, listCoefficient{P}(P[0], cs, n) ≠ P[0])
proof
  have zeroIn : R[0] ∈ R by typecheck
  obtain ⟨cs, list, coefficients⟩ := polynomialCoefficientFamily.list_representation at I, A, z, p, j with *
  have omitted := polynomialVariableCoefficient.list_omits with *
  have reconstruct := polynomialFromCoefficients.reconstruct with *
  obtain ⟨n, nIn, coefficient⟩ := polynomialVariableCoefficient.exists_nonzero at I, A, z, p, j with *
  have natural := nat.omega.backward with nIn
  have value := coefficients with n, natural
  refine ⟨cs, list, omitted, reconstruct, n, nIn, ?_⟩
  rwa value

theorem polynomialAt.reconstruction (v : Set) (cs : List(P))
  requires assignment : v : I → R
  requires coefficients : ∀ n, Nat(n) → listCoefficient{P}(P[0], cs, n) = polynomialVariableCoefficient(I, R, p, j, n)
  shows polynomialAt(I, R, v)(p) = hornerAt{A}(add, mul, z, v(j), listMap{P}(polynomialAt(I, R, v), cs))
proof
  have reconstruct := polynomialFromCoefficients.reconstruct with *
  have evaluation := polynomialAt.coefficient_horner with *
  cc

end Reconstruction