0 | ||| Properties of Data.Vect.map
 1 | module Data.Vect.Properties.Map
 2 |
 3 | import Data.Vect.Properties.Tabulate
 4 | import Data.Vect.Properties.Index
 5 |
 6 | import Data.Vect
 7 | import Data.Vect.Elem
 8 | import Data.Fin
 9 | import Data.Vect.Extra
10 |
11 | import Syntax.PreorderReasoning
12 |
13 | ||| `map` functoriality: identity preservation
14 | export
15 | mapId : (xs : Vect n a) -> map Prelude.id xs = xs
16 | mapId xs = vectorExtensionality _ _ $ \i => indexNaturality _ _ _
17 |
18 | ||| `mapWtihPos f` represents post-composition the tabulated function `f`
19 | export
20 | indexMapWithPos : (f : Fin n -> a -> b) -> (xs : Vect n a) -> (i : Fin n)
21 |   -> index i (mapWithPos f xs) = f i (index i xs)
22 | indexMapWithPos f (x :: _ )  FZ    = Refl
23 | indexMapWithPos f (_ :: xs) (FS i) = indexMapWithPos _ _ _
24 |
25 | ||| `tabulate : (Fin n ->) -> Vect n` is a natural transformation
26 | export
27 | mapTabulate : (f : a -> b) -> (g : Fin n -> a)
28 |   -> tabulate (f . g) = map f (tabulate g)
29 | mapTabulate f g = irrelevantEq $
30 |   vectorExtensionality _ _ $ \i => Calc $
31 |   |~ index i (tabulate (f . g))
32 |   ~~ f (g i)                      ...(indexTabulate _ _)
33 |   ~~ f (index i $ tabulate g)     ...(cong f (sym $ indexTabulate _ _))
34 |   ~~ index i (map f $ tabulate g) ...(sym $ indexNaturality _ _ _)
35 |
36 | ||| Tabulating with the constant function is replication
37 | export
38 | tabulateConstantly : (x : a) -> Fin.tabulate {len} (const x) === replicate len  x
39 | tabulateConstantly x = irrelevantEq $
40 |   vectorExtensionality _ _ $ \i => Calc $
41 |   |~ index i (Fin.tabulate (const x))
42 |   ~~ x ...(indexTabulate _ _)
43 |   ~~ index i (replicate _ x) ...(sym $ indexReplicate _ _)
44 |
45 | ||| It's enough that two functions agree on the elements of a vector for the maps to agree
46 | export
47 | mapRestrictedExtensional : (f, g : a -> b) -> (xs : Vect n a)
48 |   -> (prf : (i : Fin n) -> f (index i xs) = g (index i xs))
49 |   -> map f xs = map g xs
50 | mapRestrictedExtensional f g xs prf = vectorExtensionality _ _ $ \i => Calc $
51 |   |~ index i (map f xs)
52 |   ~~ f (index i xs)     ...(      indexNaturality _ _ _)
53 |   ~~ g (index i xs)     ...(prf _)
54 |   ~~ index i (map g xs) ...(sym $ indexNaturality _ _ _)
55 |
56 | ||| function extensionality is a congruence wrt map
57 | export
58 | mapExtensional : (f, g : a -> b)
59 |   -> (prf : (x : a) -> f x = g x)
60 |   -> (xs : Vect n a)
61 |   -> map f xs = map g xs
62 | mapExtensional f g prf xs = mapRestrictedExtensional f g xs (\i => prf (index i xs))
63 |
64 | ||| map-fusion property for vectors up to function extensionality
65 | export
66 | mapFusion : (f : b -> c) -> (g : a -> b) -> (xs : Vect n a)
67 |   -> map f (map g xs) = map (f . g) xs
68 | mapFusion f g    []     = Refl
69 | mapFusion f g (x :: xs) = cong (f $ g x ::) $ mapFusion f g xs
70 |
71 | ||| function extensionality is a congruence wrt mapWithElem
72 | export
73 | mapWithElemExtensional : (xs : Vect n a) -> (f, g :  (x : a) -> (0 _ : x `Elem` xs) -> b)
74 |   -> ((x : a) -> (0 pos : x `Elem` xs) -> f x pos = g x pos)
75 |   -> mapWithElem xs f = mapWithElem xs g
76 | mapWithElemExtensional    []     f g prf = Refl
77 | mapWithElemExtensional (x :: xs) f g prf
78 |   = cong2 (::) (prf x Here)
79 |                (mapWithElemExtensional xs _ _ (\x,pos => prf x (There pos)))
80 |