blob: f92c23cfb7e0353437166e9af3b930b75271f5f1 (
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
|
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
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
|
