blob: b20523a0f3550930387efa893788cb24f1c68885 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
|
module Soat.Data.Product
import Control.Relation
import Data.List.Elem
import Soat.Relation
%default total
infix 10 ^
infix 5 ++
-- Definitions
public export
data (^) : (0 _ : a -> Type) -> List a -> Type where
Nil : x ^ []
(::) : {0 x : a -> Type} -> x i -> x ^ is -> x ^ (i :: is)
public export
ary : List Type -> Type -> Type
ary [] y = y
ary (x :: xs) y = x -> ary xs y
-- Conversions
public export
uncurry : map x is `ary` a -> x ^ is -> a
uncurry f [] = f
uncurry f (x :: xs) = uncurry (f x) xs
-- Destructors
public export
head : x ^ (i :: is) -> x i
head (x :: xs) = x
public export
tail : x ^ (i :: is) -> x ^ is
tail (x :: xs) = xs
public export
consHeadTail : (xs : x ^ (i :: is)) -> head xs :: tail xs = xs
consHeadTail (x :: xs) = Refl
public export
index : x ^ is -> Elem i is -> x i
index xs Here = head xs
index xs (There elem) = index (tail xs) elem
-- Constructors
public export
tabulate : {is : List a} -> ({i : a} -> Elem i is -> x i) -> x ^ is
tabulate {is = []} f = []
tabulate {is = (i :: is)} f = f Here :: tabulate (f . There)
public export
indexTabulate : forall x . (0 f : {i : a} -> Elem i is -> x i) -> (elem : Elem i is)
-> index (tabulate f) elem = f elem
indexTabulate f Here = Refl
indexTabulate f (There elem) = indexTabulate (f . There) elem
-- Operations
public export
map : (f : (i : a) -> x i -> y i) -> {is : List a} -> x ^ is -> y ^ is
map f [] = []
map f (x :: xs) = f _ x :: map f xs
public export
indexMap : {0 f : IFunc x y} -> (xs : x ^ is) -> (elem : Elem i is)
-> index (map f xs) elem = f i (index xs elem)
indexMap (x :: xs) Here = Refl
indexMap (x :: xs) (There elem) = indexMap xs elem
public export
mapId : (xs : x ^ is) -> map (\_ => Basics.id) xs = xs
mapId [] = Refl
mapId (x :: xs) = cong ((::) x) $ mapId xs
public export
mapComp : {0 f : IFunc y z} -> {0 g : IFunc x y} -> (xs : x ^ is)
-> map (\i => f i . g i) xs = map f (map g xs)
mapComp [] = Refl
mapComp (x :: xs) = cong ((::) (f _ (g _ x))) $ mapComp xs
public export
(++) : x ^ is -> x ^ js -> x ^ (is ++ js)
(++) [] ys = ys
(++) (x :: xs) ys = x :: (xs ++ ys)
public export
wrap : (0 f : a -> b) -> (x . f) ^ is -> x ^ map f is
wrap f [] = []
wrap f (x :: xs) = x :: wrap f xs
public export
mapWrap : {0 f : IFunc x y} -> (0 g : a -> b) -> (xs : (x . g) ^ is)
-> map f (wrap g xs) = wrap g (map (\i => f (g i)) xs)
mapWrap g [] = Refl
mapWrap g (x :: xs) = cong ((::) (f (g _) x)) $ mapWrap g xs
public export
unwrap : (0 f : a -> b) -> {is : _} -> x ^ map f is -> (x . f) ^ is
unwrap f {is = []} [] = []
unwrap f {is = (i :: is)} (x :: xs) = x :: unwrap f xs
public export
mapUnwrap : {0 f : IFunc x y} -> (0 g : a -> b) -> {is : _} -> (xs : x ^ map g is)
-> map (\i => f (g i)) {is} (unwrap g xs) = unwrap g {is} (map f xs)
mapUnwrap g {is = []} [] = Refl
mapUnwrap g {is = (i :: is)} (x :: xs) = cong (Product.(::) (f (g i) x)) $ mapUnwrap g xs
public export
unwrapWrap : (0 x : a -> Type) -> (xs : (x . f) ^ is) -> unwrap f (wrap {x} f xs) = xs
unwrapWrap u [] = Refl
unwrapWrap u (x :: xs) = cong ((::) x) $ unwrapWrap u xs
public export
wrapUnwrap : {is : _} -> (xs : x ^ map f is) -> wrap f {is} (unwrap f xs) = xs
wrapUnwrap {is = []} [] = Refl
wrapUnwrap {is = (i :: is)} (x :: xs) = cong ((::) x) $ wrapUnwrap xs
-- Relations
namespace Pointwise
public export
data Pointwise : (0 _ : (i : a) -> Rel (x i)) -> forall is . Rel (x ^ is) where
Nil : Pointwise rel [] []
(::) : forall b, x, y . {0 xs, ys : b ^ is} -> {0 rel : (i : a) -> Rel (b i)}
-> (r : rel i x y) -> (rs : Pointwise rel xs ys) -> Pointwise rel (x :: xs) (y :: ys)
-- Destructors
public export
index : Pointwise rel xs ys -> (elem : Elem i is) -> rel i (index xs elem) (index ys elem)
index (r :: rs) Here = r
index (r :: rs) (There elem) = index rs elem
-- Operators
public export
map : forall b . {0 r, s : (i : a) -> Rel (b i)}
-> ((i : a) -> {x, y : b i} -> r i x y -> s i x y)
-> {is : List a} -> {xs, ys : b ^ is} -> Pointwise r {is} xs ys -> Pointwise s {is} xs ys
map f [] = []
map f (r :: rs) = f _ r :: map f rs
-- Relational Properties
public export
pwEqImpliesEqual : Pointwise (\_ => Equal) xs ys -> xs = ys
pwEqImpliesEqual [] = Refl
pwEqImpliesEqual (r :: rs) = trans
(sym $ consHeadTail _)
(trans (cong2 (::) r (pwEqImpliesEqual rs)) (consHeadTail _))
public export
equalImpliesPwEq : {xs, ys : b ^ is} -> xs = ys -> Pointwise (\_ => Equal) xs ys
equalImpliesPwEq {xs = []} {ys = []} eq = []
equalImpliesPwEq {xs = (x :: xs)} {ys = (y :: ys)} eq =
cong head eq :: equalImpliesPwEq (cong tail eq)
-- FIXME: work out how to expose interfaces
public export
pwRefl : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
-> ((i : a) -> Reflexive (x i) (rel i))
-> {is : List a} -> {xs : x ^ is} -> Pointwise rel xs xs
pwRefl f {xs = []} = []
pwRefl f {xs = (x :: xs)} = reflexive :: pwRefl f
public export
pwReflexive : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
-> ((i : a) -> Reflexive (x i) (rel i))
-> {is : List a} -> {xs, ys : x ^ is} -> xs = ys -> Pointwise rel xs ys
pwReflexive refl Refl = pwRefl refl
public export
pwSym : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
-> ((i : a) -> Symmetric (x i) (rel i))
-> {is : List a} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel ys xs
pwSym f [] = []
pwSym f (r :: rs) = symmetric r :: pwSym f rs
public export
pwTrans : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
-> ((i : a) -> Transitive (x i) (rel i))
-> {is : List a} -> {xs, ys, zs : x ^ is}
-> Pointwise rel xs ys -> Pointwise rel ys zs -> Pointwise rel xs zs
pwTrans f [] [] = []
pwTrans f (r :: rs) (s :: ss) = transitive r s :: pwTrans f rs ss
|
