0 | module Control.Relation.Closure
 1 |
 2 | import Control.Relation
 3 |
 4 | %default total
 5 |
 6 | public export
 7 | data SymClosure : Rel ty -> ty -> ty -> Type where
 8 |   Fwd : {0 x, y : ty} -> rel x y -> SymClosure rel x y
 9 |   Bwd : {0 x, y : ty} -> rel y x -> SymClosure rel x y
10 |
11 | public export
12 | Reflexive ty rel => Reflexive ty (SymClosure rel) where
13 |   reflexive = Fwd reflexive
14 |
15 | public export
16 | Symmetric ty (SymClosure rel) where
17 |   symmetric (Fwd xy) = Bwd xy
18 |   symmetric (Bwd yx) = Fwd yx
19 |
20 | ----------------------------------------
21 |
22 | public export
23 | data TransClosure : Rel ty -> ty -> ty -> Type where
24 |   Nil  : TransClosure rel x x
25 |   (::) : {y : ty} -> rel x y -> TransClosure rel y z -> TransClosure rel x z
26 |
27 | public export
28 | Reflexive ty (TransClosure rel) where
29 |   reflexive = []
30 |
31 | public export
32 | Symmetric ty rel => Symmetric ty (TransClosure rel) where
33 |   symmetric {x} {y} xy = reverseOnto [] xy
34 |     where
35 |       reverseOnto : {z : ty} ->
36 |                     TransClosure rel z x ->
37 |                     TransClosure rel z y ->
38 |                     TransClosure rel y x
39 |       reverseOnto zx [] = zx
40 |       reverseOnto zx (zw :: wy) = reverseOnto (symmetric zw :: zx) wy
41 |
42 | public export
43 | Transitive ty (TransClosure rel) where
44 |   transitive [] yz = yz
45 |   transitive (xw :: wy) yz = xw :: transitive wy yz
46 |
47 | public export
48 | Symmetric ty rel => Euclidean ty (TransClosure rel) where
49 |   euclidean = euclidean @{TSE}
50 |
51 | public export
52 | Symmetric ty rel => Tolerance ty (TransClosure rel) where
53 |
54 | public export
55 | Symmetric ty rel => PartialEquivalence ty (TransClosure rel) where
56 |
57 | public export
58 | Symmetric ty rel => Equivalence ty (TransClosure rel) where
59 |