Grace/Cumulus/Algebra/Polynomial/MonicVanishing.g17

Open in Workbench Download source

Imports

Horner · Cardinal.ListSupport

Declarations

Source

1-- Explicit monic polynomials vanishing on finite lists, without Choice.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.MonicVanishing8import Horner9import Cardinal.ListSupport1011-- If cs represents the monic polynomial P, this list represents carry+(X-a)P.12def hornerLinearProduct {A : Set} (add neg mul a carry : Set) (cs : List(A)) → Set13  | add, neg, mul, a, carry, List.nil => [call2(add, carry, neg(a))]14  | add, neg, mul, a, carry, List.cons(c, tail) => call2(add, carry, neg(call2(mul, a, c))) :: hornerLinearProduct(add, neg, mul, a, c, tail)15  descends cs1617section Rings18variable (A add zero neg mul one a : Set)19notation ring R := (A, add, zero, neg, mul, one)20hypothesis ring : IsCommRing(R)21hypothesis center : a ∈ R2223theorem hornerLinearProduct.closed (carry : Set) (cs : List(A))24  requires constant : carry ∈ R25  shows List(A, hornerLinearProduct{A}(add, neg, mul, a, carry, cs))26proof27  induction cs generalizing carry28  | List.nil =>29    intros carry constant30    have ordinary := IsCommRing.ring with ring31    have negative := IsRing.neg_closed with ordinary, center32    have head := IsRing.add_closed with ordinary, constant, negative33    rw hornerLinearProduct34    typecheck35  | List.cons(c, tail) using ih =>36    intros carry constant37    have ordinary := IsCommRing.ring with ring38    have coefficient : c ∈ R by assumption39    have rest := ih with c, coefficient40    have product := IsRing.mul_closed with ordinary, center, coefficient41    have negative := IsRing.neg_closed with ordinary, product42    have head := IsRing.add_closed with ordinary, constant, negative43    rw hornerLinearProduct44    typecheck4546theorem hornerLinearProduct.value (x carry : Set) (cs : List(A))47  requires element : x ∈ R48  requires constant : carry ∈ R49  shows hornerAt{A}(add, mul, one, x, hornerLinearProduct{A}(add, neg, mul, a, carry, cs)) = R[carry + (x - a) * hornerAt{A}(add, mul, one, x, cs)]50proof51  induction cs generalizing carry52  | List.nil =>53    intros carry constant54    have ordinary := IsCommRing.ring with ring55    have negative := IsRing.neg_closed with ordinary, center56    have coefficient := IsRing.add_closed with ordinary, constant, negative57    have empty : List(A, []) by typecheck58    rw [hornerLinearProduct, hornerAt.cons, hornerAt.nil]59    ring60  | List.cons(c, tail) using ih =>61    intros carry constant62    have ordinary := IsCommRing.ring with ring63    have coefficient : c ∈ R by assumption64    have product := IsRing.mul_closed with ordinary, center, coefficient65    have negative := IsRing.neg_closed with ordinary, product66    have productCoefficient := IsRing.add_closed with ordinary, constant,67      negative68    have multiplicative := IsRing.multiplicative with ordinary69    have unitIn := IsMonoid.unit_in_carrier with multiplicative70    have rest := hornerLinearProduct.closed at A, add, zero, neg, mul, one, a, c, tail with *71    have tailValue := hornerAt.closed at A, add, zero, neg, mul, one, one, x, tail with *72    have previous := ih with c, coefficient73    have outer := hornerAt.cons at A, add, mul, one, x, R[carry - a * c], hornerLinearProduct{A}(add, neg, mul, a, c, tail) with *74    have original := hornerAt.cons at A, add, mul, one, x, c, tail with *75    rw [hornerLinearProduct, outer, original, previous]76    ring7778end Rings7980section FiniteSets81variable (A add zero neg mul one : Set)82notation ring R := (A, add, zero, neg, mul, one)83hypothesis ring : IsCommRing(R)8485-- Starting with X guarantees positive degree, even for an empty covering list.86theorem hornerAt.monic_vanishing_on_list (xs : List(A))87  shows ∃ c ∈ R, ∃ cs, List(A, cs) ∧ (∀ x ∈ R, x ∈ listSupport{A}(xs) → hornerAt{A}(add, mul, one, x, c :: cs) = R[0])88proof89  induction xs90  | List.nil =>91    have ordinary := IsCommRing.ring with ring92    have zeroIn := IsRing.zero_in_carrier with ordinary93    have empty : List(A, []) by typecheck94    refine ⟨zero, zeroIn, [], empty, ?_⟩95    intros x element impossible96    rw listSupport at impossible97    exfalso98    exact set.empty with impossible99  | List.cons(a, tail) using ih =>100    have ordinary := IsCommRing.ring with ring101    have center : a ∈ R by assumption102    obtain ⟨c, coefficient, cs, list, vanishes⟩ := ih103    have zeroIn := IsRing.zero_in_carrier with ordinary104    have productCoefficient := IsRing.mul_closed with ordinary, center, coefficient105    have newCoefficient := IsRing.neg_closed with ordinary, productCoefficient106    have newList := hornerLinearProduct.closed at A, add, zero, neg, mul, one, a, c, cs with *107    refine ⟨R[-(a * c)], newCoefficient, hornerLinearProduct{A}(add, neg, mul, a, c, cs), newList, ?_⟩108    intros x element member109    have multiplicative := IsRing.multiplicative with ordinary110    have unitIn := IsMonoid.unit_in_carrier with multiplicative111    have value := hornerAt.closed at A, add, zero, neg, mul, one, one, x, c :: cs with *112    have product := hornerLinearProduct.value at A, add, zero, neg, mul, one, a, x, zero, c :: cs with *113    rw hornerLinearProduct at product114    have head : R[0 - a * c] = R[-(a * c)] by ring115    rw head at product116    rw product117    rw listSupport at member118    have alternatives := insert.membership.forward with member119    cases alternatives with same | previous120    . rw same at value121      rw same122      ring123    . have old := vanishes with x, element, previous124      rw old125      ring126127end FiniteSets128