0 | module Control.Relation.Trichotomy
  1 |
  2 | import Control.Relation.ReflexiveClosure
  3 | import Data.Either0
  4 |
  5 | %default total
  6 |
  7 | ||| Trichotomy formalises the fact that three relations are mutually
  8 | ||| exclusive. A value of type `Trichotomy lt m n` proofs, that
  9 | ||| exactly one of the relations `lt m n`, `m === n`, or `lt n m` holds.
 10 | |||
 11 | ||| All proofs held by a value of type `Trichotomous` are erased, so
 12 | ||| at runtime such values get optimized to numbers 0, 1, or 2
 13 | ||| respectively.
 14 | public export
 15 | data Trichotomy : (lt : a -> a -> Type) -> (a -> a -> Type) where
 16 |   LT :  {0 lt : a -> a -> Type}
 17 |      -> (0 l : lt v w)
 18 |      -> (0 e : Not (v === w))
 19 |      -> (0 g : Not (lt w v))
 20 |      -> Trichotomy lt v w
 21 |
 22 |   EQ :  {0 lt : a -> a -> Type}
 23 |      -> (0 l : Not (lt v w))
 24 |      -> (0 e : v === w)
 25 |      -> (0 g : Not (lt w v))
 26 |      -> Trichotomy lt v w
 27 |
 28 |   GT :  {0 lt : a -> a -> Type}
 29 |      -> (0 l : Not (lt v w))
 30 |      -> (0 e : Not (v === w))
 31 |      -> (0 g : lt w v)
 32 |      -> Trichotomy lt v w
 33 |
 34 | -- identity at runtim
 35 | public export
 36 | conIndex : Trichotomy lt m n -> Bits8
 37 | conIndex (LT _ _ _) = 0
 38 | conIndex (EQ _ _ _) = 1
 39 | conIndex (GT _ _ _) = 2
 40 |
 41 | public export %inline
 42 | Eq (Trichotomy lt m n) where
 43 |   x == y = conIndex x == conIndex y
 44 |
 45 | public export
 46 | Ord (Trichotomy lt m n) where
 47 |   compare x y = compare (conIndex x) (conIndex y)
 48 |
 49 | public export
 50 | Show (Trichotomy lt m n) where
 51 |   show (LT _ _ _) = "LT"
 52 |   show (EQ _ _ _) = "EQ"
 53 |   show (GT _ _ _) = "GT"
 54 |
 55 | public export
 56 | toOrdering : Trichotomy lt m n -> Ordering
 57 | toOrdering (LT _ _ _) = LT
 58 | toOrdering (EQ _ _ _) = EQ
 59 | toOrdering (GT _ _ _) = GT
 60 |
 61 | public export
 62 | swap : Trichotomy lt m n -> Trichotomy lt n m
 63 | swap (LT l e g) = GT g (\x => e $ sym x) l
 64 | swap (EQ l e g) = EQ g (sym e) l
 65 | swap (GT l e g) = LT g (\x => e $ sym x) l
 66 |
 67 | --------------------------------------------------------------------------------
 68 | --          Trichotomous
 69 | --------------------------------------------------------------------------------
 70 |
 71 | public export
 72 | interface Trichotomous (0 a : Type) (0 rel : a -> a -> Type) | rel where
 73 |   constructor MkTrichotomous
 74 |   trichotomy : (m,n : a) -> Trichotomy rel m n
 75 |
 76 | public export
 77 | interface Transitive a rel => Trichotomous a rel => Strict a rel where
 78 |   constructor MkStrict
 79 |
 80 | public export
 81 | Trichotomous a rel => Antisymmetric a rel where
 82 |   antisymmetric q p = case trichotomy x y of
 83 |     LT _ _ g   => void $ g p
 84 |     EQ f _ _   => void $ f q
 85 |     GT f _ _   => void $ f q
 86 |
 87 | public export
 88 | 0 irreflexive : {x : _} -> Trichotomous a rel => rel x x -> Void
 89 | irreflexive lt = case trichotomy x x of
 90 |   LT _ g _   => g Refl
 91 |   EQ f _ _   => f lt
 92 |   GT f _ _   => f lt
 93 |
 94 | public export
 95 | Trichotomous a rel => Antisymmetric a (ReflexiveClosure rel) where
 96 |   antisymmetric _        Refl   = Refl
 97 |   antisymmetric Refl     _      = Refl
 98 |   antisymmetric (Rel q) (Rel p) = case trichotomy x y of
 99 |     LT _ _ g   => void $ g p
100 |     EQ f _ _   => void $ f q
101 |     GT f _ _   => void $ f q
102 |
103 | --------------------------------------------------------------------------------
104 | --          Corollaries
105 | --------------------------------------------------------------------------------
106 |
107 | ||| `m < n` implies `Not (m > n)`.
108 | export
109 | 0 Not_LT_and_GT : Trichotomous a lt => lt m n -> Not (lt n m)
110 | Not_LT_and_GT isLT isGT = case trichotomy m n of
111 |   LT _ _ g => g isGT
112 |   EQ _ _ g => g isGT
113 |   GT l _ _ => l isLT
114 |
115 | ||| `m < n` implies `Not (m === n)`.
116 | export
117 | 0 Not_LT_and_EQ : Trichotomous a lt => lt m n -> Not (m === n)
118 | Not_LT_and_EQ  isLT isEQ = case trichotomy m n of
119 |   LT _ e _ => e isEQ
120 |   EQ l _ _ => l isLT
121 |   GT _ e _ => e isEQ
122 |
123 | ||| `m < n` implies `Not (m >= n)`.
124 | export
125 | 0 Not_LT_and_GTE : Trichotomous a lt => lt m n -> Not (ReflexiveClosure lt n m)
126 | Not_LT_and_GTE l (Rel prf) = Not_LT_and_GT l prf
127 | Not_LT_and_GTE l Refl      = Not_LT_and_EQ l Refl
128 |