HornerNormalization

Finite roots without a preselected leading coefficient

Open in Workbench View on GitHub

1-- Finite roots without a preselected leading coefficient.2-- Part of the Grace17 examples.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module HornerNormalization8import Grace.Cumulus.Algebra.Polynomial.HornerNormalization910section Fields11variable (A add z neg mul one : Set)12notation ring R := (A, add, z, neg, mul, one)13hypothesis field : IsField(R)1415theorem finite_roots (cs : List(A))16  requires nonzero : ∃ n, Nat(n) ∧ listCoefficient{A}(z, cs, n) ≠ z17  shows Finite(hornerRoots{A}(add, z, mul, z, cs))18proof19  exact hornerRoots.finite_of_coefficient with *2021theorem nonvanishing (cs : List(A))22  requires infinite : ¬Finite(R)23  requires nonzero : ∃ n, Nat(n) ∧ listCoefficient{A}(z, cs, n) ≠ z24  shows ∃ x ∈ R, hornerAt{A}(add, mul, z, x, cs) ≠ z25proof26  exact hornerAt.exists_nonzero_of_coefficient with *2728theorem nonvanishing_away (F : Set) (cs : List(A))29  requires infinite : ¬Finite(R)30  requires excluded : Finite(F)31  requires nonzero : ∃ n, Nat(n) ∧ listCoefficient{A}(z, cs, n) ≠ z32  shows ∃ x ∈ R, ¬(x ∈ F) ∧ hornerAt{A}(add, mul, z, x, cs) ≠ z33proof34  exact hornerAt.exists_nonzero_avoiding_of_coefficient with *3536theorem trailing_zeros (a : Set)37  requires element : a ∈ R38  requires nonzero : a ≠ z39  shows Finite(hornerRoots{A}(add, z, mul, z, [a, z, z]))40proof41  have ring := IsField.comm_ring with field42  have zeroIn : z ∈ R by typecheck43  have list : List(A, [a, z, z]) by typecheck44  have tail : List(A, [z, z]) by typecheck45  have witness : ∃ n, Nat(n) ∧ listCoefficient{A}(z, [a, z, z], n) ≠ z46    refine ⟨(0:Nat), Naturals.constructor.zero, ?_⟩47    rw listCoefficient.zero48    exact nonzero49  exact hornerRoots.finite_of_coefficient with *5051end Fields52