0 | ||| An strict preorder (sometimes known as a quasi-order, or an
 1 | ||| ordering) is what you get when you remove the diagonal `{(a,b) | a
 2 | ||| r b , b r a}` from a preorder. For example a < b is an ordering.
 3 | ||| This module extends base's Control.Order with the strict versions.
 4 | ||| The interface system seems to struggle a bit with some of the constructions,
 5 | ||| so I hacked them a bit. Sorry.
 6 | module Decidable.Order.Strict
 7 |
 8 | import Control.Relation
 9 | import Control.Order
10 | import Decidable.Equality
11 |
12 | %default total
13 |
14 | public export
15 | interface Irreflexive ty rel where
16 |   irreflexive : {x : ty} -> Not (rel x x)
17 |
18 | public export
19 | interface (Transitive ty rel, Irreflexive ty rel) => StrictPreorder  ty rel where
20 |
21 | public export
22 | interface Asymmetric ty rel where
23 |   asymmetric : {x, y : ty} -> rel x y -> Not (rel y x)
24 |
25 | public export
26 | [SPA] StrictPreorder ty rel => Asymmetric ty rel where
27 |   asymmetric xy yx = irreflexive {rel} $ transitive xy yx
28 |
29 | -- We make this completion a record type so that we do not need to name the
30 | -- interface implementations for fear of them interfering with other
31 | -- `Either`-based constructions.
32 |
33 | public export
34 | record EqOr {0 t : Type} (spo : Rel t) (a, b : t) where
35 |   constructor MkEqOr
36 |   runEqOr : Either (a = b) (a `spo` b)
37 |
38 | public export
39 | Transitive ty rel => Transitive ty (EqOr rel) where
40 |
41 |   transitive (MkEqOr (Left  Refl)) bLTEc                 = bLTEc
42 |   transitive aLTEb                 (MkEqOr (Left  Refl)) = aLTEb
43 |   transitive (MkEqOr (Right aLTb)) (MkEqOr (Right bLTc))
44 |     = MkEqOr $ Right $ transitive aLTb bLTc
45 |
46 | public export
47 | Reflexive ty (EqOr rel) where
48 |   reflexive = MkEqOr $ Left Refl
49 |
50 | public export
51 | Transitive ty rel => Preorder ty (EqOr rel) where
52 |
53 | public export
54 | (Irreflexive ty rel, Asymmetric ty rel) => Antisymmetric ty (EqOr rel) where
55 |
56 |   antisymmetric (MkEqOr p) (MkEqOr q) = go p q where
57 |
58 |     go : {a, b : ty} ->
59 |          Either (a = b) (a `rel` b) ->
60 |          Either (b = a) (b `rel` a) ->
61 |          a = b
62 |     go (Left  Refl) (Left  Refl) = Refl
63 |     go (Left  Refl) (Right bLTa) = absurd (irreflexive {rel} bLTa)
64 |     go (Right aLTb) (Left  Refl) = absurd (irreflexive {rel} aLTb)
65 |     go (Right aLTb) (Right bLTa) = absurd (asymmetric {rel} aLTb bLTa)
66 |
67 | public export
68 | (Irreflexive ty rel, Asymmetric ty rel, Transitive ty rel) =>
69 |   PartialOrder ty (EqOr rel) where
70 |
71 | public export
72 | data DecOrdering : {lt : t -> t -> Type} -> (a,b : t) -> Type where
73 |   DecLT : forall lt . (a `lt` b) -> DecOrdering {lt = lt} a b
74 |   DecEQ : forall lt . (a  =   b) -> DecOrdering {lt = lt} a b
75 |   DecGT : forall lt . (b `lt` a) -> DecOrdering {lt = lt} a b
76 |
77 | public export
78 | interface StrictPreorder t spo => StrictOrdered t spo where
79 |   order : (a,b : t) -> DecOrdering {lt = spo} a b
80 |
81 | public export
82 | Connex ty rel => Connex ty (EqOr rel) where
83 |   connex neq = bimap (MkEqOr . Right) (MkEqOr . Right) (connex neq)
84 |
85 | public export
86 | (Connex ty rel, DecEq ty) => StronglyConnex ty (EqOr rel) where
87 |   order a b = case decEq a b of
88 |     Yes eq => Left $ MkEqOr (Left eq)
89 |     No neq => connex neq
90 |