@@ -1,6 +1,7 @@
11module Control.Isomorphism
22
33import Syntax.PreorderReasoning
4+import Uninhabited
45
56%default total
67
@@ -96,6 +97,12 @@ eitherCong {a = a} {a' = a'} {b = b} {b' = b'}
9697 ok2 (Left x) = cong (fromTo x)
9798 ok2 (Right x) = cong (fromTo' x)
9899
100+eitherCongLeft : Iso a a' -> Iso (Either a b) (Either a' b)
101+eitherCongLeft i = eitherCong i isoRefl
102+
103+eitherCongRight : Iso b b' -> Iso (Either a b) (Either a b')
104+eitherCongRight i = eitherCong isoRefl i
105+
99106-- Isomorphisms over products
100107pairComm : Iso (a, b) (b, a)
101108pairComm = MkIso swap swap swapSwap swapSwap
@@ -148,6 +155,32 @@ pairCong {a = a} {a' = a'} {b = b} {b' = b'}
148155 rewrite fromTo' y in
149156 refl
150157
158+pairCongLeft : Iso a a' -> Iso (a, b) (a', b)
159+pairCongLeft i = pairCong i isoRefl
160+
161+pairCongRight : Iso b b' -> Iso (a, b) (a, b')
162+pairCongRight = pairCong isoRefl
163+
164+-- Distributivity of products over sums
165+distribLeft : Iso (Either a b, c) (Either (a, c) (b, c))
166+distribLeft = MkIso to from toFrom fromTo
167+ where to : (Either a b, c) -> Either (a, c) (b, c)
168+ to (Left x, y) = Left (x, y)
169+ to (Right x, y) = Right (x, y)
170+ from : Either (a, c) (b, c) -> (Either a b, c)
171+ from (Left (x, y)) = (Left x, y)
172+ from (Right (x, y)) = (Right x, y)
173+ toFrom : (x : Either (a, c) (b, c)) -> to (from x) = x
174+ toFrom (Left (x, y)) = refl
175+ toFrom (Right (x, y)) = refl
176+ fromTo : (x : (Either a b, c)) -> from (to x) = x
177+ fromTo (Left x, y) = refl
178+ fromTo (Right x, y) = refl
179+
180+distribRight : Iso (a, Either b c) (Either (a, b) (a, c))
181+distribRight {a} {b} {c} = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm
182+
183+
151184-- Enable preorder reasoning syntax over isomorphisms
152185qed : (a : Type) -> Iso a a
153186qed a = isoRefl
@@ -189,11 +222,11 @@ maybeVoidUnit = (Maybe _|_) ={ maybeEither }=
189222
190223eitherMaybeLeftMaybe : Iso (Either (Maybe a) b) (Maybe (Either a b))
191224eitherMaybeLeftMaybe {a} {b} =
192− (Either (Maybe a) b) ={ eitherCong maybeEither isoRefl }=
193− (Either (Either a ()) b) ={ eitherAssoc }=
194− (Either a (Either () b)) ={ eitherCong isoRefl eitherComm }=
195− (Either a (Either b ())) ={ isoSym eitherAssoc }=
196− (Either (Either a b) ()) ={ isoSym maybeEither }=
225+ (Either (Maybe a) b) ={ eitherCongLeft maybeEither }=
226+ (Either (Either a ()) b) ={ eitherAssoc }=
227+ (Either a (Either () b)) ={ eitherCongRight eitherComm }=
228+ (Either a (Either b ())) ={ isoSym eitherAssoc }=
229+ (Either (Either a b) ()) ={ isoSym maybeEither }=
197230 (Maybe (Either a b)) QED
198231
199232
@@ -205,3 +238,53 @@ eitherMaybeRightMaybe {a} {b} =
205238 (Maybe (Either a b)) QED
206239
207240
241+-- Isomorphisms over Fin
242+
243+maybeIsoS : Iso (Maybe (Fin n)) (Fin (S n))
244+maybeIsoS = MkIso forth back fb bf
245+ where forth : Maybe (Fin n) -> Fin (S n)
246+ forth Nothing = fZ
247+ forth (Just x) = fS x
248+ back : Fin (S n) -> Maybe (Fin n)
249+ back fZ = Nothing
250+ back (fS x) = Just x
251+ bf : (x : Maybe (Fin n)) -> back (forth x) = x
252+ bf Nothing = refl
253+ bf (Just x) = refl
254+ fb : (y : Fin (S n)) -> forth (back y) = y
255+ fb fZ = refl
256+ fb (fS x) = refl
257+
258+finZeroBot : Iso (Fin 0) _|_
259+finZeroBot = MkIso (\x => FalseElim (uninhabited x))
260+ (\x => FalseElim x)
261+ (\x => FalseElim x)
262+ (\x => FalseElim (uninhabited x))
263+
264+eitherFinPlus : Iso (Either (Fin m) (Fin n)) (Fin (m + n))
265+eitherFinPlus {m = Z} {n=n} =
266+ (Either (Fin 0) (Fin n)) ={ eitherCongLeft finZeroBot }=
267+ (Either _|_ (Fin n)) ={ eitherBotLeft }=
268+ (Fin n) QED
269+eitherFinPlus {m = S k} {n=n} =
270+ (Either (Fin (S k)) (Fin n)) ={ eitherCongLeft (isoSym maybeIsoS) }=
271+ (Either (Maybe (Fin k)) (Fin n)) ={ eitherMaybeLeftMaybe }=
272+ (Maybe (Either (Fin k) (Fin n))) ={ maybeCong eitherFinPlus }=
273+ (Maybe (Fin (k + n))) ={ maybeIsoS }=
274+ (Fin (S (k + n))) QED
275+
276+
277+finPairTimes : Iso (Fin m, Fin n) (Fin (m * n))
278+finPairTimes {m = Z} {n=n} =
279+ (Fin Z, Fin n) ={ pairCongLeft finZeroBot }=
280+ (_|_, Fin n) ={ pairBotLeft }=
281+ _|_ ={ isoSym finZeroBot }=
282+ (Fin Z) QED
283+finPairTimes {m = S k} {n=n} =
284+ (Fin (S k), Fin n) ={ pairCongLeft (isoSym maybeIsoS) }=
285+ (Maybe (Fin k), Fin n) ={ pairCongLeft maybeEither }=
286+ (Either (Fin k) (), Fin n) ={ distribLeft }=
287+ (Either (Fin k, Fin n) ((), Fin n)) ={ eitherCong finPairTimes pairUnitLeft }=
288+ (Either (Fin (k * n)) (Fin n)) ={ eitherComm }=
289+ (Either (Fin n) (Fin (k * n))) ={ eitherFinPlus }=
290+ (Fin (n + (k * n))) QED