-- Horner evaluation commutes with a ring homomorphism, coefficient by coefficient.
-- 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.HornerHom
import Horner
import CoefficientLists

section Homomorphisms
variable (A add zero neg mul one B plus z minus times unit h leading x : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring S := (B, plus, z, minus, times, unit)
hypothesis ring : IsCommRing(R)
hypothesis hom : IsRingHom(h, R, S)
hypothesis initial : leading ∈ R
hypothesis element : x ∈ R

theorem hornerAt.map (cs : List(A))
  shows h(hornerAt{A}(add, mul, leading, x, cs)) = hornerAt{B}(plus, times, h(leading), h(x), listMap{A}(h, cs))
proof
  induction cs
  | List.nil =>
    rw [listMap, hornerAt.nil, hornerAt.nil]
    rfl
  | List.cons(c, tail) using ih =>
    have coefficient : c ∈ R by assumption
    have function := IsRingHom.function with hom
    have image := IsRingHom.closed with hom, coefficient
    have value := hornerAt.closed at A, add, zero, neg, mul, one, leading, x, tail with *
    have ordinary := IsCommRing.ring with ring
    have product := IsRing.mul_closed with ordinary, element, value
    have sumMap := IsRingHom.add with hom, coefficient, product
    have productMap := IsRingHom.mul with hom, element, value
    have source := hornerAt.cons at A, add, mul, leading, x, c, tail with *
    have target := hornerAt.cons at B, plus, times, h(leading), h(x), h(c), listMap{A}(h, tail) with *
    rw [listMap, source, target]
    cc

end Homomorphisms
theorem hornerValue.cons (A f plus times leading x c : Set) (cs : List(A))
  requires coefficient : c ∈ A
  shows monicValue{A}(f, plus, times, leading, x, c :: cs) = plus(f(c), times(x, monicValue{A}(f, plus, times, leading, x, cs)))
proof
  rw monicValue
  rfl

section Rings
variable (A add zero neg mul one B plus z minus times unit f leading a : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring S := (B, plus, z, minus, times, unit)
hypothesis source : IsCommRing(R)
hypothesis target : IsCommRing(S)
hypothesis hom : IsRingHom(f, R, S)
hypothesis initial : leading ∈ R
hypothesis center : a ∈ R

theorem hornerAt.map_cons (c : Set) (cs : List(A))
  requires coefficient : c ∈ R
  shows f(hornerAt{A}(add, mul, leading, a, c :: cs)) = S[f(c) + f(a) * f(hornerAt{A}(add, mul, leading, a, cs))]
proof
  have ordinary := IsCommRing.ring with source
  have value := hornerAt.closed at A, add, zero, neg, mul, one, leading, a, cs with *
  have product := IsRing.mul_closed with ordinary, center, value
  have mappedProduct := IsRingHom.mul with hom, center, value
  have mappedSum := IsRingHom.add with hom, coefficient, product
  rw [hornerAt.cons, mappedSum, mappedProduct]
  rfl

-- Evaluation at an arbitrary extension element; no injectivity is required.
theorem hornerValue.synthetic_division (x c : Set) (cs : List(A))
  requires element : x ∈ S
  requires coefficient : c ∈ R
  shows monicValue{A}(f, plus, times, f(leading), x, c :: cs) = S[f(hornerAt{A}(add, mul, leading, a, c :: cs)) + (x - f(a)) * monicValue{A}(f, plus, times, f(leading), x, hornerQuotient{A}(add, mul, leading, a, cs))]
proof
  induction cs generalizing c
  | List.nil =>
    intros c coefficient
    have imageC := IsRingHom.closed with hom, coefficient
    have imageA := IsRingHom.closed with hom, center
    have imageLeading := IsRingHom.closed with hom, initial
    have mapped := hornerAt.map_cons at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, leading, a, c, [] with *
    rw [mapped, hornerAt.nil, hornerQuotient, monicValue, monicValue, monicValue]
    ring
  | List.cons(d, tail) using ih =>
    intros c coefficient
    have dIn : d ∈ R by assumption
    have imageC := IsRingHom.closed with hom, coefficient
    have imageA := IsRingHom.closed with hom, center
    have imageLeading := IsRingHom.closed with hom, initial
    have baseValue := hornerAt.closed at A, add, zero, neg, mul, one, leading, a, d :: tail with *
    have imageValue := IsRingHom.closed with hom, baseValue
    have quotient := hornerQuotient.closed at A, add, zero, neg, mul, one, leading, a, tail with *
    have valueQ := hornerValue.closed at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, f(leading), hornerQuotient{A}(add, mul, leading, a, tail) with *
    have previous := ih with d, dIn
    have mapped := hornerAt.map_cons at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, leading, a, c, d :: tail with *
    have outer := hornerValue.cons at A, f, plus, times, f(leading), x, c, d :: tail with *
    have quotientValue := hornerValue.cons at A, f, plus, times, f(leading), x, hornerAt{A}(add, mul, leading, a, d :: tail), hornerQuotient{A}(add, mul, leading, a, tail) with *
    rw [mapped, hornerQuotient, outer, quotientValue, previous]
    ring

end Rings