Grace/Cumulus/List/Sequence.g17

Imports

Declarations

coefficientWindow.closed_below theorem derivation
coefficientWindow.length_below theorem derivation
coefficientWindow.coefficient_below theorem derivation
List.of_function theorem derivation
Source

1-- Lists as finite sequences: a function on a natural number n is the2-- entry map of a list of length n, read through the coefficient window3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.List.Sequence9import Algebra.IndexedLists1011-- The window laws need the values only at the positions read.12theorem coefficientWindow.closed_below (A f : Set, start n : Nat)13  requires values : ∀ k, Nat(k) → k < n → f(start + k) ∈ A14  shows List(A, coefficientWindow(f, start, n))15proof16  induction n generalizing start17  | zero =>18    intros start startNat values19    rw coefficientWindow20    typecheck21  | succ(k) using ih =>22    intros start startNat values23    have zeroNat : Nat(0) by typecheck24    have below : 0 < succ(k) by arith25    have head := values with 0, zeroNat, below26    rw add.right_unit at head27    have shifted : ∀ j, Nat(j) → j < k → f(succ(start) + j) ∈ A28      intros j jNat bound29      have successorNat : Nat(succ(j)) by typecheck30      have bound2 : succ(j) < succ(k) by arith31      have value := values with succ(j), successorNat, bound232      have shift : succ(start) + j = start + succ(j) by simp [add, add.succ_right]33      rw shift34      exact value35    have tail := ih with succ(start), shifted36    rw coefficientWindow37    typecheck3839theorem coefficientWindow.length_below (A f : Set, start n : Nat)40  requires values : ∀ k, Nat(k) → k < n → f(start + k) ∈ A41  shows length{A}(coefficientWindow(f, start, n)) = n42proof43  induction n generalizing start44  | zero =>45    intros start startNat values46    rw [coefficientWindow, length.nil]47    rfl48  | succ(k) using ih =>49    intros start startNat values50    have zeroNat : Nat(0) by typecheck51    have below : 0 < succ(k) by arith52    have head := values with 0, zeroNat, below53    rw add.right_unit at head54    have shifted : ∀ j, Nat(j) → j < k → f(succ(start) + j) ∈ A55      intros j jNat bound56      have successorNat : Nat(succ(j)) by typecheck57      have bound2 : succ(j) < succ(k) by arith58      have value := values with succ(j), successorNat, bound259      have shift : succ(start) + j = start + succ(j) by simp [add, add.succ_right]60      rw shift61      exact value62    have tail := coefficientWindow.closed_below at A, f, succ(start), k with shifted63    have length := ih with succ(start), shifted64    rw [coefficientWindow, length.cons, length]65    rfl6667theorem coefficientWindow.coefficient_below (A z f : Set, start n k : Nat)68  requires values : ∀ j, Nat(j) → j < n → f(start + j) ∈ A69  requires bound : k < n70  shows listCoefficient{A}(z, coefficientWindow(f, start, n), k) = f(start + k)71proof72  induction n generalizing start k73  | zero =>74    intros start k startNat kNat values bound75    exfalso76    arith77  | succ(t) using ih =>78    intros start k startNat kNat values bound79    have zeroNat : Nat(0) by typecheck80    have below : 0 < succ(t) by arith81    have head := values with 0, zeroNat, below82    rw add.right_unit at head83    have shifted : ∀ j, Nat(j) → j < t → f(succ(start) + j) ∈ A84      intros j jNat jBound85      have successorNat : Nat(succ(j)) by typecheck86      have bound2 : succ(j) < succ(t) by arith87      have value := values with succ(j), successorNat, bound288      have shift : succ(start) + j = start + succ(j) by simp [add, add.succ_right]89      rw shift90      exact value91    have tail := coefficientWindow.closed_below at A, f, succ(start), t with shifted92    have shape := natural.zero_or_successor at k with *93    cases shape with zero | successor94    . rw [zero, coefficientWindow, listCoefficient.zero, add.right_unit]95      rfl96    . obtain ⟨r, rNat, equal⟩ := successor97      rw equal at bound98      have smaller : r < t by arith99      have result := ih with succ(start), r, rNat, shifted, smaller100      have shift : succ(start) + r = start + succ(r) by simp [add, add.succ_right]101      rw [equal, coefficientWindow, listCoefficient.succ, result, shift]102      rfl103104-- Every function on a natural number n into A is the entry map of a list105-- of length n.106theorem List.of_function (A f z : Set, n : Nat)107  requires function : f : n → A108  shows ∃ xs, List(A, xs) ∧ length{A}(xs) = n ∧109    (∀ k, Nat(k) → k < n → listCoefficient{A}(z, xs, k) = f(k))110proof111  have values : ∀ k, Nat(k) → k < n → f(0 + k) ∈ A112    intros k kNat bound113    have member := membership.of_Less with kNat, bound114    have shift : 0 + k = k115      rw add.commutative116      exact add.right_unit117    rw shift118    exact FunctionBetween.apply_closed with function, member119  witness coefficientWindow(f, 0, n)120  have closed := coefficientWindow.closed_below with values121  have length := coefficientWindow.length_below with values122  refine ⟨closed, length, ?_⟩123  intros k kNat bound124  have entry := coefficientWindow.coefficient_below at A, z, f, 0, n, k with values, bound125  have shift : 0 + k = k126    rw add.commutative127    exact add.right_unit128  rwa shift at entry129