0 | ||| Utility for describing chains of values linked via
  1 | ||| a transitive relation.
  2 | module Control.Relation.ReflexiveClosure
  3 |
  4 | import public Control.Order
  5 | import public Control.Relation
  6 |
  7 | %default total
  8 |
  9 | ||| The reflexive closure of a (typically transitive) relation.
 10 | |||
 11 | ||| This converts a transitive relation into a preorder.
 12 | ||| For instance, if `(<)` is a transitive relation over the integers,
 13 | ||| `ReflexiveClosure (<)` (corresponding to `(<=)` is a transitive,
 14 | ||| reflexive relation over the integers.
 15 | public export
 16 | data ReflexiveClosure : (rel : a -> a -> Type) -> (x,y : a) -> Type where
 17 |   Rel  : {0 rel : _} -> (0 prf : rel x y) -> ReflexiveClosure rel x y
 18 |   Refl : {0 rel : _} -> ReflexiveClosure rel x x
 19 |
 20 | public export
 21 | Reflexive a (ReflexiveClosure rel) where
 22 |   reflexive = Refl
 23 |
 24 | public export
 25 | Transitive a rel => Transitive a (ReflexiveClosure rel) where
 26 |   transitive (Rel x) (Rel y) = Rel $ transitive x y
 27 |   transitive (Rel x) Refl    = Rel x
 28 |   transitive Refl    y       = y
 29 |
 30 | public export
 31 | fromEq : {0 rel : _} -> (0 p : x === y) -> ReflexiveClosure rel x y
 32 | fromEq Refl = Refl
 33 |
 34 | --------------------------------------------------------------------------------
 35 | --          Transitivities
 36 | --------------------------------------------------------------------------------
 37 |
 38 | public export
 39 | 0 strictLeft : Transitive a rel => rel x y -> ReflexiveClosure rel y z -> rel x z
 40 | strictLeft w (Rel prf) = transitive w prf
 41 | strictLeft w Refl      = w
 42 |
 43 | public export
 44 | 0 strictRight : Transitive a rel => ReflexiveClosure rel x y -> rel y z -> rel x z
 45 | strictRight (Rel prf) w = transitive prf w
 46 | strictRight Refl      w = w
 47 |
 48 | --------------------------------------------------------------------------------
 49 | --          Transitive Chain
 50 | --------------------------------------------------------------------------------
 51 |
 52 | ||| A chain of values, linke by relation `ReflexiveClosure rel`.
 53 | public export
 54 | data Chain : (rel : a -> a -> Type) -> (x,y : a) -> Type where
 55 |   Nil  : {0 rel : a -> a -> Type} -> Chain rel x x
 56 |   (::) :
 57 |        {0 rel : a -> a -> Type}
 58 |     -> (0 x : a)
 59 |     -> (c : Chain rel y z)
 60 |     -> {auto 0 p : ReflexiveClosure rel x y}
 61 |     -> Chain rel x z
 62 |
 63 | ||| Witness that at least one link in a chain of values
 64 | ||| linked via `ReflexiveClosure rel` is string, and
 65 | ||| therefore (if `rel` is transitive), `rel x y` holds.
 66 | |||
 67 | ||| For instance, assume `rel` is `(<)` over the integers.
 68 | ||| Then `ReflexiveClosure rel` corresponds to `(<=)`.
 69 | ||| If we have the chain `w <= x <= y <= z` and we can
 70 | ||| show that one of the inequalities is strict (for instance,
 71 | ||| that `y < z`), then we can not only show that `w <= z` but
 72 | ||| that `w < z`.
 73 | public export
 74 | data IsStrict : {rel : _} -> Chain rel x y -> Type where
 75 |   Here  : IsStrict ((::) x c @{Rel p})
 76 |   There : IsStrict c -> IsStrict ((::) x c @{p})
 77 |
 78 | ||| If `x` and `y` are linked via a preorder `rel` over a chain
 79 | ||| of values, then `rel x y` holds.
 80 | public export
 81 | 0 chain : Preorder a rel => Chain rel x y -> rel x y
 82 | chain []                  = reflexive
 83 | chain ((::) _ c @{Rel x}) = transitive x (chain c)
 84 | chain ((::) _ c @{Refl})  = chain c
 85 |
 86 | ||| If `x` and `y` are linked via `ReflexiveClosure rel` for a transitive
 87 | ||| relation `rel` over a chain of values, then `ReflexiveClosure rel x y` holds.
 88 | public export
 89 | 0 weak : Transitive a rel => Chain rel x y -> ReflexiveClosure rel x y
 90 | weak []              = Refl
 91 | weak ((::) _ c @{p}) = transitive p $ weak c
 92 |
 93 | ||| If `x` and `y` are linked via `ReflexiveClosure rel` for a transitive
 94 | ||| relation `rel` over a chain of values, and at least one link ist
 95 | ||| strict, the `rel x y` holds.
 96 | public export
 97 | 0 strict :
 98 |      {auto _ : Transitive a rel}
 99 |   -> (c : Chain rel x y)
100 |   -> {auto p : IsStrict c}
101 |   -> rel x y
102 | strict ((::) _ c @{Rel q}) {p = Here}    = strictLeft q $ weak c
103 | strict ((::) _ c @{Rel q}) {p = There _} = transitive q $ strict c
104 | strict ((::) _ c @{Refl})  {p = There _} = strict c
105 |