@@ -0,0 +1,158 @@
1+module Control.Isomorphism.Vect
2+
3+import Interfaces.Verified
4+import Control.Isomorphism
5+import Data.Vect
6+
7+%default total
8+%access public export
9+
10+||| `Vect Z a` has only one value: `[]`.
11+nilUnit : Iso (Vect Z a) ()
12+nilUnit = MkIso (const ()) (const []) (\() => Refl) (\[] => Refl)
13+
14+||| A `Vect (S Z) a` is just an `a`.
15+oneIdentity : Iso (Vect (S Z) a) a
16+oneIdentity = MkIso to (\x => [x]) (\x => Refl) (\[x] => Refl)
17+ where to : Vect 1 a -> a
18+ to [x] = x
19+
20+||| Moves between `x :: xs` and `(x, xs)`.
21+consPair : Iso (Vect (S n) a) (a, Vect n a)
22+consPair = MkIso to (uncurry (::)) (\(x, xs) => Refl) (\(x :: xs) => Refl)
23+ where to : Vect (S n) a -> (a, Vect n a)
24+ to (x :: xs) = (x, xs)
25+
26+||| An `Iso` based on `splitAt` and `(++)`.
27+splitPair : Iso (Vect (n + m) a) (Vect n a, Vect m a)
28+splitPair {n} {m} = MkIso (splitAt n) (uncurry (++)) toFrom fromTo
29+ where pairify : q = w -> e = r -> (q, e) = (w, r)
30+ pairify Refl Refl = Refl
31+ toFrom (ns, ms) = trans (splitAtTakeDrop n (ns ++ ms)) $ pairify (takePrefix ns ms) (dropPrefix ns ms)
32+ fromTo xs = rewrite splitAtTakeDrop {m=m} n xs in takeDropConcat n xs
33+
34+vectLiftIso : Iso l r -> Iso (Vect n l) (Vect n r)
35+vectLiftIso (MkIso to from toFrom fromTo) = MkIso (map to) (map from) toFrom' fromTo'
36+ where toFrom' : {n : Nat} -> (rs : Vect n r) -> map to (map from rs) = rs
37+ toFrom' [] = Refl
38+ toFrom' (x :: xs) = rewrite toFrom x in rewrite toFrom' xs in Refl
39+ fromTo' : {n : Nat} -> (ls : Vect n l) -> map from (map to ls) = ls
40+ fromTo' [] = Refl
41+ fromTo' (x :: xs) = rewrite fromTo x in rewrite fromTo' xs in Refl
42+
43+zipped : Iso (Vect n a, Vect n b) (Vect n (a, b))
44+zipped = MkIso (uncurry zip) unzip toFrom (\(as, bs) => fromTo as bs)
45+ where toFrom : {n : Nat} -> (xs : Vect n (a, b)) -> uncurry Vect.zip (unzip xs) = xs
46+ toFrom [] = Refl
47+ toFrom ((a, b) :: xs) with (unzip xs) proof p
48+ | (as, bs) = cong $ trans (cong p) (toFrom xs)
49+ fromTo : {n : Nat} -> (as : Vect n a) -> (bs : Vect n b) -> unzip (zip as bs) = (as, bs)
50+ fromTo [] [] = Refl
51+ fromTo (a :: as) (b :: bs) = rewrite fromTo as bs in Refl
52+
53+zipped3 : Iso (Vect n a, Vect n b, Vect n c) (Vect n (a, b, c))
54+zipped3 = MkIso (uncurrry zip3) unzip3 toFrom (\(as, bs, cs) => fromTo as bs cs)
55+ where uncurrry : (w -> x -> y -> z) -> ((w, x, y) -> z)
56+ uncurrry w (x, y, z) = w x y z
57+ toFrom : {n : Nat} -> (xs : Vect n (a, b, c)) -> uncurrry Vect.zip3 (unzip3 xs) = xs
58+ toFrom [] = Refl
59+ toFrom ((a, b, c) :: xs) with (unzip3 xs) proof p
60+ | (as, bs, cs) = cong $ trans (cong p) (toFrom xs)
61+ fromTo : {n : Nat} -> (as : Vect n a) -> (bs : Vect n b) -> (cs : Vect n c) -> unzip3 (zip3 as bs cs) = (as, bs, cs)
62+ fromTo [] [] [] = Refl
63+ fromTo (a :: as) (b :: bs) (c :: cs) = rewrite fromTo as bs cs in Refl
64+
65+||| An `Iso` based on `transpose`.
66+transposition : Iso (Vect o (Vect i a)) (Vect i (Vect o a))
67+transposition {a} = MkIso transpose transpose prf prf
68+ where prf : {i : Nat} -> {o : Nat} -> (xss : Vect o (Vect i a)) -> transpose (transpose xss) = xss
69+ prf [] = vectMustBeNil $ transpose [| [] |]
70+ prf (xs :: xss) = rewrite transposeCons xs (transpose xss) in cong (prf xss)
71+||| Split the `Vect` every `m` elements, making `n` `Vect m a`s.
72+||| The result is rectangular and has the same order as the original.
73+|||
74+||| This is the inverse of `concat`.
75+unconcat : Vect (n * m) a -> Vect n (Vect m a)
76+unconcat {n = Z} [] = []
77+unconcat {n = S k} {m} xs = let (xs', xss) = splitAt m xs in xs' :: unconcat xss
78+||| An `Iso` based on `unconcat` and `concat`.
79+|||
80+||| ```idris example
81+||| from rectangular [[1,2,3],[4,5,6]]
82+||| ```
83+rectangular : Iso (Vect (n * m) a) (Vect n (Vect m a))
84+rectangular = MkIso unconcat concat toFrom fromTo
85+-- TODO: Clean up after #4001 is fixed
86+ where toFrom : (xss : Vect i (Vect o a)) -> unconcat (concat xss) = xss
87+ toFrom {i = Z} [] = Refl
88+ toFrom {i = S k} {o} (xs :: xss) with (splitAt o (xs ++ concat xss)) proof p
89+ | (tk, dr) = let sATK = sym $ trans p $ splitAtTakeDrop o (xs ++ concat xss)
90+ tkp = trans (sym $ takePrefix xs $ concat xss) $ cong {f=fst} sATK
91+ drp = trans (sym $ toFrom xss) $ cong {f=unconcat} $ trans (sym $ dropPrefix xs $ concat xss) $ cong {f=snd} sATK
92+ in replace {P = \dr' => tk :: dr' = xs :: xss} drp $ replace {P = \tk' => tk' :: xss = xs :: xss} tkp Refl
93+ fromTo : (xs : Vect (i * o) a) -> concat (unconcat xs) = xs
94+ fromTo {i = Z} [] = Refl
95+ fromTo {i = S k} {o} xs with (splitAt o xs) proof p
96+ | (tk, dr) = let sATK = sym $ trans p $ splitAtTakeDrop o xs
97+ tkp = cong {f=fst} sATK
98+ drp = trans (cong {f=snd} sATK) $ sym $ fromTo dr
99+ in replace {P = \dr' => tk ++ dr' = xs} drp $ replace {P = \tk' => tk' ++ drop o xs = xs } tkp $ takeDropConcat o xs
100+
101+-- Not an Iso because (=) is not extensional, but it works in spirit
102+||| Go through all possible inputs and tabulate the outputs in a `Vect`.
103+|||
104+||| Or: turn a function from indices to values into a `Vect`.
105+||| Or: the inverse of `index`.
106+unindex : (Fin n -> a) -> Vect n a
107+unindex {n = Z} _ = []
108+unindex {n = S k} f = f FZ :: unindex (f . FS)
109+||| Indexing into the table of outputs of `f` is like calling `f` itself.
110+indexUnindex : (i : Fin n) -> (f : Fin n -> a) -> index i (unindex f) = f i
111+indexUnindex FZ _ = Refl
112+indexUnindex (FS k) f = rewrite indexUnindex k (f . FS) in Refl
113+||| Given a function `f`, a `Vect` `xs`, and a proof that calling `f` gives the same result as indexing into `xs`,
114+||| prove that `xs` is the table of outputs of `f`.
115+unindexIndex' : (xs : Vect n a) -> (f : Fin n -> a) -> ((i : Fin n) -> f i = index i xs) -> unindex f = xs
116+unindexIndex' [] _ _ = Refl
117+unindexIndex' (x :: xs) f prf = rewrite prf FZ in rewrite unindexIndex' xs (f . FS) (\i => rewrite prf $ FS i in Refl) in Refl
118+||| If `f` and `g` are extensionally equal (equal outputs for all inputs), then `unindex f = unindex g`.
119+congExtUnindex : (f : Fin n -> a) -> (g : Fin n -> a) -> ((i : Fin n) -> f i = g i) -> unindex f = unindex g
120+congExtUnindex f g p = unindexIndex' (unindex g) f $ \i => trans (p i) $ sym $ indexUnindex i g
121+||| Functions with the same tables are the same themselves.
122+injExtUnindex : (f : Fin n -> a) -> (g : Fin n -> a) -> unindex f = unindex g -> ((i : Fin n) -> f i = g i)
123+injExtUnindex f g p i = rewrite sym $ indexUnindex i f in rewrite sym $ indexUnindex i g in cong p
124+||| A simpler version of `unindexIndex'` which only proves that `unindex` is the inverse of `index`.
125+unindexIndex : (xs : Vect n a) -> unindex (\i => index i xs) = xs
126+unindexIndex xs = unindexIndex' xs (\i => index i xs) (\i => Refl)
127+
128+||| Given a function that computes an index in the input from the index in the output, produce a `Vect o` of elements from the input.
129+fromIndices : (Fin o -> Fin i) -> Vect i a -> Vect o a
130+fromIndices f xs = unindex (flip index xs . f)
131+indexFromIndices : (f : Fin o -> Fin i) -> (xs : Vect i a) -> (n : Fin o) -> index n (fromIndices f xs) = index (f n) xs
132+indexFromIndices f xs n = indexUnindex n (\i => index (f i) xs)
133+fromIndicesFromIndices : (to : Fin n -> Fin n) -> (from : Fin n -> Fin n) -> (fromTo : (i : Fin n) -> from (to i) = i) -> (xs : Vect n a) -> fromIndices to (fromIndices from xs) = xs
134+fromIndicesFromIndices to from fromTo xs = unindexIndex' xs (\x => index (to x) (unindex (\x' => index (from x') xs))) $ \i =>
135+ rewrite indexUnindex (to i) (\x' => index (from x') xs) in rewrite fromTo i in Refl
136+
137+||| Given a permutation of the indices, provide an `Iso` that can permute a `Vect n` the "same" way. More precisely,
138+||| if the index `i` is sent to `j`, then the element at index `i` ends up at index `j` (`indexPermuted`).
139+|||
140+||| Note this has the *opposite* behavior to `fromIndices`. This function is more "visceral"; it can be imagined
141+||| as shuffling a `Vect` in the same way `map (to permutation)` shuffles `unindex id`.
142+|||
143+||| An `Iso (Fin n) (Fin n)` represents a permutation of the integers `[0, n)`, because an `Iso` ensures that no elements are "lost" or "duplicated".
144+|||
145+||| ```idris example
146+||| to (permuted (stimes 2 rotatedDown)) [1, 2, 3, 4, 5] == [3, 4, 5, 1, 2]
147+||| ```
148+|||
149+||| @ permutation an `Iso` representing the transformation on the indices
150+permuted : (permutation : Iso (Fin n) (Fin n)) -> Iso (Vect n a) (Vect n a)
151+permuted (MkIso toI fromI toFromI fromToI) = MkIso (fromIndices fromI) (fromIndices toI) (fromIndicesFromIndices fromI toI toFromI) (fromIndicesFromIndices toI fromI fromToI)
152+-- [to, from => f from, f to] is not a typo
153+-- fromIndices needs a function outputIdx => inputIdx, so to "align" the "motion" of the Fins with the elements, to uses from and from uses to.
154+permutedSym : (permutation : Iso (Fin n) (Fin n)) -> permuted (isoSym permutation) = isoSym (permuted permutation)
155+permutedSym (MkIso to from toFrom fromTo) = Refl
156+indexPermuted : (permutation : Iso (Fin n) (Fin n)) -> (i : Fin n) -> (xs : Vect n a) -> index i xs = index (to permutation i) (to (permuted permutation) xs)
157+indexPermuted (MkIso to from toFrom fromTo) i xs = replace {P = \xs' => index i xs' = index (to i) (fromIndices from xs) } (fromIndicesFromIndices to from fromTo xs) $
158+ rewrite indexFromIndices to (fromIndices from xs) i in Refl