git.iko.soy/Idris-dev
on 76ec3fe help sign in
Idris-dev/libs/base/Control/Isomorphism.idr
316 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 swap swap swapSwap swapSwap
43 where swap : Either a' b' -> Either b' a' -- a & b are parameters, so fixed!
44 swap (Left x) = Right x
45 swap (Right x) = Left x
46 swapSwap : (e : Either a' b') -> swap (swap e) = e
47 swapSwap (Left x) = Refl
48 swapSwap (Right x) = Refl
50||| Disjunction is associative
51eitherAssoc : Iso (Either (Either a b) c) (Either a (Either b c))
52eitherAssoc = MkIso eitherAssoc1 eitherAssoc2 ok1 ok2
53 where eitherAssoc1 : Either (Either a b) c -> Either a (Either b c)
54 eitherAssoc1 (Left (Left x)) = Left x
55 eitherAssoc1 (Left (Right x)) = Right (Left x)
56 eitherAssoc1 (Right x) = Right (Right x)
58 eitherAssoc2 : Either a (Either b c) -> Either (Either a b) c
59 eitherAssoc2 (Left x) = Left (Left x)
60 eitherAssoc2 (Right (Left x)) = Left (Right x)
61 eitherAssoc2 (Right (Right x)) = Right x
63 ok1 : (x : Either a (Either b c)) -> eitherAssoc1 (eitherAssoc2 x) = x
64 ok1 (Left x) = Refl
65 ok1 (Right (Left x)) = Refl
66 ok1 (Right (Right x)) = Refl
68 ok2 : (x : Either (Either a b) c) -> eitherAssoc2 (eitherAssoc1 x) = x
69 ok2 (Left (Left x)) = Refl
70 ok2 (Left (Right x)) = Refl
71 ok2 (Right x) = Refl
73||| Disjunction with false is a no-op
74eitherBotLeft : Iso (Either Void a) a
75eitherBotLeft = MkIso to from ok1 ok2
76 where to : Either Void a -> a
77 to (Left x) = void x
78 to (Right x) = x
79 from : a -> Either Void a
80 from = Right
81 ok1 : (x : a) -> to (from x) = x
82 ok1 x = Refl
83 ok2 : (x : Either Void a) -> from (to x) = x
84 ok2 (Left x) = void x
85 ok2 (Right x) = Refl
87||| Disjunction with false is a no-op
88eitherBotRight : Iso (Either a Void) a
89eitherBotRight = isoTrans eitherComm eitherBotLeft
91||| Isomorphism is a congruence with regards to disjunction
92eitherCong : Iso a a' -> Iso b b' -> Iso (Either a b) (Either a' b')
93eitherCong {a = a} {a' = a'} {b = b} {b' = b'}
94 (MkIso to from toFrom fromTo)
95 (MkIso to' from' toFrom' fromTo') =
96 MkIso (eitherMap to to') (eitherMap from from') ok1 ok2
97 where eitherMap : (c -> c') -> (d -> d') -> Either c d -> Either c' d'
98 eitherMap f g (Left x) = Left (f x)
99 eitherMap f g (Right x) = Right (g x)
100 ok1 : (x : Either a' b') -> eitherMap to to' (eitherMap from from' x) = x
101 ok1 (Left x) = cong (toFrom x)
102 ok1 (Right x) = cong (toFrom' x)
103 ok2 : (x : Either a b) -> eitherMap from from' (eitherMap to to' x) = x
104 ok2 (Left x) = cong (fromTo x)
105 ok2 (Right x) = cong (fromTo' x)
107||| Isomorphism is a congruence with regards to disjunction on the left
108eitherCongLeft : Iso a a' -> Iso (Either a b) (Either a' b)
109eitherCongLeft i = eitherCong i isoRefl
111||| Isomorphism is a congruence with regards to disjunction on the right
112eitherCongRight : Iso b b' -> Iso (Either a b) (Either a b')
113eitherCongRight i = eitherCong isoRefl i
115-- Isomorphisms over products
116||| Conjunction is commutative
117pairComm : Iso (a, b) (b, a)
118pairComm = MkIso swap swap swapSwap swapSwap
119 where swap : (a', b') -> (b', a')
120 swap (x, y) = (y, x)
122 swapSwap : (x : (a', b')) -> swap (swap x) = x
123 swapSwap (x, y) = Refl
125||| Conjunction is associative
126pairAssoc : Iso (a, (b, c)) ((a, b), c)
127pairAssoc = MkIso to from ok1 ok2
128 where
129 to : (a, (b, c)) -> ((a, b), c)
130 to (x, (y, z)) = ((x, y), z)
131 from : ((a, b), c) -> (a, (b, c))
132 from ((x, y), z) = (x, (y, z))
133 ok1 : (x : ((a, b), c)) -> to (from x) = x
134 ok1 ((x, y), z) = Refl
135 ok2 : (x : (a, (b, c))) -> from (to x) = x
136 ok2 (x, (y, z)) = Refl
138||| Conjunction with truth is a no-op
139pairUnitRight : Iso (a, ()) a
140pairUnitRight = MkIso fst (\x => (x, ())) (\x => Refl) ok
141 where ok : (x : (a, ())) -> (fst x, ()) = x
142 ok (x, ()) = Refl
144||| Conjunction with truth is a no-op
145pairUnitLeft : Iso ((), a) a
146pairUnitLeft = isoTrans pairComm pairUnitRight
148||| Conjunction preserves falsehood
149pairBotLeft : Iso (Void, a) Void
150pairBotLeft = MkIso fst void (\x => void x) (\y => void (fst y))
152||| Conjunction preserves falsehood
153pairBotRight : Iso (a, Void) Void
154pairBotRight = isoTrans pairComm pairBotLeft
156||| Isomorphism is a congruence with regards to conjunction
157pairCong : Iso a a' -> Iso b b' -> Iso (a, b) (a', b')
158pairCong {a = a} {a' = a'} {b = b} {b' = b'}
159 (MkIso to from toFrom fromTo)
160 (MkIso to' from' toFrom' fromTo') =
161 MkIso to'' from'' iso1 iso2
162 where to'' : (a, b) -> (a', b')
163 to'' (x, y) = (to x, to' y)
164 from'' : (a', b') -> (a, b)
165 from'' (x, y) = (from x, from' y)
166 iso1 : (x : (a', b')) -> to'' (from'' x) = x
167 iso1 (x, y) = rewrite toFrom x in
168 rewrite toFrom' y in
169 Refl
170 iso2 : (x : (a, b)) -> from'' (to'' x) = x
171 iso2 (x, y) = rewrite fromTo x in
172 rewrite fromTo' y in
173 Refl
175||| Isomorphism is a congruence with regards to conjunction on the left
176pairCongLeft : Iso a a' -> Iso (a, b) (a', b)
177pairCongLeft i = pairCong i isoRefl
179||| Isomorphism is a congruence with regards to conjunction on the right
180pairCongRight : Iso b b' -> Iso (a, b) (a, b')
181pairCongRight = pairCong isoRefl
183-- Distributivity of products over sums
184||| Products distribute over sums
185distribLeft : Iso (Either a b, c) (Either (a, c) (b, c))
186distribLeft = MkIso to from toFrom fromTo
187 where to : (Either a b, c) -> Either (a, c) (b, c)
188 to (Left x, y) = Left (x, y)
189 to (Right x, y) = Right (x, y)
190 from : Either (a, c) (b, c) -> (Either a b, c)
191 from (Left (x, y)) = (Left x, y)
192 from (Right (x, y)) = (Right x, y)
193 toFrom : (x : Either (a, c) (b, c)) -> to (from x) = x
194 toFrom (Left (x, y)) = Refl
195 toFrom (Right (x, y)) = Refl
196 fromTo : (x : (Either a b, c)) -> from (to x) = x
197 fromTo (Left x, y) = Refl
198 fromTo (Right x, y) = Refl
200||| Products distribute over sums
201distribRight : Iso (a, Either b c) (Either (a, b) (a, c))
202distribRight {a} {b} {c} = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm
205-- Enable preorder reasoning syntax over isomorphisms
206||| Used for preorder reasoning syntax. Not intended for direct use.
207qed : (a : Type) -> Iso a a
208qed a = isoRefl
210||| Used for preorder reasoning syntax. Not intended for direct use.
211step : (a : Type) -> Iso a b -> Iso b c -> Iso a c
212step a iso1 iso2 = isoTrans iso1 iso2
216-- Isomorphisms over Maybe
217||| Isomorphism is a congruence with respect to Maybe
218maybeCong : Iso a b -> Iso (Maybe a) (Maybe b)
219maybeCong {a} {b} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2
220 where ok1 : (y : Maybe b) -> map to (map from y) = y
221 ok1 Nothing = Refl
222 ok1 (Just x) = (Just (to (from x))) ={ cong (toFrom x) }= (Just x) QED
223 ok2 : (x : Maybe a) -> map from (map to x) = x
224 ok2 Nothing = Refl
225 ok2 (Just x) = (Just (from (to x))) ={ cong (fromTo x) }= (Just x) QED
227||| `Maybe a` is the same as `Either a ()`
228maybeEither : Iso (Maybe a) (Either a ())
229maybeEither = MkIso to from iso1 iso2
230 where to : Maybe a -> Either a ()
231 to Nothing = Right ()
232 to (Just x) = Left x
233 from : Either a () -> Maybe a
234 from (Left x) = Just x
235 from (Right ()) = Nothing
236 iso1 : (x : Either a ()) -> to (from x) = x
237 iso1 (Left x) = Refl
238 iso1 (Right ()) = Refl
239 iso2 : (y : Maybe a) -> from (to y) = y
240 iso2 Nothing = Refl
241 iso2 (Just x) = Refl
243||| Maybe of void is just unit
244maybeVoidUnit : Iso (Maybe Void) ()
245maybeVoidUnit = (Maybe Void) ={ maybeEither }=
246 (Either Void ()) ={ eitherBotLeft }=
247 () QED
249eitherMaybeLeftMaybe : Iso (Either (Maybe a) b) (Maybe (Either a b))
250eitherMaybeLeftMaybe {a} {b} =
251 (Either (Maybe a) b) ={ eitherCongLeft maybeEither }=
252 (Either (Either a ()) b) ={ eitherAssoc }=
253 (Either a (Either () b)) ={ eitherCongRight eitherComm }=
254 (Either a (Either b ())) ={ isoSym eitherAssoc }=
255 (Either (Either a b) ()) ={ isoSym maybeEither }=
256 (Maybe (Either a b)) QED
259eitherMaybeRightMaybe : Iso (Either a (Maybe b)) (Maybe (Either a b))
260eitherMaybeRightMaybe {a} {b} =
261 (Either a (Maybe b)) ={ eitherComm }=
262 (Either (Maybe b) a) ={ eitherMaybeLeftMaybe }=
263 (Maybe (Either b a)) ={ maybeCong eitherComm }=
264 (Maybe (Either a b)) QED
267-- Isomorphisms over Fin
269maybeIsoS : Iso (Maybe (Fin n)) (Fin (S n))
270maybeIsoS = MkIso forth back fb bf
271 where forth : Maybe (Fin n) -> Fin (S n)
272 forth Nothing = FZ
273 forth (Just x) = FS x
274 back : Fin (S n) -> Maybe (Fin n)
275 back FZ = Nothing
276 back (FS x) = Just x
277 bf : (x : Maybe (Fin n)) -> back (forth x) = x
278 bf Nothing = Refl
279 bf (Just x) = Refl
280 fb : (y : Fin (S n)) -> forth (back y) = y
281 fb FZ = Refl
282 fb (FS x) = Refl
284finZeroBot : Iso (Fin 0) Void
285finZeroBot = MkIso (\x => void (uninhabited x))
286 (\x => void x)
287 (\x => void x)
288 (\x => void (uninhabited x))
290eitherFinPlus : Iso (Either (Fin m) (Fin n)) (Fin (m + n))
291eitherFinPlus {m = Z} {n=n} =
292 (Either (Fin 0) (Fin n)) ={ eitherCongLeft finZeroBot }=
293 (Either Void (Fin n)) ={ eitherBotLeft }=
294 (Fin n) QED
295eitherFinPlus {m = S k} {n=n} =
296 (Either (Fin (S k)) (Fin n)) ={ eitherCongLeft (isoSym maybeIsoS) }=
297 (Either (Maybe (Fin k)) (Fin n)) ={ eitherMaybeLeftMaybe }=
298 (Maybe (Either (Fin k) (Fin n))) ={ maybeCong eitherFinPlus }=
299 (Maybe (Fin (k + n))) ={ maybeIsoS }=
300 (Fin (S (k + n))) QED
303finPairTimes : Iso (Fin m, Fin n) (Fin (m * n))
304finPairTimes {m = Z} {n=n} =
305 (Fin Z, Fin n) ={ pairCongLeft finZeroBot }=
306 (Void, Fin n) ={ pairBotLeft }=
307 Void ={ isoSym finZeroBot }=
308 (Fin Z) QED
309finPairTimes {m = S k} {n=n} =
310 (Fin (S k), Fin n) ={ pairCongLeft (isoSym maybeIsoS) }=
311 (Maybe (Fin k), Fin n) ={ pairCongLeft maybeEither }=
312 (Either (Fin k) (), Fin n) ={ distribLeft }=
313 (Either (Fin k, Fin n) ((), Fin n)) ={ eitherCong finPairTimes pairUnitLeft }=
314 (Either (Fin (k * n)) (Fin n)) ={ eitherComm }=
315 (Either (Fin n) (Fin (k * n))) ={ eitherFinPlus }=
316 (Fin (n + (k * n))) QED