-- Synthetic division for ascending coefficient lists over commutative rings.
-- 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.Horner
import Field.Algebraic

-- cs stores the lower coefficients; leading is the coefficient of X^length(cs).
def hornerAt {A : Set} (add mul leading x : Set) (cs : List(A)) : Set :=
  monicValue{A}(identity(A), add, mul, leading, x, cs)

-- For c :: cs, division by X-a has lower coefficients given by this list.
def hornerQuotient {A : Set} (add mul leading a : Set) (cs : List(A)) → Set
  | add, mul, leading, a, List.nil => []
  | add, mul, leading, a, List.cons(c, tail) => hornerAt{A}(add, mul, leading, a, c :: tail) :: hornerQuotient(add, mul, leading, a, tail)
  descends cs

theorem hornerAt.nil (A add mul leading x : Set)
  shows hornerAt{A}(add, mul, leading, x, []) = leading
proof
  unfold hornerAt
  rw monicValue
  rfl

theorem hornerAt.cons (A add mul leading x c : Set) (cs : List(A))
  requires coefficient : c ∈ A
  shows hornerAt{A}(add, mul, leading, x, c :: cs) = call2(add, c, call2(mul, x, hornerAt{A}(add, mul, leading, x, cs)))
proof
  have value := identity.apply with coefficient
  unfold hornerAt
  rw [monicValue, value]
  rfl

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

theorem hornerAt.closed (x : Set) (cs : List(A))
  requires element : x ∈ R
  shows hornerAt{A}(add, mul, leading, x, cs) ∈ R
proof
  have hom := IsRingHom.identity with ring
  unfold hornerAt
  exact hornerValue.closed with *

theorem hornerQuotient.closed (a : Set) (cs : List(A))
  requires center : a ∈ R
  shows List(A, hornerQuotient{A}(add, mul, leading, a, cs))
proof
  induction cs
  | List.nil =>
    rw hornerQuotient
    typecheck
  | List.cons(c, tail) using ih =>
    have coefficient : c ∈ R by assumption
    have value := hornerAt.closed at A, add, zero, neg, mul, one, leading, a, c :: tail with *
    rw hornerQuotient
    typecheck

theorem hornerQuotient.length (a : Set) (cs : List(A))
  requires center : a ∈ R
  shows length{A}(hornerQuotient{A}(add, mul, leading, a, cs)) = length{A}(cs)
proof
  induction cs
  | List.nil =>
    rw hornerQuotient
    rfl
  | List.cons(c, tail) using ih =>
    have coefficient : c ∈ R by assumption
    have value := hornerAt.closed at A, add, zero, neg, mul, one, leading, a, c :: tail with *
    have quotient := hornerQuotient.closed at A, add, zero, neg, mul, one, leading, a, tail with *
    rw [hornerQuotient, length.cons, length.cons, ih]
    rfl

theorem hornerAt.synthetic_division (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
  induction cs generalizing c
  | List.nil =>
    intros c coefficient
    have empty : List(A, []) by typecheck
    rw [hornerQuotient, hornerAt.cons, hornerAt.cons, hornerAt.nil, hornerAt.nil]
    ring
  | List.cons(d, tail) using ih =>
    intros c coefficient
    have dIn : d ∈ R by assumption
    have quotient := hornerQuotient.closed at A, add, zero, neg, mul, one, leading, a, tail with *
    have valueA := hornerAt.closed at A, add, zero, neg, mul, one, leading, a, d :: tail with *
    have valueQ := hornerAt.closed at A, add, zero, neg, mul, one, leading, x, hornerQuotient{A}(add, mul, leading, a, tail) with *
    have previous := ih with d, dIn
    have outerX := hornerAt.cons at A, add, mul, leading, x, c, d :: tail with *
    have outerA := hornerAt.cons at A, add, mul, leading, a, c, d :: tail with *
    have quotientValue := hornerAt.cons at A, add, mul, leading, x, hornerAt{A}(add, mul, leading, a, d :: tail), hornerQuotient{A}(add, mul, leading, a, tail) with *
    rw [outerX, outerA, hornerQuotient, quotientValue, previous]
    ring

end Rings