blob: 28076c511155468cbe8ca6a48b0b7c5f27e9e5d8 (
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
|
||| The setoid of vectors over a given setoid, defined inductively
module Data.Setoid.Vect.Inductive
import Data.Setoid.Definition
import Data.Vect
import Data.HVect
import Data.Vect.Properties
%default total
public export
data (.VectEquality) : (a : Setoid) -> Rel (Vect n (U a)) where
Nil : a.VectEquality [] []
(::) : (hdEq : a.equivalence.relation x y) ->
(tlEq : a.VectEquality xs ys) ->
a.VectEquality (x :: xs) (y :: ys)
export
(++) : a.VectEquality xs ys -> a.VectEquality as bs ->
a.VectEquality (xs ++ as) (ys ++ bs)
[] ++ qs = qs
(p :: ps) ++ qs = p :: (ps ++ qs)
public export
(.VectEqualityReflexive) : (a : Setoid) -> (xs : Vect n $ U a) -> a.VectEquality xs xs
a.VectEqualityReflexive [] = []
a.VectEqualityReflexive (x :: xs) = a.equivalence.reflexive x :: a.VectEqualityReflexive xs
public export
(.VectEqualitySymmetric) : (a : Setoid) -> (xs,ys : Vect n $ U a) -> (prf : a.VectEquality xs ys) ->
a.VectEquality ys xs
a.VectEqualitySymmetric [] [] [] = []
a.VectEqualitySymmetric (x :: xs) (y :: ys) (hdEq :: tlEq)
= a.equivalence.symmetric x y hdEq :: a.VectEqualitySymmetric xs ys tlEq
public export
(.VectEqualityTransitive) : (a : Setoid) -> (xs,ys,zs : Vect n $ U a) ->
(prf1 : a.VectEquality xs ys) -> (prf2 : a.VectEquality ys zs) ->
a.VectEquality xs zs
a.VectEqualityTransitive [] [] [] [] [] = []
a.VectEqualityTransitive (x :: xs) (y :: ys) (z :: zs) (hdEq1 :: tlEq1) (hdEq2 :: tlEq2)
= a.equivalence.transitive x y z hdEq1 hdEq2 ::
a.VectEqualityTransitive xs ys zs tlEq1 tlEq2
public export
VectSetoid : (n : Nat) -> (a : Setoid) -> Setoid
VectSetoid n a = MkSetoid (Vect n (U a))
$ MkEquivalence
{ relation = a.VectEquality
, reflexive = a.VectEqualityReflexive
, symmetric = a.VectEqualitySymmetric
, transitive = a.VectEqualityTransitive
}
public export
VectMapFunctionHomomorphism : (f : a ~> b) ->
SetoidHomomorphism (VectSetoid n a) (VectSetoid n b) (map f.H)
VectMapFunctionHomomorphism f [] [] [] = []
VectMapFunctionHomomorphism f (x :: xs) (y :: ys) (hdEq :: tlEq) =
f.homomorphic x y hdEq :: VectMapFunctionHomomorphism f xs ys tlEq
public export
VectMapHomomorphism : (f : a ~> b) -> (VectSetoid n a ~> VectSetoid n b)
VectMapHomomorphism f = MkSetoidHomomorphism (map f.H) (VectMapFunctionHomomorphism f)
public export
VectMapIsHomomorphism : SetoidHomomorphism (a ~~> b) (VectSetoid n a ~~> VectSetoid n b)
VectMapHomomorphism
VectMapIsHomomorphism f g f_eq_g [] = []
VectMapIsHomomorphism f g f_eq_g (x :: xs) = f_eq_g x :: VectMapIsHomomorphism f g f_eq_g xs
public export
VectMap : {0 a, b : Setoid} -> (a ~~> b) ~> (VectSetoid n a ~~> VectSetoid n b)
VectMap = MkSetoidHomomorphism
{ H = VectMapHomomorphism
, homomorphic = VectMapIsHomomorphism
}
|
