0 | ||| Tabulation gives a bijection between functions `f : Fin n -> a`
 1 | ||| (up to extensional equality) and vectors `tabulate f : Vect n a`.
 2 | module Data.Vect.Properties.Tabulate
 3 |
 4 | import Data.Vect
 5 | import Data.Fin
 6 |
 7 | ||| Vectors are uniquely determined by their elements
 8 | export
 9 | vectorExtensionality
10 |   : (xs, ys : Vect n a) -> (ext : (i : Fin n) -> index i xs = index i ys)
11 |  -> xs = ys
12 | vectorExtensionality    []        []     ext = Refl
13 | vectorExtensionality (x :: xs) (y :: ys) ext =
14 |   cong2 (::)
15 |         (ext FZ)
16 |         (vectorExtensionality xs ys (\i => ext (FS i)))
17 |
18 | ||| Extensionally equivalent functions tabulate to the same vector
19 | export
20 | tabulateExtensional
21 |   : {n : Nat} -> (f, g : Fin n -> a) -> (ext : (i : Fin n) -> f i = g i)
22 |  -> tabulate f = tabulate g
23 | tabulateExtensional {n = 0  } f g ext = Refl
24 | tabulateExtensional {n = S n} f g ext =
25 |   cong2 (::) (ext FZ) (tabulateExtensional (f . FS) (g . FS) (\ i => ext $ FS i))
26 |
27 | ||| Taking an index amounts to applying the tabulated function
28 | export
29 | indexTabulate : {n : Nat} -> (f : Fin n -> a) -> (i : Fin n) -> index i (tabulate f) = f i
30 | indexTabulate f  FZ    = Refl
31 | indexTabulate f (FS i) = indexTabulate (f . FS) i
32 |
33 | ||| The empty vector represents the unique function `Fin 0 -> a`
34 | export
35 | emptyInitial : (v : Vect 0 a) -> v = []
36 | emptyInitial [] = Refl
37 |