0 | ||| A binary relation is a function of type (ty -> ty -> Type).
  1 | |||
  2 | ||| A prominent example of a binary relation is LTE over Nat.
  3 | |||
  4 | ||| This module defines some interfaces for describing properties of
  5 | ||| binary relations. It also proves somes relations among relations.
  6 |
  7 | module Control.Relation
  8 |
  9 | %default total
 10 |
 11 | ||| A relation on ty is a type indexed by two ty values
 12 | public export
 13 | Rel : Type -> Type
 14 | Rel ty = ty -> ty -> Type
 15 |
 16 | ||| A relation is reflexive if x ~ x for every x.
 17 | public export
 18 | interface Reflexive ty rel | rel where
 19 |   constructor MkReflexive
 20 |   reflexive : {x : ty} -> rel x x
 21 |
 22 | ||| A relation is transitive if x ~ z when x ~ y and y ~ z.
 23 | public export
 24 | interface Transitive ty rel | rel where
 25 |   constructor MkTransitive
 26 |   transitive : {x, y, z : ty} -> rel x y -> rel y z -> rel x z
 27 |
 28 | ||| A relation is symmetric if y ~ x when x ~ y.
 29 | public export
 30 | interface Symmetric ty rel | rel where
 31 |   constructor MkSymmetric
 32 |   symmetric : {x, y : ty} -> rel x y -> rel y x
 33 |
 34 | ||| A relation is antisymmetric if no two distinct elements bear the relation to each other.
 35 | public export
 36 | interface Antisymmetric ty rel | rel where
 37 |   constructor MkAntisymmetric
 38 |   antisymmetric : {x, y : ty} -> rel x y -> rel y x -> x = y
 39 |
 40 | ||| A relation is dense if when x ~ y there is z such that x ~ z and z ~ y.
 41 | public export
 42 | interface Dense ty rel | rel where
 43 |   constructor MkDense
 44 |   dense : {x, y : ty} -> rel x y -> (z : ty ** (rel x z, rel z y))
 45 |
 46 | ||| A relation is serial if for all x there is a y such that x ~ y.
 47 | public export
 48 | interface Serial ty rel | rel where
 49 |   constructor MkSerial
 50 |   serial : {x : ty} -> (y : ty ** rel x y)
 51 |
 52 | ||| A relation is euclidean if y ~ z when x ~ y and x ~ z.
 53 | public export
 54 | interface Euclidean ty rel | rel where
 55 |   constructor MkEuclidean
 56 |   euclidean : {x, y, z : ty} -> rel x y -> rel x z -> rel y z
 57 |
 58 | ||| A tolerance relation is reflexive and symmetric.
 59 | public export
 60 | interface (Reflexive ty rel, Symmetric ty rel) => Tolerance ty rel | rel where
 61 |
 62 | ||| A partial equivalence is transitive and symmetric.
 63 | public export
 64 | interface (Transitive ty rel, Symmetric ty rel) => PartialEquivalence ty rel | rel where
 65 |
 66 | ||| An equivalence relation is transitive, symmetric, and reflexive.
 67 | public export
 68 | interface (Reflexive ty rel, Transitive ty rel, Symmetric ty rel) => Equivalence ty rel | rel where
 69 |
 70 | ----------------------------------------
 71 |
 72 | ||| Every reflexive relation is dense.
 73 | public export
 74 | Reflexive ty rel => Dense ty rel where
 75 |   dense xy = (x ** (reflexive, xy))
 76 |
 77 | ||| Every reflexive relation is serial.
 78 | public export
 79 | Reflexive ty rel => Serial ty rel where
 80 |   serial = (x ** reflexive)
 81 |
 82 | ||| A transitive symmetric serial relation is reflexive.
 83 | public export
 84 | (Transitive ty rel, Symmetric ty rel, Serial ty rel) => Reflexive ty rel where
 85 |   reflexive = let (y ** xy) = serial in transitive xy $ symmetric xy
 86 |
 87 | ||| A reflexive euclidean relation is symmetric.
 88 | public export
 89 | [RES] (Reflexive ty rel, Euclidean ty rel) => Symmetric ty rel where
 90 |   symmetric xy = euclidean xy $ reflexive
 91 |
 92 | ||| A reflexive euclidean relation is transitive.
 93 | public export
 94 | [RET] (Reflexive ty rel, Euclidean ty rel) =>
 95 |       Transitive ty rel using RES where
 96 |   transitive xy yz = symmetric $ euclidean yz $ symmetric xy
 97 |
 98 | ||| A transitive symmetrics relation is euclidean.
 99 | public export
100 | [TSE] (Transitive ty rel, Symmetric ty rel) => Euclidean ty rel where
101 |   euclidean xy xz = transitive (symmetric xy) xz
102 |
103 | ----------------------------------------
104 |
105 | public export
106 | Reflexive ty Equal where
107 |   reflexive = Refl
108 |
109 | public export
110 | Symmetric ty Equal where
111 |   symmetric xy = sym xy
112 |
113 | public export
114 | Transitive ty Equal where
115 |   transitive xy yz = trans xy yz
116 |
117 | public export
118 | Euclidean ty Equal where
119 |   euclidean = euclidean @{TSE}
120 |
121 | public export
122 | Tolerance ty Equal where
123 |
124 | public export
125 | PartialEquivalence ty Equal where
126 |
127 | public export
128 | Equivalence ty Equal where
129 |