blob: cd69098cbb873ced8396d644c15b8c4cb7fffdb7 (
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
|
module Soat.Data.Product
import Control.Relation
import Data.List.Elem
%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
(++) : x ^ is -> x ^ js -> x ^ (is ++ js)
(++) [] ys = ys
(++) (x :: xs) ys = x :: (xs ++ ys)
-- 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)
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
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
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
|
