git.iko.soy/Idris-dev
on master help sign in
Merge pull request #748 from david-christiansen/feature/isomorphisms
6b70ce0Edwin Brady
libs/base/Control/Isomorphism.idr+173−5
compare with master
unifiedsplit
@@ -1,6 +1,7 @@
1module Control.Isomorphism
1module Control.Isomorphism
2
2
3import Syntax.PreorderReasoning
3import Syntax.PreorderReasoning
4+import Uninhabited
4
5
5%default total
6%default total
6
7
@@ -22,13 +23,14 @@ isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
22 MkIso (\x => to' (to x))
23 MkIso (\x => to' (to x))
23 (\y => from (from' y))
24 (\y => from (from' y))
24 (\y => (to' (to (from (from' y)))) ={ cong (toFrom (from' y)) }=
25 (\y => (to' (to (from (from' y)))) ={ cong (toFrom (from' y)) }=
25− (to' (from' y)) ={ toFrom' y }=
26+ (to' (from' y)) ={ toFrom' y }=
26− y QED)
27+ y QED)
27 (\x => (from (from' (to' (to x)))) ={ cong (fromTo' (to x)) }=
28 (\x => (from (from' (to' (to x)))) ={ cong (fromTo' (to x)) }=
28− (from (to x)) ={ fromTo x }=
29+ (from (to x)) ={ fromTo x }=
29− x QED)
30+ x QED)
30−
31
31
32+isoSym : Iso a b -> Iso b a
33+isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom
32
34
33-- Isomorphisms over sums
35-- Isomorphisms over sums
34
36
@@ -79,6 +81,28 @@ eitherBotLeft = MkIso to from ok1 ok2
79eitherBotRight : Iso (Either a _|_) a
81eitherBotRight : Iso (Either a _|_) a
80eitherBotRight = isoTrans eitherComm eitherBotLeft
82eitherBotRight = isoTrans eitherComm eitherBotLeft
81
83
84+
85+eitherCong : Iso a a' -> Iso b b' -> Iso (Either a b) (Either a' b')
86+eitherCong {a = a} {a' = a'} {b = b} {b' = b'}
87+ (MkIso to from toFrom fromTo)
88+ (MkIso to' from' toFrom' fromTo') =
89+ MkIso (eitherMap to to') (eitherMap from from') ok1 ok2
90+ where eitherMap : (c -> c') -> (d -> d') -> Either c d -> Either c' d'
91+ eitherMap f g (Left x) = Left (f x)
92+ eitherMap f g (Right x) = Right (g x)
93+ ok1 : (x : Either a' b') -> eitherMap to to' (eitherMap from from' x) = x
94+ ok1 (Left x) = cong (toFrom x)
95+ ok1 (Right x) = cong (toFrom' x)
96+ ok2 : (x : Either a b) -> eitherMap from from' (eitherMap to to' x) = x
97+ ok2 (Left x) = cong (fromTo x)
98+ ok2 (Right x) = cong (fromTo' x)
99+
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+
82-- Isomorphisms over products
106-- Isomorphisms over products
83pairComm : Iso (a, b) (b, a)
107pairComm : Iso (a, b) (b, a)
84pairComm = MkIso swap swap swapSwap swapSwap
108pairComm = MkIso swap swap swapSwap swapSwap
@@ -113,6 +137,49 @@ pairBotLeft = MkIso fst FalseElim (\x => FalseElim x) (\y => FalseElim (fst y))
113pairBotRight : Iso (a, _|_) _|_
137pairBotRight : Iso (a, _|_) _|_
114pairBotRight = isoTrans pairComm pairBotLeft
138pairBotRight = isoTrans pairComm pairBotLeft
115
139
140+pairCong : Iso a a' -> Iso b b' -> Iso (a, b) (a', b')
141+pairCong {a = a} {a' = a'} {b = b} {b' = b'}
142+ (MkIso to from toFrom fromTo)
143+ (MkIso to' from' toFrom' fromTo') =
144+ MkIso to'' from'' iso1 iso2
145+ where to'' : (a, b) -> (a', b')
146+ to'' (x, y) = (to x, to' y)
147+ from'' : (a', b') -> (a, b)
148+ from'' (x, y) = (from x, from' y)
149+ iso1 : (x : (a', b')) -> to'' (from'' x) = x
150+ iso1 (x, y) = rewrite toFrom x in
151+ rewrite toFrom' y in
152+ refl
153+ iso2 : (x : (a, b)) -> from'' (to'' x) = x
154+ iso2 (x, y) = rewrite fromTo x in
155+ rewrite fromTo' y in
156+ refl
157+
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+
116
183
117-- Enable preorder reasoning syntax over isomorphisms
184-- Enable preorder reasoning syntax over isomorphisms
118qed : (a : Type) -> Iso a a
185qed : (a : Type) -> Iso a a
@@ -120,3 +187,104 @@ qed a = isoRefl
120
187
121step : (a : Type) -> Iso a b -> Iso b c -> Iso a c
188step : (a : Type) -> Iso a b -> Iso b c -> Iso a c
122step a iso1 iso2 = isoTrans iso1 iso2
189step a iso1 iso2 = isoTrans iso1 iso2
190+
191+
192+
193+-- Isomorphisms over Maybe
194+maybeCong : Iso a b -> Iso (Maybe a) (Maybe b)
195+maybeCong {a} {b} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2
196+ where ok1 : (y : Maybe b) -> map to (map from y) = y
197+ ok1 Nothing = refl
198+ ok1 (Just x) = (Just (to (from x))) ={ cong (toFrom x) }= (Just x) QED
199+ ok2 : (x : Maybe a) -> map from (map to x) = x
200+ ok2 Nothing = refl
201+ ok2 (Just x) = (Just (from (to x))) ={ cong (fromTo x) }= (Just x) QED
202+
203+maybeEither : Iso (Maybe a) (Either a ())
204+maybeEither = MkIso to from iso1 iso2
205+ where to : Maybe a -> Either a ()
206+ to Nothing = Right ()
207+ to (Just x) = Left x
208+ from : Either a () -> Maybe a
209+ from (Left x) = Just x
210+ from (Right ()) = Nothing
211+ iso1 : (x : Either a ()) -> to (from x) = x
212+ iso1 (Left x) = refl
213+ iso1 (Right ()) = refl
214+ iso2 : (y : Maybe a) -> from (to y) = y
215+ iso2 Nothing = refl
216+ iso2 (Just x) = refl
217+
218+maybeVoidUnit : Iso (Maybe _|_) ()
219+maybeVoidUnit = (Maybe _|_) ={ maybeEither }=
220+ (Either _|_ ()) ={ eitherBotLeft }=
221+ () QED
222+
223+eitherMaybeLeftMaybe : Iso (Either (Maybe a) b) (Maybe (Either a b))
224+eitherMaybeLeftMaybe {a} {b} =
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 }=
230+ (Maybe (Either a b)) QED
231+
232+
233+eitherMaybeRightMaybe : Iso (Either a (Maybe b)) (Maybe (Either a b))
234+eitherMaybeRightMaybe {a} {b} =
235+ (Either a (Maybe b)) ={ eitherComm }=
236+ (Either (Maybe b) a) ={ eitherMaybeLeftMaybe }=
237+ (Maybe (Either b a)) ={ maybeCong eitherComm }=
238+ (Maybe (Either a b)) QED
239+
240+
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
libs/prelude/Prelude/Fin.idr+8
@@ -38,6 +38,10 @@ weaken : Fin n -> Fin (S n)
38weaken fZ = fZ
38weaken fZ = fZ
39weaken (fS k) = fS (weaken k)
39weaken (fS k) = fS (weaken k)
40
40
41+weakenN : (n : Nat) -> Fin m -> Fin (m + n)
42+weakenN n fZ = fZ
43+weakenN n (fS f) = fS (weakenN n f)
44+
41strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
45strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
42strengthen {n = S k} fZ = Right fZ
46strengthen {n = S k} fZ = Right fZ
43strengthen {n = S k} (fS i) with (strengthen i)
47strengthen {n = S k} (fS i) with (strengthen i)
@@ -45,6 +49,10 @@ strengthen {n = S k} (fS i) with (strengthen i)
45 strengthen (fS k) | Right x = Right (fS x)
49 strengthen (fS k) | Right x = Right (fS x)
46strengthen f = Left f
50strengthen f = Left f
47
51
52+shift : (m : Nat) -> Fin n -> Fin (m + n)
53+shift Z f = f
54+shift {n=n} (S m) f = fS {k = (m + n)} (shift m f)
55+
48last : Fin (S n)
56last : Fin (S n)
49last {n=Z} = fZ
57last {n=Z} = fZ
50last {n=S _} = fS last
58last {n=S _} = fS last