-- Constructive translation of coefficient lists, preserving their leading term (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.HornerTranslation
import HornerArithmetic

def hornerTranslate {A : Set} (add mul one leading a : Set) (cs : List(A)) → Set
  | add, mul, one, leading, a, List.nil => []
  | add, mul, one, leading, a, List.cons(c, tail) => hornerAffineProduct{A}(add, mul, leading, a, one, c, hornerTranslate(add, mul, one, leading, a, tail))
  descends cs

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

theorem hornerTranslate.data (cs : List(A))
  shows List(A, hornerTranslate{A}(add, mul, one, leading, a, cs)) ∧ length{A}(hornerTranslate{A}(add, mul, one, leading, a, cs)) = length{A}(cs)
proof
  induction cs
  | List.nil =>
    rw hornerTranslate
    constructor
    . typecheck
    . rfl
  | List.cons(c, tail) using ih =>
    have coefficient : c ∈ R by assumption
    have unit : R[1] ∈ R by typecheck
    have data := hornerAffineProduct.data at A, add, zero, neg, mul, one, leading, a, one, c, hornerTranslate{A}(add, mul, one, leading, a, tail) with *
    rw hornerTranslate
    constructor
    . exact data.left
    . rw [data.right, ih.right, length.cons]
      rfl

theorem hornerTranslate.affine_value (x c : Set) (ds : List(A))
  requires element : x ∈ R
  requires coefficient : c ∈ R
  shows hornerAt{A}(add, mul, leading, x, hornerAffineProduct{A}(add, mul, leading, a, one, c, ds)) = R[c + (a + x) * hornerAt{A}(add, mul, leading, x, ds)]
proof
  have hom := IsRingHom.identity with ring
  have unit : R[1] ∈ R by typecheck
  have terminal : R[1 * leading] = leading by ring
  have leadingValue := identity.apply with initial
  have centerValue := identity.apply with center
  have unitValue := identity.apply with unit
  have coefficientValue := identity.apply with coefficient
  have expansion : monicValue{A}(identity(A), add, mul, identity(A)(R[1 * leading]), x, hornerAffineProduct{A}(add, mul, leading, a, one, c, ds)) = R[identity(A)(c) + (identity(A)(a) + identity(A)(one) * x) * monicValue{A}(identity(A), add, mul, identity(A)(leading), x, ds)]
    exact hornerAffineProduct.map_value with *
  rw [terminal, leadingValue, centerValue, unitValue, coefficientValue] at expansion
  have oneTimes : R[1 * x] = x by ring
  rw oneTimes at expansion
  simp [hornerAt]

theorem hornerTranslate.value (x : Set) (cs : List(A))
  requires element : x ∈ R
  shows hornerAt{A}(add, mul, leading, x, hornerTranslate{A}(add, mul, one, leading, a, cs)) = hornerAt{A}(add, mul, leading, R[a + x], cs)
proof
  induction cs
  | List.nil =>
    rw [hornerTranslate, hornerAt.nil, hornerAt.nil]
    rfl
  | List.cons(c, tail) using ih =>
    have coefficient : c ∈ R by assumption
    have data := hornerTranslate.data at A, add, zero, neg, mul, one, leading, a, tail with *
    have expansion := hornerTranslate.affine_value at A, add, zero, neg, mul, one, leading, a, x, c, hornerTranslate{A}(add, mul, one, leading, a, tail) with *
    rw [hornerTranslate, expansion, ih, hornerAt.cons]
    rfl

theorem hornerAt.at_zero (cs : List(A))
  shows hornerAt{A}(add, mul, leading, zero, cs) = listHeadOr{A}(leading, cs)
proof
  induction cs
  | List.nil =>
    rw [hornerAt.nil, listHeadOr]
    rfl
  | List.cons(c, tail) using ih =>
    have coefficient : c ∈ R by assumption
    have zeroIn : R[0] ∈ R by typecheck
    have rest := hornerAt.closed at A, add, zero, neg, mul, one, leading, zero, tail with *
    rw [hornerAt.cons, listHeadOr]
    ring

theorem hornerTranslate.constant (cs : List(A))
  shows listHeadOr{A}(leading, hornerTranslate{A}(add, mul, one, leading, a, cs)) = hornerAt{A}(add, mul, leading, a, cs)
proof
  have zeroIn : R[0] ∈ R by typecheck
  have data := hornerTranslate.data at A, add, zero, neg, mul, one, leading, a, cs with *
  have translated := hornerTranslate.value at A, add, zero, neg, mul, one, leading, a, zero, cs with *
  have constant := hornerAt.at_zero at A, add, zero, neg, mul, one, leading, a, hornerTranslate{A}(add, mul, one, leading, a, cs) with *
  have centerAtZero : R[a + 0] = a by ring
  rwa [constant, centerAtZero] at translated

end Rings