0 | ||| An order is a particular kind of binary relation. The order
  1 | ||| relation is intended to proceed in some direction, though not
  2 | ||| necessarily with a unique path.
  3 | |||
  4 | ||| Orders are often defined simply as bundles of binary relation
  5 | ||| properties.
  6 | |||
  7 | ||| A prominent example of an order relation is LTE over Nat.
  8 |
  9 | module Control.Order
 10 |
 11 | import Control.Relation
 12 |
 13 | ||| A preorder is reflexive and transitive.
 14 | public export
 15 | interface (Reflexive ty rel, Transitive ty rel) => Preorder ty rel where
 16 |
 17 | ||| A partial order is an antisymmetrics preorder.
 18 | public export
 19 | interface (Preorder ty rel, Antisymmetric ty rel) => PartialOrder ty rel where
 20 |
 21 | ||| A relation is connex if for any two distinct x and y, either x ~ y or y ~ x.
 22 | |||
 23 | ||| This can also be stated as a trichotomy: x ~ y or x = y or y ~ x.
 24 | public export
 25 | interface Connex ty rel where
 26 |   connex : {x, y : ty} -> Not (x = y) -> Either (rel x y) (rel y x)
 27 |
 28 | ||| A relation is strongly connex if for any two x and y, either x ~ y or y ~ x.
 29 | public export
 30 | interface StronglyConnex ty rel where
 31 |   order : (x, y : ty) -> Either (rel x y) (rel y x)
 32 |
 33 | ||| A linear order is a connex partial order.
 34 | public export
 35 | interface (PartialOrder ty rel, Connex ty rel) => LinearOrder ty rel where
 36 |
 37 | ----------------------------------------
 38 |
 39 | ||| Every equivalence relation is a preorder.
 40 | public export
 41 | [EP] Equivalence ty rel => Preorder ty rel where
 42 |
 43 | --- Derivaties of order-based stuff ---
 44 |
 45 | ||| Gives the leftmost of a strongly connex relation among the given two elements, generalisation of `min`.
 46 | |||
 47 | ||| That is, leftmost x y ~ x and leftmost x y ~ y, and `leftmost x y` is either `x` or `y`
 48 | public export
 49 | leftmost : (0 rel : _) -> StronglyConnex ty rel => ty -> ty -> ty
 50 | leftmost rel x y = either (const x) (const y) $ order {rel} x y
 51 |
 52 | ||| Gives the rightmost of a strongly connex relation among the given two elements, generalisation of `max`.
 53 | |||
 54 | ||| That is, x ~ rightmost x y and y ~ rightmost x y, and `rightmost x y` is either `x` or `y`
 55 | public export
 56 | rightmost : (0 rel : _) -> StronglyConnex ty rel => ty -> ty -> ty
 57 | rightmost rel x y = either (const y) (const x) $ order {rel} x y
 58 |
 59 | -- properties --
 60 |
 61 | export
 62 | leftmostRelL : (0 rel : _) -> Reflexive ty rel => StronglyConnex ty rel => (x, y : ty) -> leftmost rel x y `rel` x
 63 | leftmostRelL rel x y with (order {rel} x y)
 64 |   _ | Left  _  = reflexive {rel}
 65 |   _ | Right yx = yx
 66 |
 67 | export
 68 | leftmostRelR : (0 rel : _) -> Reflexive ty rel => StronglyConnex ty rel => (x, y : ty) -> leftmost rel x y `rel` y
 69 | leftmostRelR rel x y with (order {rel} x y)
 70 |   _ | Left  xy = xy
 71 |   _ | Right _  = reflexive {rel}
 72 |
 73 | export
 74 | leftmostPreserves : (0 rel : _) -> StronglyConnex ty rel => (x, y : ty) -> Either (leftmost rel x y = x) (leftmost rel x y = y)
 75 | leftmostPreserves rel x y with (order {rel} x y)
 76 |   _ | Left  _ = Left  Refl
 77 |   _ | Right _ = Right Refl
 78 |
 79 | export
 80 | leftmostIsRightmostLeft : (0 rel : _) -> StronglyConnex ty rel =>
 81 |                           (x, y : ty) ->
 82 |                           (z : ty) -> (z `rel` x) -> (z `rel` y) ->
 83 |                           (z `rel` leftmost rel x y)
 84 | leftmostIsRightmostLeft rel x y z zx zy with (order {rel} x y)
 85 |   _ | Left  _ = zx
 86 |   _ | Right _ = zy
 87 |
 88 | export
 89 | rightmostRelL : (0 rel : _) -> Reflexive ty rel => StronglyConnex ty rel => (x, y : ty) -> x `rel` rightmost rel x y
 90 | rightmostRelL rel x y with (order {rel} x y)
 91 |   _ | Left  xy = xy
 92 |   _ | Right _  = reflexive {rel}
 93 |
 94 | export
 95 | rightmostRelR : (0 rel : _) -> Reflexive ty rel => StronglyConnex ty rel => (x, y : ty) -> y `rel` rightmost rel x y
 96 | rightmostRelR rel x y with (order {rel} x y)
 97 |   _ | Left  _  = reflexive {rel}
 98 |   _ | Right yx = yx
 99 |
100 | export
101 | rightmostPreserves : (0 rel : _) -> StronglyConnex ty rel => (x, y : ty) -> Either (rightmost rel x y = x) (rightmost rel x y = y)
102 | rightmostPreserves rel x y with (order {rel} x y)
103 |   _ | Left  _ = Right Refl
104 |   _ | Right _ = Left  Refl
105 |
106 | export
107 | rightmostIsLeftmostRight : (0 rel : _) -> StronglyConnex ty rel =>
108 |                            (x, y : ty) ->
109 |                            (z : ty) -> (x `rel` z) -> (y `rel` z) ->
110 |                            (leftmost rel x y `rel` z)
111 | rightmostIsLeftmostRight rel x y z zx zy with (order {rel} x y)
112 |   _ | Left  _ = zx
113 |   _ | Right _ = zy
114 |