-- Finite roots and nonvanishing of nonzero-leading Horner polynomials.
-- 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.HornerRoots
import Horner

def hornerRoots {A : Set} (add z mul leading : Set) (cs : List(A)) : Set :=
  {x ∈ A | hornerAt{A}(add, mul, leading, x, cs) = z}

theorem hornerRoots.nil (A add z mul leading : Set)
  requires nonzero : leading ≠ z
  shows hornerRoots{A}(add, z, mul, leading, []) = ∅
proof
  ext x
  have value := hornerAt.nil at A, add, mul, leading, x
  constructor
  . intro member
    have data := hornerRoots.membership.forward with member
    have equal := data.right
    rw value at equal
    exfalso
    exact nonzero with equal
  . intro impossible
    exfalso
    simp

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

theorem hornerRoots.divide (a c : Set) (cs : List(A))
  requires center : a ∈ R
  requires coefficient : c ∈ R
  requires root : hornerAt{A}(add, mul, leading, a, c :: cs) = R[0]
  shows hornerRoots{A}(add, z, mul, leading, c :: cs) ⊆ insert(a, hornerRoots{A}(add, z, mul, leading, hornerQuotient{A}(add, mul, leading, a, cs)))
proof
  have ring := IsField.comm_ring with field
  have ordinary := IsCommRing.ring with ring
  have quotient := hornerQuotient.closed at A, add, z, neg, mul, one, leading, a, cs with *
  have noZero := IsField.no_zero_divisors with field
  intros x hx
  obtain ⟨element, vanishes⟩ := hornerRoots.membership.forward at
    A, add, z, mul, leading, c :: cs, x with *
  have division := hornerAt.synthetic_division at A, add, z, neg, mul, one, leading, a, x, c, cs with *
  have value := hornerAt.closed at A, add, z, neg, mul, one, leading, x, hornerQuotient{A}(add, mul, leading, a, cs) with *
  have negative := IsRing.neg_closed with ordinary, center
  have difference := IsRing.add_closed with ordinary, element, negative
  rw [root, vanishes] at division
  have productZero : R[(x - a) * hornerAt{A}(add, mul, leading, x, hornerQuotient{A}(add, mul, leading, a, cs))] = R[0]
    linear_combination -division
  have alternatives := noZero with R[x - a], difference, hornerAt{A}(add, mul, leading, x, hornerQuotient{A}(add, mul, leading, a, cs)), productZero
  cases alternatives with same | remaining
  . have equal : x = a
      linear_combination same
    rw equal
    exact insert.self
  . have member : x ∈ hornerRoots{A}(add, z, mul, leading, hornerQuotient{A}(add, mul, leading, a, cs))
      apply hornerRoots.membership.backward
      refine ⟨element, remaining⟩
    exact insert.contains with member

hypothesis nonzero : leading ≠ R[0]

theorem hornerRoots.finite_of_length (n : Nat) (cs : List(A))
  requires size : length{A}(cs) = n
  shows Finite(hornerRoots{A}(add, z, mul, leading, cs))
proof
  induction n generalizing cs
  | zero =>
    intros cs list size
    have cases := List.cases with list
    cases cases with empty | cons
    . rw [empty, hornerRoots.nil]
      exact Finite.empty
    . obtain ⟨c, coefficient, tail, tailList, shape⟩ := cons
      rw [shape, length.cons] at size
      have impossible := Naturals.disjoint.zero.succ at length{A}(tail)
      exfalso
      apply impossible
      symm
      exact size
  | succ(k) using ih =>
    intros cs list size
    have cases := List.cases with list
    cases cases with empty | cons
    . rw [empty, hornerRoots.nil]
      exact Finite.empty
    . obtain ⟨c, coefficient, tail, tailList, shape⟩ := cons
      have tailSize : length{A}(tail) = k
        rw [shape, length.cons] at size
        exact Naturals.injective.succ with size
      have alternatives : (∃ a, a ∈ hornerRoots{A}(add, z, mul, leading, cs)) ∨ ¬(∃ a, a ∈ hornerRoots{A}(add, z, mul, leading, cs))
        tauto
      cases alternatives with inhabited | emptyRoots
      . obtain ⟨a, ha⟩ := inhabited
        rw shape at ha
        obtain ⟨center, root⟩ := hornerRoots.membership.forward at
          A, add, z, mul, leading, c :: tail, a with *
        have ring := IsField.comm_ring with field
        have quotient := hornerQuotient.closed at A, add, z, neg, mul, one, leading, a, tail with *
        have quotientLength := hornerQuotient.length at A, add, z, neg, mul, one, leading, a, tail with *
        have quotientSize : length{A}(hornerQuotient{A}(add, mul, leading, a, tail)) = k by cc
        have finite := ih with hornerQuotient{A}(add, mul, leading, a, tail), quotientSize
        have inserted := Finite.insert at hornerRoots{A}(add, z, mul, leading, hornerQuotient{A}(add, mul, leading, a, tail)), a with finite
        have subset := hornerRoots.divide at A, add, z, neg, mul, one, leading, a, c, tail with *
        rw shape
        exact Finite.subset with inserted, subset
      . have empty : hornerRoots{A}(add, z, mul, leading, cs) = ∅
          ext x
          constructor
          . intro member
            exfalso
            apply emptyRoots
            refine ⟨x, member⟩
          . intro impossible
            exfalso
            exact set.empty with impossible
        rw empty
        exact Finite.empty

theorem hornerRoots.finite (cs : List(A))
  shows Finite(hornerRoots{A}(add, z, mul, leading, cs))
proof
  have size : length{A}(cs) = length{A}(cs) by rfl
  exact hornerRoots.finite_of_length with *

theorem hornerAt.exists_nonzero (cs : List(A))
  requires infinite : ¬Finite(R)
  shows ∃ x ∈ R, hornerAt{A}(add, mul, leading, x, cs) ≠ R[0]
proof
  have finite := hornerRoots.finite with *
  by_contra absent
  have equal : hornerRoots{A}(add, z, mul, leading, cs) = R
    ext x
    constructor
    . intro member
      have data := hornerRoots.membership.forward with member
      exact data.left
    . intro member
      apply hornerRoots.membership.backward
      refine ⟨member, ?_⟩
      by_contra value
      apply absent
      refine ⟨x, member, value⟩
  rw equal at finite
  exact infinite with finite

theorem hornerAt.exists_nonzero_avoiding (F : Set) (cs : List(A))
  requires infinite : ¬Finite(R)
  requires excluded : Finite(F)
  shows ∃ x ∈ R, ¬(x ∈ F) ∧ hornerAt{A}(add, mul, leading, x, cs) ≠ R[0]
proof
  have roots := hornerRoots.finite with *
  have finite := Finite.union with excluded, roots
  by_contra absent
  have included : R ⊆ F ∪ hornerRoots{A}(add, z, mul, leading, cs)
    intros x hx
    have alternatives : x ∈ F ∨ ¬(x ∈ F) by tauto
    cases alternatives with forbidden | fresh
    . settle with union2.membership
    . have vanishes : hornerAt{A}(add, mul, leading, x, cs) = R[0]
        by_contra value
        apply absent
        refine ⟨x, hx, fresh, value⟩
      have root : x ∈ hornerRoots{A}(add, z, mul, leading, cs)
        apply hornerRoots.membership.backward
        refine ⟨hx, vanishes⟩
      simp
  have impossible := Finite.subset with finite, included
  exact infinite with impossible

end Fields