0 | ||| Reflexive closure of a (binary) relation.  Internally used instead of Maybe, to maintain continuity of indexs.
 1 | module TypeAligned.ZeroOne
 2 |
 3 | import Control.Relation
 4 | import Data.Linear.Notation
 5 |
 6 | %default total
 7 |
 8 | ||| Reflexive closure of a relation
 9 | public export
10 | data ZeroOne : Rel a -> a -> a -> Type where
11 |   Zero : (0 eqxy : x = y) -> ZeroOne p x y
12 |   One : {0 p : a -> a -> Type} -> p x y -@ ZeroOne p x y
13 |
14 | ||| Convenience constructor
15 | export
16 | ZeroEq : ZeroOne p x x
17 | ZeroEq = Zero Refl
18 |
19 | ||| Unrestricted 'One'
20 | export
21 | singleton : {0 p : Rel a} -> p x y -> ZeroOne p x y
22 | singleton xy = One xy
23 |
24 | parameters {0 p : Rel a}
25 |   parameters {0 f : a -> b} {0 q : Rel b}
26 |     parameters (pq : {0 x, y : a} -> p x y -@ q (f x) (f y))
27 |       ||| Linear 'mapReduceL'
28 |       export
29 |       mapReduceLOnce : q (f x) (f x) -> ZeroOne p x y -@ q (f x) (f y)
30 |       mapReduceLOnce qx (Zero Refl) = qx
31 |       mapReduceLOnce  _ (One xy) = pq xy
32 |
33 |       ||| Linear 'mapReduceR'
34 |       export
35 |       mapReduceROnce : q (f y) (f y) -> ZeroOne p x y -@ q (f x) (f y)
36 |       mapReduceROnce qy (Zero Refl) = qy
37 |       mapReduceROnce  _ (One xy) = pq xy
38 |
39 |       ||| Linear 'map'
40 |       export
41 |       mapOnce : ZeroOne p x y -@ ZeroOne q (f x) (f y)
42 |       mapOnce (Zero eq) = Zero (cong f eq)
43 |       mapOnce (One xy) = One (pq xy)
44 |
45 |     parameters (pq : {0 x, y : a} -> p x y -> q (f x) (f y))
46 |       ||| Reduce to left index, while changing relation
47 |       export
48 |       mapReduceL : q (f x) (f x) -> ZeroOne p x y -> q (f x) (f y)
49 |       mapReduceL qx (Zero Refl) = qx
50 |       mapReduceL  _ (One xy) = pq xy
51 |
52 |       ||| Reduce to right index, while changing relation
53 |       export
54 |       mapReduceR : q (f y) (f y) -> ZeroOne p x y -> q (f x) (f y)
55 |       mapReduceR qy (Zero Refl) = qy
56 |       mapReduceR  _ (One xy) = pq xy
57 |
58 |       ||| Change inner relation
59 |       export
60 |       map : ZeroOne p x y -> ZeroOne q (f x) (f y)
61 |       map (Zero eq) = Zero (cong f eq)
62 |       map (One xy) = One (pq xy)
63 |
64 |   parameters (px : p x x)
65 |     ||| Linear 'reduceL'
66 |     export
67 |     reduceLOnce : ZeroOne p x y -@ p x y
68 |     reduceLOnce (Zero Refl) = px
69 |     reduceLOnce (One pxy) = pxy
70 |
71 |     ||| Reduce to left index
72 |     export
73 |     reduceL : ZeroOne p x y -> p x y
74 |     reduceL zo = reduceLOnce zo
75 |
76 |   parameters (py : p y y)
77 |     ||| Linear 'reduceR'
78 |     export
79 |     reduceROnce : ZeroOne p x y -@ p x y
80 |     reduceROnce (Zero Refl) = py
81 |     reduceROnce (One pxy) = pxy
82 |
83 |     ||| Reduce to right index
84 |     export
85 |     reduceR : ZeroOne p x y -> p x y
86 |     reduceR zo = reduceROnce zo
87 |
88 | ||| Independent of the underlying relation, the reflexive closure is Reflexive.
89 | export
90 | Reflexive a (ZeroOne p) where
91 |   reflexive = ZeroEq
92 |