git.iko.soy/Idris-dev
on 54e4e41 help sign in
Idris-dev/libs/base/Control/Isomorphism.idr
310 lines 12 kB history raw
1module Control.Isomorphism
3import Syntax.PreorderReasoning
4import Data.Fin
6%default total
8||| An isomorphism between two types
9data Iso : Type -> Type -> Type where
10 MkIso : (to : a -> b) ->
11 (from : b -> a) ->
12 (toFrom : (y : b) -> to (from y) = y) ->
13 (fromTo : (x : a) -> from (to x) = x) ->
14 Iso a b
16-- Isomorphism properties
18||| Isomorphism is Reflexive
19isoRefl : Iso a a
20isoRefl = MkIso id id (\x => Refl) (\x => Refl)
22||| Isomorphism is transitive
23isoTrans : Iso a b -> Iso b c -> Iso a c
24isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
25 MkIso (\x => to' (to x))
26 (\y => from (from' y))
27 (\y => (to' (to (from (from' y)))) ={ cong (toFrom (from' y)) }=
28 (to' (from' y)) ={ toFrom' y }=
29 y QED)
30 (\x => (from (from' (to' (to x)))) ={ cong (fromTo' (to x)) }=
31 (from (to x)) ={ fromTo x }=
32 x QED)
34||| Isomorphism is symmetric
35isoSym : Iso a b -> Iso b a
36isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom
38-- Isomorphisms over sums
40||| Disjunction is commutative
41eitherComm : Iso (Either a b) (Either b a)
42eitherComm = MkIso mirror mirror mirrorMirror mirrorMirror
43 where mirrorMirror : (e : Either a' b') -> mirror (mirror e) = e
44 mirrorMirror (Left x) = Refl
45 mirrorMirror (Right x) = Refl
47||| Disjunction is associative
48eitherAssoc : Iso (Either (Either a b) c) (Either a (Either b c))
49eitherAssoc = MkIso eitherAssoc1 eitherAssoc2 ok1 ok2
50 where eitherAssoc1 : Either (Either a b) c -> Either a (Either b c)
51 eitherAssoc1 (Left (Left x)) = Left x
52 eitherAssoc1 (Left (Right x)) = Right (Left x)
53 eitherAssoc1 (Right x) = Right (Right x)
55 eitherAssoc2 : Either a (Either b c) -> Either (Either a b) c
56 eitherAssoc2 (Left x) = Left (Left x)
57 eitherAssoc2 (Right (Left x)) = Left (Right x)
58 eitherAssoc2 (Right (Right x)) = Right x
60 ok1 : (x : Either a (Either b c)) -> eitherAssoc1 (eitherAssoc2 x) = x
61 ok1 (Left x) = Refl
62 ok1 (Right (Left x)) = Refl
63 ok1 (Right (Right x)) = Refl
65 ok2 : (x : Either (Either a b) c) -> eitherAssoc2 (eitherAssoc1 x) = x
66 ok2 (Left (Left x)) = Refl
67 ok2 (Left (Right x)) = Refl
68 ok2 (Right x) = Refl
70||| Disjunction with false is a no-op
71eitherBotLeft : Iso (Either Void a) a
72eitherBotLeft = MkIso to from ok1 ok2
73 where to : Either Void a -> a
74 to (Left x) = void x
75 to (Right x) = x
76 from : a -> Either Void a
77 from = Right
78 ok1 : (x : a) -> to (from x) = x
79 ok1 x = Refl
80 ok2 : (x : Either Void a) -> from (to x) = x
81 ok2 (Left x) = void x
82 ok2 (Right x) = Refl
84||| Disjunction with false is a no-op
85eitherBotRight : Iso (Either a Void) a
86eitherBotRight = isoTrans eitherComm eitherBotLeft
88||| Isomorphism is a congruence with regards to disjunction
89eitherCong : Iso a a' -> Iso b b' -> Iso (Either a b) (Either a' b')
90eitherCong {a = a} {a' = a'} {b = b} {b' = b'}
91 (MkIso to from toFrom fromTo)
92 (MkIso to' from' toFrom' fromTo') =
93 MkIso (eitherMap to to') (eitherMap from from') ok1 ok2
94 where eitherMap : (c -> c') -> (d -> d') -> Either c d -> Either c' d'
95 eitherMap f g (Left x) = Left (f x)
96 eitherMap f g (Right x) = Right (g x)
97 ok1 : (x : Either a' b') -> eitherMap to to' (eitherMap from from' x) = x
98 ok1 (Left x) = cong (toFrom x)
99 ok1 (Right x) = cong (toFrom' x)
100 ok2 : (x : Either a b) -> eitherMap from from' (eitherMap to to' x) = x
101 ok2 (Left x) = cong (fromTo x)
102 ok2 (Right x) = cong (fromTo' x)
104||| Isomorphism is a congruence with regards to disjunction on the left
105eitherCongLeft : Iso a a' -> Iso (Either a b) (Either a' b)
106eitherCongLeft i = eitherCong i isoRefl
108||| Isomorphism is a congruence with regards to disjunction on the right
109eitherCongRight : Iso b b' -> Iso (Either a b) (Either a b')
110eitherCongRight i = eitherCong isoRefl i
112-- Isomorphisms over products
113||| Conjunction is commutative
114pairComm : Iso (a, b) (b, a)
115pairComm = MkIso swap swap swapSwap swapSwap
116 where swapSwap : (x : (a', b')) -> swap (swap x) = x
117 swapSwap (x, y) = Refl
119||| Conjunction is associative
120pairAssoc : Iso (a, (b, c)) ((a, b), c)
121pairAssoc = MkIso to from ok1 ok2
122 where
123 to : (a, (b, c)) -> ((a, b), c)
124 to (x, (y, z)) = ((x, y), z)
125 from : ((a, b), c) -> (a, (b, c))
126 from ((x, y), z) = (x, (y, z))
127 ok1 : (x : ((a, b), c)) -> to (from x) = x
128 ok1 ((x, y), z) = Refl
129 ok2 : (x : (a, (b, c))) -> from (to x) = x
130 ok2 (x, (y, z)) = Refl
132||| Conjunction with truth is a no-op
133pairUnitRight : Iso (a, ()) a
134pairUnitRight = MkIso fst (\x => (x, ())) (\x => Refl) ok
135 where ok : (x : (a, ())) -> (fst x, ()) = x
136 ok (x, ()) = Refl
138||| Conjunction with truth is a no-op
139pairUnitLeft : Iso ((), a) a
140pairUnitLeft = isoTrans pairComm pairUnitRight
142||| Conjunction preserves falsehood
143pairBotLeft : Iso (Void, a) Void
144pairBotLeft = MkIso fst void (\x => void x) (\y => void (fst y))
146||| Conjunction preserves falsehood
147pairBotRight : Iso (a, Void) Void
148pairBotRight = isoTrans pairComm pairBotLeft
150||| Isomorphism is a congruence with regards to conjunction
151pairCong : Iso a a' -> Iso b b' -> Iso (a, b) (a', b')
152pairCong {a = a} {a' = a'} {b = b} {b' = b'}
153 (MkIso to from toFrom fromTo)
154 (MkIso to' from' toFrom' fromTo') =
155 MkIso to'' from'' iso1 iso2
156 where to'' : (a, b) -> (a', b')
157 to'' (x, y) = (to x, to' y)
158 from'' : (a', b') -> (a, b)
159 from'' (x, y) = (from x, from' y)
160 iso1 : (x : (a', b')) -> to'' (from'' x) = x
161 iso1 (x, y) = rewrite toFrom x in
162 rewrite toFrom' y in
163 Refl
164 iso2 : (x : (a, b)) -> from'' (to'' x) = x
165 iso2 (x, y) = rewrite fromTo x in
166 rewrite fromTo' y in
167 Refl
169||| Isomorphism is a congruence with regards to conjunction on the left
170pairCongLeft : Iso a a' -> Iso (a, b) (a', b)
171pairCongLeft i = pairCong i isoRefl
173||| Isomorphism is a congruence with regards to conjunction on the right
174pairCongRight : Iso b b' -> Iso (a, b) (a, b')
175pairCongRight = pairCong isoRefl
177-- Distributivity of products over sums
178||| Products distribute over sums
179distribLeft : Iso (Either a b, c) (Either (a, c) (b, c))
180distribLeft = MkIso to from toFrom fromTo
181 where to : (Either a b, c) -> Either (a, c) (b, c)
182 to (Left x, y) = Left (x, y)
183 to (Right x, y) = Right (x, y)
184 from : Either (a, c) (b, c) -> (Either a b, c)
185 from (Left (x, y)) = (Left x, y)
186 from (Right (x, y)) = (Right x, y)
187 toFrom : (x : Either (a, c) (b, c)) -> to (from x) = x
188 toFrom (Left (x, y)) = Refl
189 toFrom (Right (x, y)) = Refl
190 fromTo : (x : (Either a b, c)) -> from (to x) = x
191 fromTo (Left x, y) = Refl
192 fromTo (Right x, y) = Refl
194||| Products distribute over sums
195distribRight : Iso (a, Either b c) (Either (a, b) (a, c))
196distribRight {a} {b} {c} = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm
199-- Enable preorder reasoning syntax over isomorphisms
200||| Used for preorder reasoning syntax. Not intended for direct use.
201qed : (a : Type) -> Iso a a
202qed a = isoRefl
204||| Used for preorder reasoning syntax. Not intended for direct use.
205step : (a : Type) -> Iso a b -> Iso b c -> Iso a c
206step a iso1 iso2 = isoTrans iso1 iso2
210-- Isomorphisms over Maybe
211||| Isomorphism is a congruence with respect to Maybe
212maybeCong : Iso a b -> Iso (Maybe a) (Maybe b)
213maybeCong {a} {b} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2
214 where ok1 : (y : Maybe b) -> map to (map from y) = y
215 ok1 Nothing = Refl
216 ok1 (Just x) = (Just (to (from x))) ={ cong (toFrom x) }= (Just x) QED
217 ok2 : (x : Maybe a) -> map from (map to x) = x
218 ok2 Nothing = Refl
219 ok2 (Just x) = (Just (from (to x))) ={ cong (fromTo x) }= (Just x) QED
221||| `Maybe a` is the same as `Either a ()`
222maybeEither : Iso (Maybe a) (Either a ())
223maybeEither = MkIso to from iso1 iso2
224 where to : Maybe a -> Either a ()
225 to Nothing = Right ()
226 to (Just x) = Left x
227 from : Either a () -> Maybe a
228 from (Left x) = Just x
229 from (Right ()) = Nothing
230 iso1 : (x : Either a ()) -> to (from x) = x
231 iso1 (Left x) = Refl
232 iso1 (Right ()) = Refl
233 iso2 : (y : Maybe a) -> from (to y) = y
234 iso2 Nothing = Refl
235 iso2 (Just x) = Refl
237||| Maybe of void is just unit
238maybeVoidUnit : Iso (Maybe Void) ()
239maybeVoidUnit = (Maybe Void) ={ maybeEither }=
240 (Either Void ()) ={ eitherBotLeft }=
241 () QED
243eitherMaybeLeftMaybe : Iso (Either (Maybe a) b) (Maybe (Either a b))
244eitherMaybeLeftMaybe {a} {b} =
245 (Either (Maybe a) b) ={ eitherCongLeft maybeEither }=
246 (Either (Either a ()) b) ={ eitherAssoc }=
247 (Either a (Either () b)) ={ eitherCongRight eitherComm }=
248 (Either a (Either b ())) ={ isoSym eitherAssoc }=
249 (Either (Either a b) ()) ={ isoSym maybeEither }=
250 (Maybe (Either a b)) QED
253eitherMaybeRightMaybe : Iso (Either a (Maybe b)) (Maybe (Either a b))
254eitherMaybeRightMaybe {a} {b} =
255 (Either a (Maybe b)) ={ eitherComm }=
256 (Either (Maybe b) a) ={ eitherMaybeLeftMaybe }=
257 (Maybe (Either b a)) ={ maybeCong eitherComm }=
258 (Maybe (Either a b)) QED
261-- Isomorphisms over Fin
263maybeIsoS : Iso (Maybe (Fin n)) (Fin (S n))
264maybeIsoS = MkIso forth back fb bf
265 where forth : Maybe (Fin n) -> Fin (S n)
266 forth Nothing = FZ
267 forth (Just x) = FS x
268 back : Fin (S n) -> Maybe (Fin n)
269 back FZ = Nothing
270 back (FS x) = Just x
271 bf : (x : Maybe (Fin n)) -> back (forth x) = x
272 bf Nothing = Refl
273 bf (Just x) = Refl
274 fb : (y : Fin (S n)) -> forth (back y) = y
275 fb FZ = Refl
276 fb (FS x) = Refl
278finZeroBot : Iso (Fin 0) Void
279finZeroBot = MkIso (\x => void (uninhabited x))
280 (\x => void x)
281 (\x => void x)
282 (\x => void (uninhabited x))
284eitherFinPlus : Iso (Either (Fin m) (Fin n)) (Fin (m + n))
285eitherFinPlus {m = Z} {n=n} =
286 (Either (Fin 0) (Fin n)) ={ eitherCongLeft finZeroBot }=
287 (Either Void (Fin n)) ={ eitherBotLeft }=
288 (Fin n) QED
289eitherFinPlus {m = S k} {n=n} =
290 (Either (Fin (S k)) (Fin n)) ={ eitherCongLeft (isoSym maybeIsoS) }=
291 (Either (Maybe (Fin k)) (Fin n)) ={ eitherMaybeLeftMaybe }=
292 (Maybe (Either (Fin k) (Fin n))) ={ maybeCong eitherFinPlus }=
293 (Maybe (Fin (k + n))) ={ maybeIsoS }=
294 (Fin (S (k + n))) QED
297finPairTimes : Iso (Fin m, Fin n) (Fin (m * n))
298finPairTimes {m = Z} {n=n} =
299 (Fin Z, Fin n) ={ pairCongLeft finZeroBot }=
300 (Void, Fin n) ={ pairBotLeft }=
301 Void ={ isoSym finZeroBot }=
302 (Fin Z) QED
303finPairTimes {m = S k} {n=n} =
304 (Fin (S k), Fin n) ={ pairCongLeft (isoSym maybeIsoS) }=
305 (Maybe (Fin k), Fin n) ={ pairCongLeft maybeEither }=
306 (Either (Fin k) (), Fin n) ={ distribLeft }=
307 (Either (Fin k, Fin n) ((), Fin n)) ={ eitherCong finPairTimes pairUnitLeft }=
308 (Either (Fin (k * n)) (Fin n)) ={ eitherComm }=
309 (Either (Fin n) (Fin (k * n))) ={ eitherFinPlus }=
310 (Fin (n + (k * n))) QED