-- Extract the first nonzero term without choosing a coefficient or a degree.
-- 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.HornerVanishing
import HornerTranslation
import Group.Power

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
hypothesis nonzero : leading ≠ R[0]

-- The remaining Horner polynomial has nonzero constant coefficient. Its
-- degree plus the extracted multiplicity is exactly the original degree.
theorem hornerAt.first_nonzero (cs : List(A))
  shows ∃ n ∈ ℕ, ∃ ds, List(A, ds) ∧ listHeadOr{A}(leading, ds) ≠ R[0] ∧
    length{A}(cs) = Grace.Core.Nat.Rec.add(n, length{A}(ds)) ∧
    (∀ x ∈ R, hornerAt{A}(add, mul, leading, x, cs) = R[monoidPow(R, x, n) * hornerAt{A}(add, mul, leading, x, ds)])
proof
  have ordinary := IsCommRing.ring with ring
  have monoid := IsRing.multiplicative with ordinary
  induction cs
  | List.nil =>
    have zeroNat : (0:N) ∈ ℕ by typecheck
    have empty : List(A, []) by typecheck
    have head : listHeadOr{A}(leading, []) ≠ R[0] by rwa listHeadOr
    refine ⟨(0:N), zeroNat, [], empty, head, ?_⟩
    constructor
    . rw add.left_unit
      rfl
    . intros x member
      rw [monoidPow.zero, hornerAt.nil]
      ring
  | List.cons(c, tail) using ih =>
    have coefficient : c ∈ R by assumption
    have list : List(A, c :: tail) by typecheck
    have comparison : c = R[0] ∨ c ≠ R[0] by tauto
    cases comparison with vanishes | survives
    . obtain ⟨n, nIn, ds, dsList, head, degree, factor⟩ := ih
      have nNat := nat.omega.backward at n with *
      have next : succ(n) ∈ ℕ by typecheck
      refine ⟨succ(n), next, ds, dsList, head, ?_⟩
      constructor
      . rw [length.cons, degree, Grace.Core.Nat.Rec.add]
        rfl
      . intros x member
        have ordinary := IsCommRing.ring with ring
        have monoid := IsRing.multiplicative with ordinary
        have power := monoidPow.closed at A, mul, one, x, n with *
        have rest := hornerAt.closed at A, add, zero, neg, mul, one, leading, x, ds with *
        have decomposition := factor with x, member
        rw [hornerAt.cons, vanishes, decomposition, monoidPow.succ]
        ring
    . have zeroNat : (0:N) ∈ ℕ
        typecheck
      have head : listHeadOr{A}(leading, c :: tail) ≠ R[0] by rwa listHeadOr
      refine ⟨(0:N), zeroNat, c :: tail, list, head, ?_⟩
      constructor
      . rw add.left_unit
        rfl
      . intros x member
        have value := hornerAt.closed at A, add, zero, neg, mul, one, leading, x, c :: tail with *
        rw monoidPow.zero
        ring

end Rings