Grace/Cumulus/Algebra/Polynomial/HornerNormalization.g17

Open in Workbench Download source

Imports

HornerRoots · CoefficientLists

Declarations

Source

1-- Removing trailing zeros from finite Horner coefficient lists (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Polynomial.HornerNormalization8import HornerRoots9import CoefficientLists1011section Rings12variable (A add z neg mul one : Set)13notation ring R := (A, add, z, neg, mul, one)14hypothesis ring : IsCommRing(R)1516theorem hornerAt.zero_coefficients (cs : List(A))17  requires coefficients : ∀ n, Nat(n) → listCoefficient{A}(z, cs, n) = z18  shows ∀ x ∈ R, hornerAt{A}(add, mul, z, x, cs) = z19proof20  induction cs21  | List.nil =>22    intros coefficients x element23    exact hornerAt.nil with *24  | List.cons(c, tail) using ih =>25    intros coefficients x element26    have coefficient : c ∈ R by assumption27    have head := coefficients with (0:Nat), Naturals.constructor.zero28    rw listCoefficient.zero at head29    have rest : ∀ n, Nat(n) → listCoefficient{A}(z, tail, n) = z30      intros n natural31      have value := coefficients with succ(n)32      rwa listCoefficient.succ at value33    have tailZero := ih with rest, x, element34    rw [hornerAt.cons, tailZero, head]35    ring3637theorem hornerAt.normalize (cs : List(A))38  requires nonzero : ∃ n, Nat(n) ∧ listCoefficient{A}(z, cs, n) ≠ z39  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)))40proof41  induction cs42  | List.nil =>43    intro nonzero44    obtain ⟨n, natural, different⟩ := nonzero45    have value := listCoefficient.nil at A, z, n with *46    exfalso47    exact different with value48  | List.cons(c, tail) using ih =>49    intro nonzero50    have coefficient : c ∈ R by assumption51    have alternatives : (∃ n, Nat(n) ∧ listCoefficient{A}(z, tail, n) ≠ z) ∨ ¬(∃ n, Nat(n) ∧ listCoefficient{A}(z, tail, n) ≠ z)52      tauto53    cases alternatives with tailNonzero | tailZero54    . obtain ⟨leading, initial, different, lower, list, equal⟩ := ih with tailNonzero55      have consList : List(A, c :: lower) by typecheck56      refine ⟨leading, initial, different, c :: lower, consList, ?_⟩57      intros x element58      have value := equal with x, element59      rw [hornerAt.cons, hornerAt.cons, value]60      rfl61    . have zeros : ∀ n, Nat(n) → listCoefficient{A}(z, tail, n) = z62        intros n natural63        by_contra different64        apply tailZero65        refine ⟨n, natural, different⟩66      have different : c ≠ z67        intro headZero68        obtain ⟨n, natural, value⟩ := nonzero69        have cases := natural.zero_or_successor with natural70        cases cases with zero | successor71        . rw [zero, listCoefficient.zero] at value72          exact value with headZero73        . obtain ⟨k, kNat, shape⟩ := successor74          rw [shape, listCoefficient.succ] at value75          have tailValue := zeros with k, kNat76          exact value with tailValue77      have empty : List(A, []) by typecheck78      refine ⟨c, coefficient, different, [], empty, ?_⟩79      intros x element80      have vanishes := hornerAt.zero_coefficients with *81      have tailValue := vanishes with x, element82      rw [hornerAt.cons, tailValue, hornerAt.nil]83      ring8485end Rings86section Fields87variable (A add z neg mul one : Set)88notation ring R := (A, add, z, neg, mul, one)89hypothesis field : IsField(R)9091theorem hornerRoots.finite_of_coefficient (cs : List(A))92  requires nonzero : ∃ n, Nat(n) ∧ listCoefficient{A}(z, cs, n) ≠ z93  shows Finite(hornerRoots{A}(add, z, mul, z, cs))94proof95  have ring := IsField.comm_ring with field96  obtain ⟨leading, initial, different, lower, list, equal⟩ := hornerAt.normalize at A, add, z, neg, mul, one, cs with *97  have finite := hornerRoots.finite at A, add, z, neg, mul, one, leading, lower with *98  have same : hornerRoots{A}(add, z, mul, z, cs) = hornerRoots{A}(add, z, mul, leading, lower)99    ext x100    constructor101    . intro member102      obtain ⟨element, root⟩ := hornerRoots.membership.forward at103        A, add, z, mul, z, cs, x with *104      have value := equal with x, element105      apply hornerRoots.membership.backward106      refine ⟨element, ?_⟩107      cc108    . intro member109      obtain ⟨element, root⟩ := hornerRoots.membership.forward at110        A, add, z, mul, leading, lower, x with *111      have value := equal with x, element112      apply hornerRoots.membership.backward113      refine ⟨element, ?_⟩114      cc115  rwa same116117theorem hornerAt.exists_nonzero_of_coefficient (cs : List(A))118  requires infinite : ¬Finite(R)119  requires nonzero : ∃ n, Nat(n) ∧ listCoefficient{A}(z, cs, n) ≠ z120  shows ∃ x ∈ R, hornerAt{A}(add, mul, z, x, cs) ≠ z121proof122  have ring := IsField.comm_ring with field123  obtain ⟨leading, initial, different, lower, list, equal⟩ := hornerAt.normalize at A, add, z, neg, mul, one, cs with *124  obtain ⟨x, element, value⟩ := hornerAt.exists_nonzero at A, add, z, neg, mul, one, leading, lower with *125  have same := equal with x, element126  refine ⟨x, element, ?_⟩127  rwa same128129theorem hornerAt.exists_nonzero_avoiding_of_coefficient (F : Set) (cs : List(A))130  requires infinite : ¬Finite(R)131  requires excluded : Finite(F)132  requires nonzero : ∃ n, Nat(n) ∧ listCoefficient{A}(z, cs, n) ≠ z133  shows ∃ x ∈ R, ¬(x ∈ F) ∧ hornerAt{A}(add, mul, z, x, cs) ≠ z134proof135  have ring := IsField.comm_ring with field136  obtain ⟨leading, initial, different, lower, list, equal⟩ := hornerAt.normalize at A, add, z, neg, mul, one, cs with *137  obtain ⟨x, element, fresh, value⟩ := hornerAt.exists_nonzero_avoiding at A, add, z, neg, mul, one, leading, F, lower with *138  have same := equal with x, element139  refine ⟨x, element, fresh, ?_⟩140  rwa same141142end Fields143