Grace/Cumulus/Algebra/CoefficientLists.g17

Open in Workbench Download source

Imports

Coefficients · Nat.Order

Declarations

Source

1-- Finite windows of coefficient functions and their indexed list values (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.CoefficientLists8import Coefficients9import Nat.Order1011def listHeadOr {A : Set} (z : Set) (xs : List(A)) → Set12  | z, List.nil => z13  | z, List.cons(a, tail) => a1415def listTail {A : Set} (xs : List(A)) → Set16  | List.nil => []17  | List.cons(a, tail) => tail1819def listCoefficient {A : Set} (z : Set) (xs : List(A)) (n : Nat) → Set20  | z, xs, zero => listHeadOr{A}(z, xs)21  | z, xs, succ(k) => listCoefficient{A}(z, listTail{A}(xs), k)22  descends n2324def coefficientWindow (f : Set, start n : Nat) → Set25  | f, start, zero => []26  | f, start, succ(k) => f(start) :: coefficientWindow(f, succ(start), k)27  descends n2829def listMap {A : Set} (f : Set) (xs : List(A)) → Set30  | f, List.nil => []31  | f, List.cons(a, tail) => f(a) :: listMap(f, tail)32  descends xs3334theorem listTail.closed (A : Set) (xs : List(A))35  shows List(A, listTail{A}(xs))36proof37  induction xs38  | List.nil =>39    rw listTail40    typecheck41  | List.cons(a, tail) using ih =>42    rwa listTail4344theorem listCoefficient.nil (A z : Set, n : Nat)45  shows listCoefficient{A}(z, [], n) = z46proof47  induction n48  | zero =>49    rw [listCoefficient, listHeadOr]50    rfl51  | succ(k) using ih =>52    rw [listCoefficient, listTail]53    exact ih5455theorem listCoefficient.zero (A z a : Set) (xs : List(A))56  requires element : a ∈ A57  shows listCoefficient{A}(z, a :: xs, 0) = a58proof59  rw [listCoefficient, listHeadOr]60  rfl6162theorem listCoefficient.succ (A z a : Set) (xs : List(A)) (n : Nat)63  requires element : a ∈ A64  shows listCoefficient{A}(z, a :: xs, succ(n)) = listCoefficient{A}(z, xs, n)65proof66  rw [listCoefficient, listTail]67  rfl6869theorem listMap.closed (A B f : Set) (xs : List(A))70  requires function : f : A → B71  shows List(B, listMap{A}(f, xs))72proof73  induction xs74  | List.nil =>75    rw listMap76    typecheck77  | List.cons(a, tail) using ih =>78    have element : a ∈ A by assumption79    have image := FunctionBetween.apply_closed with function, element80    rw listMap81    typecheck8283theorem listMap.compose (A B C f g : Set) (xs : List(A))84  requires first : f : A → B85  requires second : g : B → C86  shows listMap{B}(g, listMap{A}(f, xs)) = listMap{A}(compose(g, f, A, B, C), xs)87proof88  induction xs89  | List.nil => simp [listMap]90  | List.cons(a, tail) using ih =>91    have member : a ∈ A by assumption92    have image := FunctionBetween.apply_closed with first, member93    have value := compose.apply at g, f, A, B, C, a with *94    simp [listMap, ih, value]9596theorem listMap.length (A B f : Set) (xs : List(A))97  requires function : f : A → B98  shows length{B}(listMap{A}(f, xs)) = length{A}(xs)99proof100  induction xs101  | List.nil =>102    rw [listMap, length.nil, length.nil]103    rfl104  | List.cons(a, tail) using ih =>105    have element : a ∈ A by assumption106    have image := FunctionBetween.apply_closed with function, element107    have mapped := listMap.closed with *108    rw [listMap, length.cons, length.cons, ih]109    rfl110111theorem listCoefficient.map (A B f z : Set) (xs : List(A)) (n : Nat)112  requires function : f : A → B113  requires default : z ∈ A114  shows listCoefficient{B}(f(z), listMap{A}(f, xs), n) = f(listCoefficient{A}(z, xs, n))115proof116  induction xs generalizing n117  | List.nil =>118    intros n natural119    rw [listMap, listCoefficient.nil, listCoefficient.nil]120    rfl121  | List.cons(a, tail) using ih =>122    intros n natural123    have element : a ∈ A by assumption124    have mapped := FunctionBetween.apply_closed with function, element125    have tailList := listMap.closed with *126    have shape := natural.zero_or_successor with *127    cases shape with zero | successor128    . rw [zero, listMap, listCoefficient.zero, listCoefficient.zero]129      rfl130    . obtain ⟨k, kNat, equal⟩ := successor131      rw [equal, listMap, listCoefficient.succ, listCoefficient.succ]132      exact ih with k, kNat133134theorem listMap.congr_coefficients (A z f g : Set) (xs : List(A))135  requires agreement : ∀ n, Nat(n) → f(listCoefficient{A}(z, xs, n)) = g(listCoefficient{A}(z, xs, n))136  shows listMap{A}(f, xs) = listMap{A}(g, xs)137proof138  induction xs139  | List.nil =>140    intro agreement141    rw [listMap, listMap]142    rfl143  | List.cons(a, tail) using ih =>144    intro agreement145    have element : a ∈ A by assumption146    have head := agreement with 0, Naturals.constructor.zero147    rw listCoefficient.zero at head148    have rest : ∀ n, Nat(n) → f(listCoefficient{A}(z, tail, n)) = g(listCoefficient{A}(z, tail, n))149      intros n natural150      have value := agreement with succ(n)151      rwa listCoefficient.succ at value152    have equal := ih with rest153    rw [listMap, listMap]154    cc155156theorem coefficientWindow.closed (A f : Set, start n : Nat)157  requires function : f : ℕ → A158  shows List(A, coefficientWindow(f, start, n))159proof160  induction n generalizing start161  | zero =>162    intros start startNat163    rw coefficientWindow164    typecheck165  | succ(k) using ih =>166    intros start startNat167    have startIn := nat.omega.forward at start with *168    have head := FunctionBetween.apply_closed with function, startIn169    have tail := ih with succ(start)170    rw coefficientWindow171    typecheck172173theorem coefficientWindow.length (A f : Set, start n : Nat)174  requires function : f : ℕ → A175  shows length{A}(coefficientWindow(f, start, n)) = n176proof177  induction n generalizing start178  | zero =>179    intros start startNat180    rw [coefficientWindow, length.nil]181    rfl182  | succ(k) using ih =>183    intros start startNat184    have startIn := nat.omega.forward at start with *185    have head := FunctionBetween.apply_closed with function, startIn186    have tail := coefficientWindow.closed at A, f, succ(start), k with *187    have length := ih with succ(start)188    rw [coefficientWindow, length.cons, length]189    rfl190191theorem coefficientWindow.coefficient (A z f : Set, start n k : Nat)192  requires function : f : ℕ → A193  requires bound : k < n194  shows listCoefficient{A}(z, coefficientWindow(f, start, n), k) = f(start + k)195proof196  induction n generalizing start k197  | zero =>198    intros start k startNat kNat bound199    have impossible : 0 < 0 by arith200    exfalso201    have irreflexive := Less.irreflexive with Naturals.constructor.zero202    exact irreflexive with impossible203  | succ(t) using ih =>204    intros start k startNat kNat bound205    have startIn := nat.omega.forward at start with *206    have head := FunctionBetween.apply_closed with function, startIn207    have tail := coefficientWindow.closed at A, f, succ(start), t with *208    have shape := natural.zero_or_successor at k with *209    cases shape with zero | successor210    . rw [zero, coefficientWindow, listCoefficient.zero, add.right_unit]211      rfl212    . obtain ⟨r, rNat, equal⟩ := successor213      have smaller : r < t by arith214      have result := ih with succ(start), r, rNat, smaller215      have shift : succ(start) + r = start + succ(r) by simp [add, add.succ_right]216      rw [equal, coefficientWindow, listCoefficient.succ, result, shift]217      rfl218219theorem listCoefficient.outside (A z : Set) (xs : List(A)) (n : Nat)220  requires bound : length{A}(xs) ≤ n221  shows listCoefficient{A}(z, xs, n) = z222proof223  induction xs generalizing n224  | List.nil =>225    intros n nNat bound226    exact listCoefficient.nil with *227  | List.cons(a, tail) using ih =>228    intros n nNat bound229    have element : a ∈ A by assumption230    rw length.cons at bound231    have shape := natural.zero_or_successor with *232    cases shape with zero | successor233    . have impossible : 0 < 0234        arith235      exfalso236      have irreflexive := Less.irreflexive with Naturals.constructor.zero237      exact irreflexive with impossible238    . obtain ⟨r, rNat, equal⟩ := successor239      have smaller : length{A}(tail) ≤ r by arith240      have result := ih with r, rNat, smaller241      rwa [equal, listCoefficient.succ]242243-- Every finitely supported natural-indexed function is represented by a finite list.244theorem CoefficientMap.list_representation (A z f : Set)245  requires map : CoefficientMap(f, ℕ, A, z)246  shows ∃ cs, List(A, cs) ∧ (∀ k, Nat(k) → listCoefficient{A}(z, cs, k) = f(k))247proof248  have function := CoefficientMap.function with map249  have finite := CoefficientMap.finite_support with map250  have domain := functionSupport.subset at f, ℕ, z251  obtain ⟨b, bNat, bound⟩ := Finite.naturals_bounded with domain, finite252  have list := coefficientWindow.closed at A, f, 0, succ(b) with *253  refine ⟨coefficientWindow(f, 0, succ(b)), list, ?_⟩254  intros k kNat255  have alternatives : k < succ(b) ∨ ¬(k < succ(b)) by tauto256  cases alternatives with inside | outside257  . have value := coefficientWindow.coefficient at A, z, f, 0, succ(b), k with *258    have equal := add.left_unit at k with *259    rwa equal at value260  . have absent : ¬(k ∈ functionSupport(f, ℕ, z))261      intro supported262      have member := bound with k, supported263      have smaller := Less.of_membership at k, succ(b) with *264      have less := smaller with member265      exact outside with less266    have kIn := nat.omega.forward at k with *267    have vanishes := functionSupport.outside at f, ℕ, z, k with *268    have length := coefficientWindow.length at A, f, 0, succ(b) with *269    have enough : length{A}(coefficientWindow(f, 0, succ(b))) ≤ k270      rw length271      exact LessEqual.of_not_Less with *272    have value := listCoefficient.outside at A, z, coefficientWindow(f, 0, succ(b)), k with *273    cc274