
   0 | module Decidable.Ordering
   1 | 
   2 | import Control.Relation.TotalOrder
   3 | import Data.Nat
   4 | import Decidable.Equality
   5 | import Decidable.Equality.Eq
   6 | import Decidable.EqOrd
   7 | 
   8 | 
   9 | public export
  10 | data OrdDecides : (0 r : a -> a -> Type) -> (x : a) -> (y : a) -> Ordering -> Type where
  11 |   LT : {0 r : a -> a -> Type} -> r x y -> OrdDecides r x y LT
  12 |   EQ : {0 r : a -> a -> Type} -> x = y -> OrdDecides r x y EQ
  13 |   GT : {0 r : a -> a -> Type} -> r y x -> OrdDecides r x y GT
  14 | 
  15 | public export
  16 | interface (TotalOrder a r, Ord a) => DecOrd a (0 r : a -> a -> Type) where
  17 |   decOrd : (x : a) -> (y : a) -> OrdDecides r x y (compare x y)
  18 | 
  19 | 
  20 | public export
  21 | ordDecidesEq : (Ord a, Irreflexive a r) => {x : a} -> {y : a} -> OrdDecides r x y (compare x y) -> Dec (x = y)
  22 | ordDecidesEq d with (compare x y)
  23 |   ordDecidesEq (LT p) | LT = No (irrefl' p)
  24 |   ordDecidesEq (EQ p) | EQ = Yes p
  25 |   ordDecidesEq (GT p) | GT = No (\e => irrefl' p (sym e))
  26 | 
  27 | 
  28 | public export
  29 | data BoolOrder : Bool -> Bool -> Type where
  30 |   FalseTrue : BoolOrder False True
  31 | 
  32 | public export
  33 | Irreflexive Bool BoolOrder where
  34 |   irrefl FalseTrue impossible
  35 | 
  36 | public export
  37 | Trichotomous Bool BoolOrder where
  38 |   trichotomy False False = EQ Refl
  39 |   trichotomy False True = LT FalseTrue
  40 |   trichotomy True False = GT FalseTrue
  41 |   trichotomy True True = EQ Refl
  42 | 
  43 | public export
  44 | Transitive Bool BoolOrder where
  45 |   transitive FalseTrue FalseTrue impossible
  46 | 
  47 | public export
  48 | TotalOrder Bool BoolOrder where
  49 | 
  50 | public export
  51 | DecOrd Bool BoolOrder where
  52 |   decOrd False True = LT FalseTrue
  53 |   decOrd True False = GT FalseTrue
  54 |   decOrd False False = EQ Refl
  55 |   decOrd True True = EQ Refl
  56 | 
  57 | public export
  58 | decOrdNatSucc : OrdDecides LT m n (compare m n) -> OrdDecides LT (S m) (S n) (compare (S m) (S n))
  59 | decOrdNatSucc {m} {n} c with 0 (compare m n)
  60 |   decOrdNatSucc (LT p) | LT = LT (LTESucc p)
  61 |   decOrdNatSucc (EQ q) | EQ = EQ (cong S q)
  62 |   decOrdNatSucc (GT r) | GT = GT (LTESucc r)
  63 | 
  64 | public export
  65 | DecOrd Nat LT where
  66 |   decOrd 0 0 = EQ Refl
  67 |   decOrd 0 (S n) = LT (LTESucc LTEZero)
  68 |   decOrd (S m) 0 = GT (LTESucc LTEZero)
  69 |   decOrd (S m) (S n) = decOrdNatSucc (decOrd m n)
  70 | 
  71 | 
  72 | data EitherOrder : {0 a : Type} -> {0 b : Type} -> (a -> a -> Type) -> (b -> b -> Type) -> Either a b -> Either a b -> Type where
  73 |   LL : {0 x : a} -> {0 y : a} -> r x y -> EitherOrder r s (Left x) (Left y)
  74 |   LR : EitherOrder r s (Left x) (Right y)
  75 |   RR : {0 x : b} -> {0 y : b} -> s x y -> EitherOrder r s (Right x) (Right y)
  76 | 
  77 | (Irreflexive a r, Irreflexive b s) => Irreflexive (Either a b) (EitherOrder r s) where
  78 |   irrefl (LL e) = irrefl e
  79 |   irrefl (RR e) = irrefl e
  80 | 
  81 | (Trichotomous a r, Trichotomous b s) => Trichotomous (Either a b) (EitherOrder r s) where
  82 |   trichotomy (Left x) (Left y) with (trichotomy {r = r} x y)
  83 |     trichotomy (Left x) (Left y) | LT e = LT (LL e)
  84 |     trichotomy (Left x) (Left x) | EQ Refl = EQ Refl
  85 |     trichotomy (Left x) (Left y) | GT e = GT (LL e)
  86 |   trichotomy (Left x) (Right y) = LT LR
  87 |   trichotomy (Right x) (Left y) = GT LR
  88 |   trichotomy (Right x) (Right y) with (trichotomy {r = s} x y)
  89 |     trichotomy (Right x) (Right y) | (LT e) = LT (RR e)
  90 |     trichotomy (Right x) (Right x) | (EQ Refl) = EQ Refl
  91 |     trichotomy (Right x) (Right y) | (GT e) = GT (RR e)
  92 | 
  93 | (Transitive a r, Transitive b s) => Transitive (Either a b) (EitherOrder r s) where
  94 |   transitive (LL u) (LL v) = LL (transitive u v)
  95 |   transitive (LL _) LR = LR
  96 |   transitive LR (RR _) = LR
  97 |   transitive (RR u) (RR v) = RR (transitive u v)
  98 | 
  99 | (TotalOrder a r, TotalOrder b s) => TotalOrder (Either a b) (EitherOrder r s) where
 100 | 
 101 | (DecOrd a r, DecOrd b s) => DecOrd (Either a b) (EitherOrder r s) where
 102 |   decOrd (Left x) (Left y) with (decOrd {r = r} x y) | (compare x y)
 103 |     decOrd (Left x) (Left y) | (LT p) | LT = LT (LL p)
 104 |     decOrd (Left x) (Left y) | (EQ e) | EQ = EQ (cong Left e)
 105 |     decOrd (Left x) (Left y) | (GT p) | GT = GT (LL p)
 106 |   decOrd (Left x) (Right y) = LT LR
 107 |   decOrd (Right x) (Left y) = GT LR
 108 |   decOrd (Right x) (Right y) with (decOrd {r = s} x y) | (compare x y)
 109 |     decOrd (Right x) (Right y) | (LT p) | LT = LT (RR p)
 110 |     decOrd (Right x) (Right y) | (EQ e) | EQ = EQ (cong Right e)
 111 |     decOrd (Right x) (Right y) | (GT p) | GT = GT (RR p)
 112 | 
 113 | 
 114 | data PairOrder : {0 a : Type} -> {0 b : Type} -> (a -> a -> Type) -> (b -> b -> Type) -> (a, b) -> (a, b) -> Type where
 115 |   OnFst : {0 y1 : b} -> {0 y2 : b} -> r x1 x2 -> PairOrder r s (x1,y1) (x2,y2)
 116 |   OnSnd : x1 = x2 -> s y1 y2 -> PairOrder r s (x1,y1) (x2,y2)
 117 | 
 118 | (Irreflexive a r, Irreflexive b s) => Irreflexive (a, b) (PairOrder r s) where
 119 |   irrefl (OnFst p) = irrefl p
 120 |   irrefl (OnSnd _ p) = irrefl p
 121 | 
 122 | (Trichotomous a r, Trichotomous b s) => Trichotomous (a, b) (PairOrder r s) where
 123 |   trichotomy (x1,y1) (x2,y2) with (trichotomy {r = r} x1 x2)
 124 |     trichotomy (x1,y1) (x2,y2) | (LT p) = LT (OnFst p)
 125 |     trichotomy (x1,y1) (x2,y2) | (GT p) = GT (OnFst p)
 126 |     trichotomy (x1,y1) (x2,y2) | (EQ e) with (trichotomy {r = s} y1 y2)
 127 |       trichotomy (x1,y1) (x2,y2) | (EQ e) | (LT p) = LT (OnSnd e p)
 128 |       trichotomy (x1,y1) (x2,y2) | (EQ e) | (GT p) = GT (OnSnd (sym e) p)
 129 |       trichotomy (x1,y1) (x1,y1) | (EQ Refl) | (EQ Refl) = EQ Refl
 130 | 
 131 | (Transitive a r, Transitive b s) => Transitive (a, b) (PairOrder r s) where
 132 |   transitive (OnFst p) (OnFst q) = OnFst (transitive p q)
 133 |   transitive (OnFst p) (OnSnd Refl _) = OnFst p
 134 |   transitive (OnSnd Refl _) (OnFst q) = OnFst q
 135 |   transitive (OnSnd Refl p) (OnSnd Refl q) = OnSnd Refl (transitive p q)
 136 | 
 137 | (TotalOrder a r, TotalOrder b s) => TotalOrder (a, b) (PairOrder r s) where
 138 | 
 139 | {-
 140 | (OrdCompatible a, DecOrd a r, DecOrd b s) => DecOrd (a, b) (PairOrder r s) where
 141 |   decOrd (x1,y1) (x2,y2) with (decOrd {r = r} x1 x2) | (eqOrdCompat x1 x2) | (compare x1 x2) | (x1 == x2)
 142 |     decOrd (x1,y1) (x2,y2) | DecOrd.LT p | EqOrdCompat.LT | Compare.LT | False = ?what1
 143 |     decOrd (x1,y1) (x2,y2) | DecOrd.EQ e | EqOrdCompat.EQ | Compare.EQ | True = ?what2
 144 |     decOrd (x1,y1) (x2,y2) | DecOrd.GT p | EqOrdCompat.GT | Compare.GT | False = ?what3
 145 | -}
 146 | 
 147 | 
 148 | data Lexicographic : (r : a -> a -> Type) -> List a -> List a -> Type where
 149 |   CmpNil : Lexicographic r [] (y :: ys)
 150 |   CmpNow : {0 xs : List a} -> {0 ys : List a} -> r x y -> Lexicographic r (x :: xs) (y :: ys)
 151 |   CmpLater : x = y -> Lexicographic r xs ys -> Lexicographic r (x :: xs) (y :: ys)
 152 | 
 153 | (Irreflexive a r) => Irreflexive (List a) (Lexicographic r) where
 154 |   irrefl (CmpNow p) = irrefl p
 155 |   irrefl (CmpLater _ p) = irrefl p
 156 | 
 157 | (Trichotomous a r) => Trichotomous (List a) (Lexicographic r) where
 158 |   trichotomy [] [] = EQ Refl
 159 |   trichotomy [] (_ :: _) = LT CmpNil
 160 |   trichotomy (_ :: _) [] = GT CmpNil
 161 |   trichotomy (x :: xs) (y :: ys) with (trichotomy {r} x y)
 162 |     trichotomy (x :: xs) (y :: ys) | (LT p) = LT (CmpNow p)
 163 |     trichotomy (x :: xs) (y :: ys) | (GT p) = GT (CmpNow p)
 164 |     trichotomy (x :: xs) (y :: ys) | (EQ e) with (trichotomy {r = Lexicographic r} xs ys)
 165 |       trichotomy (x :: xs) (y :: ys) | (EQ e) | (LT p) = LT (CmpLater e p)
 166 |       trichotomy (x :: xs) (y :: ys) | (EQ e) | (GT p) = GT (CmpLater (sym e) p)
 167 |       trichotomy (x :: xs) (x :: xs) | (EQ Refl) | (EQ Refl) = EQ Refl
 168 | 
 169 | (Transitive a r) => Transitive (List a) (Lexicographic r) where
 170 |   transitive CmpNil (CmpNow _) = CmpNil
 171 |   transitive CmpNil (CmpLater _ _) = CmpNil
 172 |   transitive (CmpNow p) (CmpNow q) = CmpNow (transitive p q)
 173 |   transitive (CmpNow p) (CmpLater Refl _) = CmpNow p
 174 |   transitive (CmpLater Refl _) (CmpNow q) = CmpNow q
 175 |   transitive (CmpLater Refl p) (CmpLater Refl q) = CmpLater Refl (transitive p q)
 176 | 
 177 | (TotalOrder a r) => TotalOrder (List a) (Lexicographic r) where
 178 | 
 179 | (DecOrd a r) => DecOrd (List a) (Lexicographic r) where
 180 |   decOrd [] [] = EQ Refl
 181 |   decOrd [] (y :: ys) = LT CmpNil
 182 |   decOrd (x :: xs) [] = GT CmpNil
 183 |   decOrd (x :: xs) (y :: ys) with (decOrd {r = r} x y) | (compare x y)
 184 |     decOrd (x :: xs) (y :: ys) | (LT p) | LT = LT (CmpNow p)
 185 |     decOrd (x :: xs) (y :: ys) | (GT p) | GT = GT (CmpNow p)
 186 |     decOrd (x :: xs) (y :: ys) | (EQ e) | EQ with (decOrd {r = Lexicographic r} xs ys) | (compare xs ys)
 187 |       decOrd (x :: xs) (y :: ys) | (EQ e) | EQ | (LT p) | LT = LT (CmpLater e p)
 188 |       decOrd (x :: xs) (y :: ys) | (EQ e) | EQ | (GT p) | GT = GT (CmpLater (sym e) p)
 189 |       decOrd (x :: xs) (y :: ys) | (EQ e) | EQ | (EQ f) | EQ = EQ (cong2 (::) e f)
 190 |