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
|
||| The setoid of vectors over a given setoid, defined using a function
module Data.Setoid.Vect.Functional
import Data.Setoid.Definition
import Data.Vect
import Data.HVect
import Data.Vect.Properties
import Data.Setoid.Vect.Inductive
import Control.Order
import Syntax.PreorderReasoning.Setoid
%default total
public export
0 (.VectEquality) : (a : Setoid) -> Rel (Vect n (U a))
a.VectEquality xs ys = (i : Fin n) ->
a.equivalence.relation (index i xs) (index i ys)
-- Not using the more sensible type definition
-- Inductive.(.VectEquality) a xs ys -> Functional.(.VectEquality) a xs ys
-- so that the arguments are in the order as Vect's index.
export
index : (i : Fin n) ->
Inductive.(.VectEquality) a xs ys ->
a.equivalence.relation (index i xs) (index i ys)
index FZ (hdEq :: _) = hdEq
index (FS k) (_ :: tlEq) = index k tlEq
%hide Inductive.(.VectEquality)
%hide Inductive.VectSetoid
public export
VectSetoid : (n : Nat) -> (a : Setoid) -> Setoid
VectSetoid n a = MkSetoid (Vect n (U a))
$ MkEquivalence
{ relation = (.VectEquality) a
, reflexive = \xs , i =>
a.equivalence.reflexive _
, symmetric = \xs,ys, prf , i =>
a.equivalence.symmetric _ _ (prf i)
, transitive = \xs, ys, zs, prf1, prf2, i =>
a.equivalence.transitive _ _ _ (prf1 i) (prf2 i)
}
public export
VectMap : {a, b : Setoid} -> (a ~~> b) ~>
(VectSetoid n a ~~> VectSetoid n b)
VectMap = MkSetoidHomomorphism
(\f => MkSetoidHomomorphism
(\xs => map f.H xs)
$ \xs, ys, prf, i => CalcWith b $
|~ index i (map f.H xs)
~~ f.H (index i xs)
.=.(indexNaturality _ _ _)
~~ f.H (index i ys) ...(f.homomorphic _ _ $ prf i)
~~ index i (map f.H ys)
.=<(indexNaturality _ _ _))
$ \f,g,prf,xs,i => CalcWith b $
|~ index i (map f.H xs)
~~ f.H (index i xs) .=.(indexNaturality _ _ _)
~~ g.H (index i xs) ...(prf _)
~~ index i (map g.H xs) .=<(indexNaturality _ _ _)
|
