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
|
module Data.Setoid.Product
import Data.List.Elem
import public Data.Product
import Data.Setoid.Indexed
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
pwEqImpliesEqual : Pointwise (\_ => Equal) xs ys -> xs = ys
pwEqImpliesEqual [] = Refl
pwEqImpliesEqual (r :: rs) = trans
(sym $ consHeadTail _)
(trans (cong2 (::) r (pwEqImpliesEqual rs)) (consHeadTail _))
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)
pwRefl : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
-> ((i : a) -> (u : x i) -> rel i u u)
-> {is : List a} -> (xs : x ^ is) -> Pointwise rel xs xs
pwRefl refl [] = []
pwRefl refl (x :: xs) = refl _ x :: pwRefl refl xs
pwSym : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
-> ((i : a) -> (u, v : x i) -> rel i u v -> rel i v u)
-> {is : List a} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel ys xs
pwSym sym [] = []
pwSym sym (r :: rs) = sym _ _ _ r :: pwSym sym rs
pwTrans : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
-> ((i : a) -> (u, v, w : x i) -> rel i u v -> rel i v w -> rel i u w)
-> {is : List a} -> {xs, ys, zs : x ^ is}
-> Pointwise rel xs ys -> Pointwise rel ys zs -> Pointwise rel xs zs
pwTrans trans [] [] = []
pwTrans trans (r :: rs) (s :: ss) = trans _ _ _ _ r s :: pwTrans trans rs ss
public export
pwEquivalence : IndexedEquivalence a x -> IndexedEquivalence (List a) ((^) x)
pwEquivalence eq = MkIndexedEquivalence
{ relation = \_ => Pointwise eq.relation
, reflexive = \_ => pwRefl eq.reflexive
, symmetric = \_, _, _ => pwSym eq.symmetric
, transitive = \_, _, _, _ => pwTrans eq.transitive
}
public export
Product : IndexedSetoid a -> IndexedSetoid (List a)
Product x = MkIndexedSetoid ((^) x.U) (pwEquivalence x.equivalence)
-- Introductors and Eliminators
public export
mapIntro'' : forall x, y . {0 rel : (i : a) -> Rel (x i)} -> {0 rel' : (i : a) -> Rel (y i)}
-> {0 f, g : (i : a) -> x i -> y i}
-> (cong : (i : a) -> (u, v : x i) -> rel i u v -> rel' i (f i u) (g i v))
-> {is : _} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel' (map f xs) (map g ys)
mapIntro'' cong [] = []
mapIntro'' cong (r :: rs) = cong _ _ _ r :: mapIntro'' cong rs
public export
mapIntro' : forall x, y . {0 rel : (i : a) -> Rel (x i)} -> {0 rel' : (i : a) -> Rel (y i)}
-> {0 f, g : (i : a) -> x i -> y i}
-> (cong : (i : a) -> {u, v : x i} -> rel i u v -> rel' i (f i u) (g i v))
-> {is : _} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel' (map f xs) (map g ys)
mapIntro' cong = mapIntro'' (\t, _, _ => cong t)
public export
mapIntro : (f : x ~> y) -> {is : _} -> {xs, ys : x.U ^ is}
-> Pointwise x.equivalence.relation xs ys
-> Pointwise y.equivalence.relation (map f.H xs) (map f.H ys)
mapIntro f = mapIntro' f.homomorphic
public export
wrapIntro : forall f . {0 rel : (i : a) -> Rel (x i)} -> {0 xs, ys : (x . f) ^ is}
-> Pointwise (\i => rel (f i)) xs ys -> Pointwise rel (wrap f xs) (wrap f ys)
wrapIntro [] = []
wrapIntro (r :: rs) = r :: wrapIntro rs
public export
wrapFunc : (0 x : IndexedSetoid b) -> (0 f : a -> b)
-> Product (reindex f x) ~> reindex (map f) (Product x)
wrapFunc x f = MkIndexedSetoidHomomorphism (\_ => wrap f) (\_, _, _ => wrapIntro)
public export
unwrapIntro : forall f . {0 rel : (i : b) -> Rel (x i)} -> {is : _} -> {0 xs, ys : x ^ map f is}
-> Pointwise rel xs ys -> Pointwise (\i => rel (f i)) {is = is} (unwrap f xs) (unwrap f ys)
unwrapIntro {is = []} [] = []
unwrapIntro {is = (i :: is)} (r :: rs) = r :: unwrapIntro rs
|
