-- One-variable polynomials over a bundled ring in Horner form: the value
-- horner(R, leading, x, cs), the synthetic quotient, the remainder and
-- factor theorems, the polynomial hornerPolynomial(R, I, j, leading, cs) of
-- polynomialRing(R, I) with that value, and over a field the finiteness of
-- the root set rootSet(R, leading, cs); everything here is 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.BundledRoots
import BundledEvaluation
import HornerPolynomial
import FactorTheorem

-- cs lists the lower coefficients and leading is the coefficient of the
-- top power, so horner(R, leading, x, c :: cs) = c + x * horner(…, cs).
def horner (R leading x cs : Set) : Set :=
  hornerAt{R.carrier}(R.add, R.mul, leading, x, cs)
def syntheticQuotient (R leading a cs : Set) : Set :=
  hornerQuotient{R.carrier}(R.add, R.mul, leading, a, cs)
def rootSet (R leading cs : Set) : Set :=
  hornerRoots{R.carrier}(R.add, R.zero, R.mul, leading, cs)
def hornerPolynomial (R I j leading cs : Set) : Set :=
  polynomialFromHorner(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, j,
    leading, cs)

theorem horner.graph (R leading x cs : Set)
  shows horner(R, leading, x, cs) =
    hornerAt{R.carrier}(R.add, R.mul, leading, x, cs)
proof
  simp [horner]

theorem syntheticQuotient.graph (R leading a cs : Set)
  shows syntheticQuotient(R, leading, a, cs) =
    hornerQuotient{R.carrier}(R.add, R.mul, leading, a, cs)
proof
  simp [syntheticQuotient]

theorem rootSet.graph (R leading cs : Set)
  shows rootSet(R, leading, cs) =
    hornerRoots{R.carrier}(R.add, R.zero, R.mul, leading, cs)
proof
  simp [rootSet]

theorem hornerPolynomial.graph (R I j leading cs : Set)
  shows hornerPolynomial(R, I, j, leading, cs) =
    polynomialFromHorner(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, j,
      leading, cs)
proof
  simp [hornerPolynomial]

section Rings
variable (R leading : Set)
hypothesis comm : CommRing(R)
hypothesis initial : leading ∈ R

theorem horner.nil (x : R)
  shows horner(R, leading, x, []) = leading
proof
  rw horner.graph
  exact hornerAt.nil

theorem horner.cons (x c : R) (cs : List(R.carrier))
  shows horner(R, leading, x, c :: cs) = c + x * horner(R, leading, x, cs)
proof
  have cIn : c ∈ R by assumption
  rw [horner.graph, horner.graph]
  exact hornerAt.cons with cIn

instance horner.mem (x : R) (cs : List(R.carrier))
  shows horner(R, leading, x, cs) ∈ R
proof
  have parts := CommRing.parts with comm
  have xIn : x ∈ R by assumption
  rw horner.graph
  exact hornerAt.closed with parts, initial, xIn

theorem syntheticQuotient.list (a : R) (cs : List(R.carrier))
  shows List(R.carrier, syntheticQuotient(R, leading, a, cs))
proof
  have parts := CommRing.parts with comm
  have aIn : a ∈ R by assumption
  rw syntheticQuotient.graph
  exact hornerQuotient.closed with parts, initial, aIn

-- The remainder theorem: dividing by X - a leaves the remainder p(a).
theorem horner.remainder (a x c : R) (cs : List(R.carrier))
  shows horner(R, leading, x, c :: cs) = horner(R, leading, a, c :: cs) +
    (x - a) * horner(R, leading, x, syntheticQuotient(R, leading, a, cs))
proof
  have parts := CommRing.parts with comm
  have aIn : a ∈ R by assumption
  have xIn : x ∈ R by assumption
  have cIn : c ∈ R by assumption
  have engine := remainder.theorem with parts, initial, aIn, xIn, cIn
  have ordinary := CommRing.to_ring with comm
  rw [Ring.sub.value, horner.graph, horner.graph, horner.graph,
    syntheticQuotient.graph]
  exact engine

-- The factor theorem: at a root a, X - a divides p with the synthetic
-- quotient, and conversely such a factorization forces the root.
theorem horner.factor (a x c : R) (cs : List(R.carrier))
  requires root : horner(R, leading, a, c :: cs) = R[0]
  shows horner(R, leading, x, c :: cs) =
    (x - a) * horner(R, leading, x, syntheticQuotient(R, leading, a, cs))
proof
  have parts := CommRing.parts with comm
  have aIn : a ∈ R by assumption
  have xIn : x ∈ R by assumption
  have cIn : c ∈ R by assumption
  rw horner.graph at root
  have engine := factor.theorem with parts, initial, aIn, xIn, cIn, root
  have ordinary := CommRing.to_ring with comm
  rw [Ring.sub.value, horner.graph, horner.graph, syntheticQuotient.graph]
  exact engine

theorem horner.root_of_factor (a c : R) (cs : List(R.carrier))
  requires factor : ∀ x ∈ R, horner(R, leading, x, c :: cs) =
    (x - a) * horner(R, leading, x, syntheticQuotient(R, leading, a, cs))
  shows horner(R, leading, a, c :: cs) = R[0]
proof
  have parts := CommRing.parts with comm
  have ordinary := CommRing.to_ring with comm
  have aIn : a ∈ R by assumption
  have cIn : c ∈ R by assumption
  have engineFactor : ∀ x ∈ R,
      hornerAt{R.carrier}(R.add, R.mul, leading, x, c :: cs) =
      (x + -a) * hornerAt{R.carrier}(R.add, R.mul, leading, x,
        hornerQuotient{R.carrier}(R.add, R.mul, leading, a, cs))
    intros x hx
    have value := factor with x, hx
    rw [Ring.sub.value, horner.graph] at value
    rw [horner.graph, syntheticQuotient.graph] at value
    exact value
  rw horner.graph
  exact factor.root with parts, initial, aIn, cIn, engineFactor

-- The Horner form as an element of the polynomial ring in the variable j.
section Polynomials
variable (I j : Set)

theorem hornerPolynomial.mem (cs : List(R.carrier))
  shows hornerPolynomial(R, I, j, leading, cs) ∈ polynomialRing(R, I)
proof
  have parts := CommRing.parts with comm
  rw [hornerPolynomial.graph, polynomialRing.carrierOf]
  exact polynomialFromHorner.member with parts, initial

theorem hornerPolynomial.cons (c : R) (cs : List(R.carrier))
  shows hornerPolynomial(R, I, j, leading, c :: cs) =
    Ring.add(polynomialRing(R, I))(polynomialConstant(R, I)(c),
      Ring.mul(polynomialRing(R, I))(X(R, I, j),
        hornerPolynomial(R, I, j, leading, cs)))
proof
  have parts := CommRing.parts with comm
  have cIn : c ∈ R by assumption
  rw [hornerPolynomial.graph, hornerPolynomial.graph, polynomialRing.addOf,
    polynomialRing.mulOf, polynomialConstant.apply, X.value]
  exact polynomialFromHorner.cons with parts, initial, cIn

theorem hornerPolynomial.eval (v : Set) (cs : List(R.carrier))
  requires assignment : v : I → R.carrier
  requires index : j ∈ I
  shows evaluationAt(R, I, v)(hornerPolynomial(R, I, j, leading, cs)) =
    horner(R, leading, v(j), cs)
proof
  have parts := CommRing.parts with comm
  rw [hornerPolynomial.graph, evaluationAt.graph, horner.graph]
  exact polynomialAt.from_horner with parts, initial, assignment, index

end Polynomials
end Rings

section Fields
variable (R leading : Set)
hypothesis field : Field(R)
hypothesis initial : leading ∈ R
hypothesis nonzero : leading ≠ R[0]

theorem rootSet.membership (x : Set) (cs : List(R.carrier))
  shows x ∈ rootSet(R, leading, cs) ↔
    x ∈ R ∧ horner(R, leading, x, cs) = R[0]
proof
  rw [rootSet.graph, horner.graph]
  exact hornerRoots.membership

-- A nonzero polynomial over a field has finitely many roots, so over an
-- infinite field it takes a nonzero value.
theorem rootSet.finite (cs : List(R.carrier))
  shows Finite(rootSet(R, leading, cs))
proof
  have isField := Field.parts with field
  rw rootSet.graph
  exact hornerRoots.finite with isField, initial, nonzero

theorem horner.exists_nonzero (cs : List(R.carrier))
  requires infinite : ¬Finite(R)
  shows ∃ x ∈ R, horner(R, leading, x, cs) ≠ R[0]
proof
  have isField := Field.parts with field
  obtain ⟨x, xIn, value⟩ := hornerAt.exists_nonzero with isField, initial,
    nonzero, infinite
  refine ⟨x, xIn, ?_⟩
  rw horner.graph
  exact value

end Fields