0 | ||| Properties of Data.Vect.index
 1 | module Data.Vect.Properties.Index
 2 |
 3 | import Data.Vect.Properties.Tabulate
 4 |
 5 | import Data.Vect
 6 | import Data.Vect.Elem
 7 | import Data.Fin
 8 |
 9 | import Syntax.PreorderReasoning
10 |
11 | ||| Recall an element by its position, as we may not have the element
12 | ||| at runtime
13 | public export
14 | recallElem : {xs : Vect n a} -> x `Elem` xs -> a
15 | recallElem {xs = x :: _ }  Here         = x
16 | recallElem {xs = _ :: xs} (There later) = recallElem later
17 |
18 | ||| Recalling by a position of `x` does yield `x`
19 | export
20 | recallElemSpec : (pos : x `Elem` xs) -> recallElem pos = x
21 | recallElemSpec  Here         = Refl
22 | recallElemSpec (There later) = recallElemSpec later
23 |
24 | ||| `index i : Vect n a -> a` is a natural transformation
25 | export
26 | indexNaturality : (i : Fin n) -> (f : a -> b) -> (xs : Vect n a)
27 |   -> index i (map f xs) = f (index i xs)
28 | indexNaturality  FZ    f (x :: xs) = Refl
29 | indexNaturality (FS x) f (_ :: xs)  = indexNaturality x f xs
30 |
31 | ||| Replication tabulates the constant function
32 | export
33 | indexReplicate : (i : Fin n) -> (x : a)
34 |   -> index i (replicate n x) = x
35 | indexReplicate  FZ    x = Refl
36 | indexReplicate (FS i) x = indexReplicate i x
37 |
38 | ||| `range` tabulates the identity function (by definition)
39 | export
40 | indexRange : (i : Fin n) -> index i (range {len = n}) === i
41 | indexRange i = irrelevantEq $ indexTabulate id i
42 |
43 | ||| Inductive step auxiliary lemma for indexTranspose
44 | indexZipWith_Cons : (i : Fin n) -> (xs : Vect n a) -> (xss : Vect n (Vect m a))
45 |   -> index i (zipWith (::) xs xss)
46 |   = (index i xs)       :: (index i xss)
47 | indexZipWith_Cons  FZ    (x :: _ ) (xs:: _  ) = Refl
48 | indexZipWith_Cons (FS i) (_ :: xs) (_ :: xss) = indexZipWith_Cons i xs xss
49 |
50 | ||| The `i`-th vector in a transposed matrix is the vector of `i`-th components
51 | export
52 | indexTranspose : (xss : Vect m (Vect n a)) -> (i : Fin n)
53 |   -> index i (transpose xss) = map (index i) xss
54 | indexTranspose     []      i = indexReplicate i []
55 | indexTranspose (xs :: xss) i = Calc $
56 |   |~ index i (transpose (xs :: xss))
57 |   ~~ index i (zipWith (::) xs (transpose xss))  ...(Refl)
58 |   ~~ index i xs :: index i (transpose xss)      ...(indexZipWith_Cons i xs (transpose xss))
59 |   ~~ index i xs :: map (index i) xss            ...(cong (index i xs ::)
60 |                                                          $ indexTranspose xss i)
61 |