-- Horner coefficient lists as sparse polynomials, with evaluation compatibility.
-- 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.HornerPolynomial
import HornerRoots
import Assignment
import Constants

-- The result is an element of the finite-support polynomial ring.
def polynomialFromHorner (I A add z neg mul one j leading : Set) (cs : List(A)) : Set :=
  monicValue{A}(polynomialCoefficients(I, A, z), polynomialAdd(I, A, add, z, neg, mul, one), polynomialMul(I, A, add, z, neg, mul, one), polynomialConstant(I, A, z, leading), polynomialVariable(I, A, z, one, j), cs)

notation scoped polynomialFromHorner(I, R, j, leading, cs) => polynomialFromHorner(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, j, leading, cs)

theorem polynomialFromHorner.nil (I A add z neg mul one j leading : Set)
  shows polynomialFromHorner(I, A, add, z, neg, mul, one, j, leading, []) = polynomialConstant(I, A, z, leading)
proof
  unfold polynomialFromHorner
  rw monicValue
  rfl

section Rings
variable (I A add z neg mul one j leading : Set)
notation ring R := (A, add, z, neg, mul, one)
notation ring P := R[I]
hypothesis ring : IsCommRing(R)
hypothesis initial : leading ∈ R

theorem polynomialFromHorner.member (cs : List(A))
  shows polynomialFromHorner(I, R, j, leading, cs) ∈ P
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have monoid := IsRing.multiplicative with ordinary
  have oneIn := IsMonoid.unit_in_carrier with monoid
  have variable := polynomialVariable.member at I, A, z, one, j with *
  have constant := polynomialConstant.member at I, A, z, leading with *
  have target : IsCommRing(P)
    exact polynomials.comm_ring with *
  have hom : IsRingHom(polynomialCoefficients(I, R), R, P)
    exact polynomialCoefficients.hom with *
  unfold polynomialFromHorner
  exact hornerValue.closed with *

theorem polynomialFromHorner.cons (c : Set) (cs : List(A))
  requires coefficient : c ∈ R
  shows polynomialFromHorner(I, R, j, leading, c :: cs) = P[polynomialConstant(I, R, c) + polynomialVariable(I, R, j) * polynomialFromHorner(I, R, j, leading, cs)]
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have value := polynomialCoefficients.value at I, A, z, c with *
  unfold polynomialFromHorner
  rw [monicValue, value]
  rfl

section Assignments
variable (v : Set)
hypothesis assignment : v : I → R
hypothesis index : j ∈ I

theorem polynomialAt.from_horner (cs : List(A))
  shows polynomialAt(I, R, v)(polynomialFromHorner(I, R, j, leading, cs)) = hornerAt{A}(add, mul, leading, v(j), cs)
proof
  induction cs
  | List.nil =>
    rw [polynomialFromHorner.nil, hornerAt.nil]
    exact polynomialAt.constant with *
  | List.cons(c, tail) using ih =>
    have coefficient : c ∈ R by assumption
    have ordinary := IsCommRing.ring with ring
    have zeroIn := IsRing.zero_in_carrier with ordinary
    have monoid := IsRing.multiplicative with ordinary
    have oneIn := IsMonoid.unit_in_carrier with monoid
    have source : IsCommRing(P)
      exact polynomials.comm_ring with *
    have polynomialRing := IsCommRing.ring with source
    have constant := polynomialConstant.member at I, A, z, c with *
    have variable := polynomialVariable.member at I, A, z, one, j with *
    have tailMember : polynomialFromHorner(I, R, j, leading, tail) ∈ P
      exact polynomialFromHorner.member with *
    have product := IsRing.mul_closed with polynomialRing, variable, tailMember
    have evaluation : IsRingHom(polynomialAt(I, R, v), P, R)
      exact polynomialAt.hom with *
    have sumValue := IsRingHom.add with evaluation, constant, product
    have productValue := IsRingHom.mul with evaluation, variable, tailMember
    have constantValue := polynomialAt.constant with coefficient
    have variableValue := polynomialAt.variable with *
    rw [polynomialFromHorner.cons, hornerAt.cons]
    cc

end Assignments
end Rings

section Fields
variable (I A add z neg mul one j leading : Set)
notation ring R := (A, add, z, neg, mul, one)
notation ring P := R[I]
hypothesis field : IsField(R)
hypothesis initial : leading ∈ R
hypothesis nonzero : leading ≠ R[0]
hypothesis infinite : ¬Finite(R)
hypothesis index : j ∈ I

theorem polynomialFromHorner.nonvanishing (cs : List(A))
  shows ∃ v, FunctionBetween(v, I, R) ∧ polynomialAt(I, R, v)(polynomialFromHorner(I, R, j, leading, cs)) ≠ R[0]
proof
  have point : ∃ x ∈ R, hornerAt{A}(add, mul, leading, x, cs) ≠ R[0]
    exact hornerAt.exists_nonzero with *
  obtain ⟨x, element, value⟩ := point
  have ring := IsField.comm_ring with field
  have assignment := constantFunction.function at I, A, x with element
  have coordinate := constantFunction.apply at I, A, j, x with *
  have evaluation := polynomialAt.from_horner at I, A, add, z, neg, mul, one, j, leading, constantFunction(I, A, x), cs with *
  refine ⟨constantFunction(I, A, x), assignment, ?_⟩
  rwa [evaluation, coordinate]

theorem polynomialFromHorner.nonzero (cs : List(A))
  shows polynomialFromHorner(I, R, j, leading, cs) ≠ P[0]
proof
  have ring := IsField.comm_ring with field
  have point : ∃ v, FunctionBetween(v, I, R) ∧ polynomialAt(I, R, v)(polynomialFromHorner(I, R, j, leading, cs)) ≠ R[0]
    exact polynomialFromHorner.nonvanishing with *
  obtain ⟨v, assignment, nonvanishing⟩ := point
  have evaluation : IsRingHom(polynomialAt(I, R, v), P, R)
    exact polynomialAt.hom with *
  have zeroValue := IsRingHom.zero with evaluation
  intro equal
  apply nonvanishing
  rwa equal

end Fields