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
|
||| Setoid of lists over a setoid and associated definitions
module Data.Setoid.List
import Data.List
import Data.Setoid.Definition
%default total
namespace Relation
public export
data (.ListEquality) : (a : Setoid) -> Rel (List $ U a) where
Nil : a.ListEquality [] []
(::) : (hdEq : a.equivalence.relation x y) -> (tlEq : a.ListEquality xs ys) ->
a.ListEquality (x :: xs) (y :: ys)
public export
(.ListEqualityReflexive) : (a : Setoid) -> (xs : List $ U a) -> a.ListEquality xs xs
a.ListEqualityReflexive [] = []
a.ListEqualityReflexive (x :: xs) = a.equivalence.reflexive x :: a.ListEqualityReflexive xs
public export
(.ListEqualitySymmetric) : (a : Setoid) -> (xs,ys : List $ U a) -> (prf : a.ListEquality xs ys) ->
a.ListEquality ys xs
a.ListEqualitySymmetric [] [] [] = []
a.ListEqualitySymmetric (x :: xs) (y :: ys) (hdEq :: tlEq)
= a.equivalence.symmetric x y hdEq :: a.ListEqualitySymmetric xs ys tlEq
public export
(.ListEqualityTransitive) : (a : Setoid) -> (xs,ys,zs : List $ U a) ->
(prf1 : a.ListEquality xs ys) -> (prf2 : a.ListEquality ys zs) ->
a.ListEquality xs zs
a.ListEqualityTransitive [] [] [] [] [] = []
a.ListEqualityTransitive (x :: xs) (y :: ys) (z :: zs) (hdEq1 :: tlEq1) (hdEq2 :: tlEq2)
= a.equivalence.transitive x y z hdEq1 hdEq2 ::
a.ListEqualityTransitive xs ys zs tlEq1 tlEq2
public export
ListSetoid : (a : Setoid) -> Setoid
ListSetoid a = MkSetoid (List $ U a)
$ MkEquivalence
{ relation = a.ListEquality
, reflexive = a.ListEqualityReflexive
, symmetric = a.ListEqualitySymmetric
, transitive = a.ListEqualityTransitive
}
public export
ListMapFunctionHomomorphism : (f : a ~> b) ->
SetoidHomomorphism (ListSetoid a) (ListSetoid b) (map f.H)
ListMapFunctionHomomorphism f [] [] [] = []
ListMapFunctionHomomorphism f (x :: xs) (y :: ys) (hdEq :: tlEq) =
f.homomorphic x y hdEq :: ListMapFunctionHomomorphism f xs ys tlEq
public export
ListMapHomomorphism : (f : a ~> b) -> (ListSetoid a ~> ListSetoid b)
ListMapHomomorphism f = MkSetoidHomomorphism (map f.H) (ListMapFunctionHomomorphism f)
public export
ListMapIsHomomorphism : SetoidHomomorphism (a ~~> b) (ListSetoid a ~~> ListSetoid b)
ListMapHomomorphism
ListMapIsHomomorphism f g f_eq_g [] = []
ListMapIsHomomorphism f g f_eq_g (x :: xs) = f_eq_g x :: ListMapIsHomomorphism f g f_eq_g xs
public export
ListMap : {0 a, b : Setoid} -> (a ~~> b) ~> (ListSetoid a ~~> ListSetoid b)
ListMap = MkSetoidHomomorphism
{ H = ListMapHomomorphism
, homomorphic = ListMapIsHomomorphism
}
public export
reverseHomomorphic : {a : Setoid} -> (x, y : List (U a)) ->
(a.ListEquality x y) -> a.ListEquality (reverse x) (reverse y)
reverseHomomorphic x y prf = roh [] [] x y (a.ListEqualityReflexive _) prf
where roh : (ws, xs, ys, zs : List (U a)) -> a.ListEquality ws xs -> a.ListEquality ys zs ->
a.ListEquality (reverseOnto ws ys) (reverseOnto xs zs)
roh ws xs [] [] wx [] = wx
roh ws xs (y::ys) (z::zs) wx (yzh :: yzt) = roh (y::ws) (z::xs) ys zs (yzh :: wx) yzt
public export
appendCongruence : {a : Setoid} -> (x1, x2, y1, y2 : List (U a)) ->
a.ListEquality x1 y1 -> a.ListEquality x2 y2 -> a.ListEquality (x1 ++ x2) (y1 ++ y2)
appendCongruence [] x2 [] y2 [] p = p
appendCongruence (x::xs) x2 (y::ys) y2 (ph::pt) p = ph :: appendCongruence _ _ _ _ pt p
|
