-- Removing trailing zeros from finite Horner coefficient lists (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.HornerNormalization
import HornerRoots
import CoefficientLists

section Rings
variable (A add z neg mul one : Set)
notation ring R := (A, add, z, neg, mul, one)
hypothesis ring : IsCommRing(R)

theorem hornerAt.zero_coefficients (cs : List(A))
  requires coefficients : ∀ n, Nat(n) → listCoefficient{A}(z, cs, n) = z
  shows ∀ x ∈ R, hornerAt{A}(add, mul, z, x, cs) = z
proof
  induction cs
  | List.nil =>
    intros coefficients x element
    exact hornerAt.nil with *
  | List.cons(c, tail) using ih =>
    intros coefficients x element
    have coefficient : c ∈ R by assumption
    have head := coefficients with (0:Nat), Naturals.constructor.zero
    rw listCoefficient.zero at head
    have rest : ∀ n, Nat(n) → listCoefficient{A}(z, tail, n) = z
      intros n natural
      have value := coefficients with succ(n)
      rwa listCoefficient.succ at value
    have tailZero := ih with rest, x, element
    rw [hornerAt.cons, tailZero, head]
    ring

theorem hornerAt.normalize (cs : List(A))
  requires nonzero : ∃ n, Nat(n) ∧ listCoefficient{A}(z, cs, n) ≠ z
  shows ∃ leading ∈ R, leading ≠ z ∧ (∃ lower, List(A, lower) ∧ (∀ x ∈ R, hornerAt{A}(add, mul, z, x, cs) = hornerAt{A}(add, mul, leading, x, lower)))
proof
  induction cs
  | List.nil =>
    intro nonzero
    obtain ⟨n, natural, different⟩ := nonzero
    have value := listCoefficient.nil at A, z, n with *
    exfalso
    exact different with value
  | List.cons(c, tail) using ih =>
    intro nonzero
    have coefficient : c ∈ R by assumption
    have alternatives : (∃ n, Nat(n) ∧ listCoefficient{A}(z, tail, n) ≠ z) ∨ ¬(∃ n, Nat(n) ∧ listCoefficient{A}(z, tail, n) ≠ z)
      tauto
    cases alternatives with tailNonzero | tailZero
    . obtain ⟨leading, initial, different, lower, list, equal⟩ := ih with tailNonzero
      have consList : List(A, c :: lower) by typecheck
      refine ⟨leading, initial, different, c :: lower, consList, ?_⟩
      intros x element
      have value := equal with x, element
      rw [hornerAt.cons, hornerAt.cons, value]
      rfl
    . have zeros : ∀ n, Nat(n) → listCoefficient{A}(z, tail, n) = z
        intros n natural
        by_contra different
        apply tailZero
        refine ⟨n, natural, different⟩
      have different : c ≠ z
        intro headZero
        obtain ⟨n, natural, value⟩ := nonzero
        have cases := natural.zero_or_successor with natural
        cases cases with zero | successor
        . rw [zero, listCoefficient.zero] at value
          exact value with headZero
        . obtain ⟨k, kNat, shape⟩ := successor
          rw [shape, listCoefficient.succ] at value
          have tailValue := zeros with k, kNat
          exact value with tailValue
      have empty : List(A, []) by typecheck
      refine ⟨c, coefficient, different, [], empty, ?_⟩
      intros x element
      have vanishes := hornerAt.zero_coefficients with *
      have tailValue := vanishes with x, element
      rw [hornerAt.cons, tailValue, hornerAt.nil]
      ring

end Rings
section Fields
variable (A add z neg mul one : Set)
notation ring R := (A, add, z, neg, mul, one)
hypothesis field : IsField(R)

theorem hornerRoots.finite_of_coefficient (cs : List(A))
  requires nonzero : ∃ n, Nat(n) ∧ listCoefficient{A}(z, cs, n) ≠ z
  shows Finite(hornerRoots{A}(add, z, mul, z, cs))
proof
  have ring := IsField.comm_ring with field
  obtain ⟨leading, initial, different, lower, list, equal⟩ := hornerAt.normalize at A, add, z, neg, mul, one, cs with *
  have finite := hornerRoots.finite at A, add, z, neg, mul, one, leading, lower with *
  have same : hornerRoots{A}(add, z, mul, z, cs) = hornerRoots{A}(add, z, mul, leading, lower)
    ext x
    constructor
    . intro member
      obtain ⟨element, root⟩ := hornerRoots.membership.forward at
        A, add, z, mul, z, cs, x with *
      have value := equal with x, element
      apply hornerRoots.membership.backward
      refine ⟨element, ?_⟩
      cc
    . intro member
      obtain ⟨element, root⟩ := hornerRoots.membership.forward at
        A, add, z, mul, leading, lower, x with *
      have value := equal with x, element
      apply hornerRoots.membership.backward
      refine ⟨element, ?_⟩
      cc
  rwa same

theorem hornerAt.exists_nonzero_of_coefficient (cs : List(A))
  requires infinite : ¬Finite(R)
  requires nonzero : ∃ n, Nat(n) ∧ listCoefficient{A}(z, cs, n) ≠ z
  shows ∃ x ∈ R, hornerAt{A}(add, mul, z, x, cs) ≠ z
proof
  have ring := IsField.comm_ring with field
  obtain ⟨leading, initial, different, lower, list, equal⟩ := hornerAt.normalize at A, add, z, neg, mul, one, cs with *
  obtain ⟨x, element, value⟩ := hornerAt.exists_nonzero at A, add, z, neg, mul, one, leading, lower with *
  have same := equal with x, element
  refine ⟨x, element, ?_⟩
  rwa same

theorem hornerAt.exists_nonzero_avoiding_of_coefficient (F : Set) (cs : List(A))
  requires infinite : ¬Finite(R)
  requires excluded : Finite(F)
  requires nonzero : ∃ n, Nat(n) ∧ listCoefficient{A}(z, cs, n) ≠ z
  shows ∃ x ∈ R, ¬(x ∈ F) ∧ hornerAt{A}(add, mul, z, x, cs) ≠ z
proof
  have ring := IsField.comm_ring with field
  obtain ⟨leading, initial, different, lower, list, equal⟩ := hornerAt.normalize at A, add, z, neg, mul, one, cs with *
  obtain ⟨x, element, fresh, value⟩ := hornerAt.exists_nonzero_avoiding at A, add, z, neg, mul, one, leading, F, lower with *
  have same := equal with x, element
  refine ⟨x, element, fresh, ?_⟩
  rwa same

end Fields