-- The remainder and factor theorems: dividing a polynomial by X − a leaves
-- the remainder p(a), and a is a root exactly when X − a divides p
-- 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.FactorTheorem
import Horner

section Rings
variable (A add zero neg mul one leading : Set)
notation ring R := (A, add, zero, neg, mul, one)
hypothesis ring : IsCommRing(R)
hypothesis initial : leading ∈ R

-- The remainder theorem: p(x) = p(a) + (x − a)·q(x) with q the synthetic
-- quotient, so the remainder on division by X − a is p(a).
theorem remainder.theorem (a x c : Set) (cs : List(A))
  requires center : a ∈ R
  requires element : x ∈ R
  requires coefficient : c ∈ R
  shows hornerAt{A}(add, mul, leading, x, c :: cs) = R[hornerAt{A}(add, mul, leading, a, c :: cs) + (x - a) * hornerAt{A}(add, mul, leading, x, hornerQuotient{A}(add, mul, leading, a, cs))]
proof
  exact hornerAt.synthetic_division with *

-- The factor theorem: at a root a, X − a divides p with the synthetic quotient.
theorem factor.theorem (a x c : Set) (cs : List(A))
  requires center : a ∈ R
  requires element : x ∈ R
  requires coefficient : c ∈ R
  requires root : hornerAt{A}(add, mul, leading, a, c :: cs) = R[0]
  shows hornerAt{A}(add, mul, leading, x, c :: cs) = R[(x - a) * hornerAt{A}(add, mul, leading, x, hornerQuotient{A}(add, mul, leading, a, cs))]
proof
  have division := hornerAt.synthetic_division at A, add, zero, neg, mul, one, leading, a, x, c, cs with *
  have quotient := hornerQuotient.closed at A, add, zero, neg, mul, one, leading, a, cs with *
  have quotientValue := hornerAt.closed at A, add, zero, neg, mul, one, leading, x, hornerQuotient{A}(add, mul, leading, a, cs) with *
  rw root at division
  rw division
  ring

-- Conversely, a factor X − a forces a root at a.
theorem factor.root (a c : Set) (cs : List(A))
  requires center : a ∈ R
  requires coefficient : c ∈ R
  requires factor : ∀ x ∈ R, hornerAt{A}(add, mul, leading, x, c :: cs) = R[(x - a) * hornerAt{A}(add, mul, leading, x, hornerQuotient{A}(add, mul, leading, a, cs))]
  shows hornerAt{A}(add, mul, leading, a, c :: cs) = R[0]
proof
  have quotient := hornerQuotient.closed at A, add, zero, neg, mul, one, leading, a, cs with *
  have quotientValue := hornerAt.closed at A, add, zero, neg, mul, one, leading, a, hornerQuotient{A}(add, mul, leading, a, cs) with *
  have atRoot := factor with center
  rw atRoot
  ring

end Rings