
   0 | ||| Axioms and propsitions for primitive types with an
   1 | ||| `Ord` implementation.
   2 | module Data.Prim.Ord
   3 | 
   4 | import public Data.Trichotomy
   5 | 
   6 | %default total
   7 | 
   8 | ||| Similar to `Either` but with erased fields.
   9 | public export
  10 | data Either0 : Type -> Type -> Type where
  11 |   Left0  : (0 v : a) -> Either0 a b
  12 |   Right0 : (0 v : b) -> Either0 a b
  13 | 
  14 | ||| We often don't trust values of type `a === b`, as they might
  15 | ||| have been magically crafted using `believe_me` or `assert_total`
  16 | ||| followed by `idris_crash`. If a value of another type follows
  17 | ||| from a (potentially) magically crafted one, we only want the
  18 | ||| second value to reduce at compile time, if the first value
  19 | ||| reduces to `Refl`. Otherwise, we risk blowing up the compiler
  20 | ||| in an absurd context.
  21 | export
  22 | strictRefl : (0 prf : a === b) -> Lazy c -> c
  23 | strictRefl Refl x = x
  24 | 
  25 | --------------------------------------------------------------------------------
  26 | --          Interface
  27 | --------------------------------------------------------------------------------
  28 | 
  29 | ||| This interface is a witness that the given primitive type
  30 | ||| comes with a relation `lt`, with `lt` being a strict total order.
  31 | ||| We typically define the following aliases
  32 | ||| (or name the relation accordingly):
  33 | |||
  34 | |||   `m < n`  := lt m n
  35 | |||   `m > n`  := lt n m
  36 | |||   `m <= n` := Either (lt m n) (m === n)
  37 | |||   `m >= n` := Either (lt n m) (n === m)
  38 | |||   `m /= n` := Either (lt m n) (lt n m)
  39 | |||
  40 | ||| The following axioms must hold:
  41 | |||   1. (<) is transitive: From `k < m` and `m < n` follows `k < n`.
  42 | |||
  43 | |||   2. Trichotomy: For all values `m` and `n` exactly one of the
  44 | |||      following holds: `m < n`, `m === n`, or `n < m`.
  45 | |||
  46 | ||| It is in the nature of a primitive that we can't proof these axioms
  47 | ||| in Idris itself. We must therefore assume that they hold on all backends,
  48 | ||| and it is the responsibility of programmers implementing
  49 | ||| interface `Total` to make sure that the axioms actually hold.
  50 | public export
  51 | interface Total (0 a : Type) (0 lt : a -> a -> Type) | lt where
  52 |   ||| Axiom I: `<` is transitive.
  53 |   0 transLT : {k,m,n : a} -> lt k m -> lt m n -> lt k n
  54 | 
  55 |   ||| Axiom II: Trichotomy of `<`, `===`, and `>`.
  56 |   trichotomy : (m,n : a) -> Trichotomy lt m n
  57 | 
  58 | ||| Tests if the first value is strictly less than the second or not
  59 | export
  60 | testLT : Total a lt => (x,y : a) -> Either0 (lt x y) (Either (lt y x) (y === x))
  61 | testLT x y = case trichotomy {lt} x y of
  62 |   LT p _ _ => Left0 p
  63 |   EQ _ p _ => Right0 (Right $ sym p)
  64 |   GT _ _ p => Right0 (Left p)
  65 | 
  66 | ||| Tests if the first value is strictly greater than the second or not
  67 | export
  68 | testGT : Total a lt => (x,y : a) -> Either0 (lt y x) (Either (lt x y) (x === y))
  69 | testGT x y = case trichotomy {lt} x y of
  70 |   GT _ _ p => Left0 p
  71 |   LT p _ _ => Right0 (Left p)
  72 |   EQ _ p _ => Right0 (Right p)
  73 | 
  74 | ||| Tests if the two values are provably equal or not
  75 | export
  76 | testEQ : Total a lt => (x,y : a) -> Either0 (x === y) (Either (lt x y) (lt y x))
  77 | testEQ x y = case trichotomy {lt} x y of
  78 |   EQ _ p _ => Left0 p
  79 |   LT p _ _ => Right0 (Left p)
  80 |   GT _ _ p => Right0 (Right p)
  81 | 
  82 | --------------------------------------------------------------------------------
  83 | --          Corollaries
  84 | --------------------------------------------------------------------------------
  85 | 
  86 | ||| `<` is irreflexive.
  87 | export
  88 | 0 irrefl : Total a lt => Not (lt m m)
  89 | irrefl x = case trichotomy m m of
  90 |   LT y _ f => f y
  91 |   EQ f _ _ => f x
  92 |   GT f _ y => f y
  93 | 
  94 | --------------------------------------------------------------------------------
  95 | --          Transitivities
  96 | --------------------------------------------------------------------------------
  97 | 
  98 | namespace LT
  99 | 
 100 |   ||| This is an alias for `transLT`
 101 |   export
 102 |   0 trans : Total a lt => lt k m -> lt m n -> lt k n
 103 |   trans = transLT
 104 | 
 105 | ||| `k === m` and `m /= n` implies `k /= n`.
 106 | export
 107 | 0 trans_EQ_NEQ :
 108 |      {auto _ : Total a lt}
 109 |   -> k === m
 110 |   -> Either (lt m n) (lt n m)
 111 |   -> Either (lt k n) (lt n k)
 112 | trans_EQ_NEQ eqv neq  = rewrite eqv in neq
 113 | 
 114 | ||| `k === m` and `m /= n` implies `k /= n`.
 115 | export
 116 | 0 trans_NEQ_EQ :
 117 |      {auto _ : Total a lt}
 118 |   -> Either (lt k m) (lt m k)
 119 |   -> m === n
 120 |   -> Either (lt k n) (lt n k)
 121 | trans_NEQ_EQ neq eqv = rewrite (sym eqv) in neq
 122 | 
 123 | ||| `k < m` and `m === n` implies `k < n`
 124 | export
 125 | 0 trans_LT_EQ : Total a lt => lt k m -> m === n -> lt k n
 126 | trans_LT_EQ p eqv = rewrite sym eqv in p
 127 | 
 128 | ||| `k === m` and `m < n` implies `k < n`
 129 | export
 130 | 0 trans_EQ_LT : Total a lt => k === m -> lt m n -> lt k n
 131 | trans_EQ_LT eqv q = rewrite eqv in q
 132 | 
 133 | ||| `k <= m` and `m < n` implies `k < n`
 134 | export
 135 | 0 trans_LTE_LT : Total a lt => Either (lt k m) (k === m) -> lt m n -> lt k n
 136 | trans_LTE_LT x y = either (`trans` y) (`trans_EQ_LT` y) x
 137 | 
 138 | ||| `k < m` and `m <= n` implies `k < n`
 139 | export
 140 | 0 trans_LT_LTE : Total a lt => lt k m -> Either (lt m n) (m === n) -> lt k n
 141 | trans_LT_LTE x = either (trans x) (trans_LT_EQ x)
 142 | 
 143 | ||| `k > m` and `m === n` implies `k > n`
 144 | export
 145 | 0 trans_GT_EQ : Total a lt => lt m k -> m === n -> lt n k
 146 | trans_GT_EQ p eqv = rewrite sym eqv in p
 147 | 
 148 | ||| `k === m` and `m > n` implies `k > n`
 149 | export
 150 | 0 trans_EQ_GT : Total a lt => k === m -> lt n m -> lt n k
 151 | trans_EQ_GT eqv q = rewrite eqv in q
 152 | 
 153 | ||| `k >= m` and `m > n` implies `k > n`
 154 | export
 155 | 0 trans_GTE_GT : Total a lt => Either (lt m k) (m === k) -> lt n m -> lt n k
 156 | trans_GTE_GT x y = either (trans y) (\v => trans_EQ_GT (sym v) y) x
 157 | 
 158 | ||| `k > m` and `m >= n` implies `k > n`
 159 | export
 160 | 0 trans_GT_GTE : Total a lt => lt m k -> Either (lt n m) (n === m) -> lt n k
 161 | trans_GT_GTE x (Left y)  = trans y x
 162 | trans_GT_GTE x (Right y) = trans_GT_EQ x (sym y)
 163 | 
 164 | namespace LTE
 165 | 
 166 |   ||| `<=` is reflexive.
 167 |   export
 168 |   0 refl : Total a lt => Either (lt m m) (m === m)
 169 |   refl = Right Refl
 170 | 
 171 |   ||| `<=` is transitive.
 172 |   export
 173 |   0 trans :
 174 |        {auto _ : Total a lt}
 175 |     -> Either (lt k m) (k === m)
 176 |     -> Either (lt m n) (m === n)
 177 |     -> Either (lt k n) (k === n)
 178 |   trans (Left x)  y         = Left (trans_LT_LTE x y)
 179 |   trans (Right x) (Left y)  = Left (trans_EQ_LT x y)
 180 |   trans (Right x) (Right y) = Right (trans x y)
 181 | 
 182 |   ||| `<=` is antisymmetric.
 183 |   export
 184 |   0 antisym :
 185 |        {auto _ : Total a lt}
 186 |     -> Either (lt m n) (m === n)
 187 |     -> Either (lt n m) (m === n)
 188 |     -> m === n
 189 |   antisym (Right x) _         = x
 190 |   antisym (Left x)  (Right y) = y
 191 |   antisym (Left x)  (Left y)  = void (irrefl $ trans x y)
 192 | 
 193 | ||| `k <= m` and `m === n` implies `k <= n`
 194 | export
 195 | 0 trans_LTE_EQ :
 196 |      {auto _ : Total a lt}
 197 |   -> Either (lt k m) (k === m)
 198 |   -> m === n
 199 |   -> Either (lt k n) (k === n)
 200 | trans_LTE_EQ lte eq = trans lte (Right eq)
 201 | 
 202 | ||| `k === m` and `m <= n` implies `(k <= n)`
 203 | export
 204 | 0 trans_EQ_LTE :
 205 |      {auto _ : Total a lt}
 206 |   -> k === m
 207 |   -> Either (lt m n) (m === n)
 208 |   -> Either (lt k n) (k === n)
 209 | trans_EQ_LTE eq lte = trans (Right eq) lte
 210 | 
 211 | namespace GTE
 212 | 
 213 |   ||| `>=` is transitive.
 214 |   export
 215 |   0 trans :
 216 |        {auto _ : Total a lt}
 217 |     -> Either (lt m k) (m === k)
 218 |     -> Either (lt n m) (n === m)
 219 |     -> Either (lt n k) (n === k)
 220 |   trans (Left x)  y         = Left (trans_GT_GTE x y)
 221 |   trans (Right x) (Left y)  = Left (trans_EQ_GT (sym x) y)
 222 |   trans (Right x) (Right y) = Right (trans y x)
 223 | 
 224 |   ||| `>=` is antisymmetric.
 225 |   export
 226 |   0 antisym :
 227 |        {auto _ : Total a lt}
 228 |     -> Either (lt n m) (m === n)
 229 |     -> Either (lt m n) (m === n)
 230 |     -> m === n
 231 |   antisym (Right x) _         = x
 232 |   antisym (Left x)  (Right y) = y
 233 |   antisym (Left x)  (Left y)  = void (irrefl $ trans x y)
 234 | 
 235 | ||| `k >= m` and `m === n` implies `k >= n`
 236 | export
 237 | 0 trans_GTE_EQ :
 238 |      {auto _ : Total a lt}
 239 |   -> Either (lt m k) (m === k)
 240 |   -> m === n
 241 |   -> Either (lt n k) (n === k)
 242 | trans_GTE_EQ gte eq = trans gte (Right $ sym eq)
 243 | 
 244 | ||| `k === m` and `m <= n` implies `(k <= n)`
 245 | export
 246 | 0 trans_EQ_GTE :
 247 |      {auto _ : Total a lt}
 248 |   -> k === m
 249 |   -> Either (lt n m) (n === m)
 250 |   -> Either (lt n k) (n === k)
 251 | trans_EQ_GTE eq gte = trans (Right $ sym eq) gte
 252 | 
 253 | --------------------------------------------------------------------------------
 254 | --          Conversions
 255 | --------------------------------------------------------------------------------
 256 | 
 257 | ||| `m < n` implies `Not (m > n)`.
 258 | export
 259 | 0 LT_not_GT : Total a lt => lt m n -> Not (lt n m)
 260 | LT_not_GT isLT isGT = case trichotomy m n of
 261 |   LT _ _ g => g isGT
 262 |   EQ _ _ g => g isGT
 263 |   GT f _ _ => f isLT
 264 | 
 265 | ||| `m < n` implies `Not (m === n)`.
 266 | export
 267 | 0 LT_not_EQ : Total a lt => lt m n -> Not (m === n)
 268 | LT_not_EQ isLT isEQ = case trichotomy m n of
 269 |   LT _ g _ => g isEQ
 270 |   EQ f _ _ => f isLT
 271 |   GT _ g _ => g isEQ
 272 | 
 273 | ||| `m < n` implies `Not (m >= n)`.
 274 | export
 275 | 0 LT_not_GTE : Total a lt => lt m n -> Not (Either (lt n m) (n === m))
 276 | LT_not_GTE l = either (LT_not_GT l) (\e => LT_not_EQ l (sym e))
 277 | 
 278 | ||| `Not (m < n)` implies `m >= n`.
 279 | export
 280 | 0 Not_LT_to_GTE : Total a lt => Not (lt m n) -> Either (lt n m) (n === m)
 281 | Not_LT_to_GTE f = case trichotomy m n of
 282 |   LT x _ _ => void (f x)
 283 |   EQ _ x _ => Right (sym x)
 284 |   GT _ _ x => Left x
 285 | 
 286 | ||| `m === n` implies `Not (m < n)`.
 287 | export
 288 | 0 EQ_not_LT : Total a lt => m === n -> Not (lt m n)
 289 | EQ_not_LT = flip LT_not_EQ
 290 | 
 291 | ||| `m === n` implies `Not (m > n)`.
 292 | export
 293 | 0 EQ_not_GT : Total a lt => m === n -> Not (lt n m)
 294 | EQ_not_GT isEQ = EQ_not_LT (sym isEQ)
 295 | 
 296 | ||| `m === n` implies `Not (m /= n)`.
 297 | export
 298 | 0 EQ_not_NEQ : Total a lt => m === n -> Not (Either (lt m n) (lt n m))
 299 | EQ_not_NEQ isEQ = either (EQ_not_LT isEQ) (EQ_not_GT isEQ)
 300 | 
 301 | ||| `Not (m < n)` implies `m /= n`.
 302 | export
 303 | 0 Not_EQ_to_NEQ : Total a lt => Not (m === n) -> Either (lt m n) (lt n m)
 304 | Not_EQ_to_NEQ f = case trichotomy m n of
 305 |   LT x _ _ => Left x
 306 |   EQ _ x _ => void (f x)
 307 |   GT _ _ x => Right x
 308 | 
 309 | ||| `m > n` implies `Not (m < n)`.
 310 | export
 311 | 0 GT_not_LT : Total a lt => lt n m -> Not (lt m n)
 312 | GT_not_LT = LT_not_GT
 313 | 
 314 | ||| `m > n` implies `Not (m === n)`.
 315 | export
 316 | 0 GT_not_EQ : Total a lt => lt n m -> Not (m === n)
 317 | GT_not_EQ = flip EQ_not_GT
 318 | 
 319 | ||| `m > n` implies `Not (m <= n)`.
 320 | export
 321 | 0 GT_not_LTE : Total a lt => lt n m -> Not (Either (lt m n) (m === n))
 322 | GT_not_LTE gt = either (GT_not_LT gt) (GT_not_EQ gt)
 323 | 
 324 | ||| `Not (m > n)` implies `m <= n`.
 325 | export
 326 | 0 Not_GT_to_LTE : Total a lt => Not (lt n m) -> Either (lt m n) (m === n)
 327 | Not_GT_to_LTE f = case trichotomy m n of
 328 |   LT x _ _ => Left x
 329 |   EQ _ x _ => Right x
 330 |   GT _ _ x => void (f x)
 331 | 
 332 | ||| `m <= n` implies `Not (m > n)`.
 333 | export
 334 | 0 LTE_not_GT : Total a lt => (Either (lt m n) (m === n)) -> Not (lt n m)
 335 | LTE_not_GT = either LT_not_GT EQ_not_GT
 336 | 
 337 | ||| `Not (m <= n)` implies `m > n`.
 338 | export
 339 | 0 Not_LTE_to_GT : Total a lt => Not (Either (lt m n) (m === n)) -> lt n m
 340 | Not_LTE_to_GT f = case trichotomy m n of
 341 |   LT x _ _ => void (f $ Left x)
 342 |   EQ _ x _ => void (f $ Right x)
 343 |   GT _ _ x => x
 344 | 
 345 | ||| `m <= n` and `m >= n` implies `m === n`.
 346 | export
 347 | 0 LTE_and_GTE_to_EQ :
 348 |      {auto _ : Total a lt}
 349 |   -> Either (lt m n) (m === n)
 350 |   -> Either (lt n m) (n === m)
 351 |   -> m === n
 352 | LTE_and_GTE_to_EQ (Left x)  (Right y) = sym y
 353 | LTE_and_GTE_to_EQ (Right x) _         = x
 354 | LTE_and_GTE_to_EQ (Left x)  (Left y)  = void (LT_not_GT x y)
 355 | 
 356 | ||| `m <= n` and `m /= n` implies `m < n`.
 357 | export
 358 | 0 LTE_and_NEQ_to_LT :
 359 |      {auto _ : Total a lt}
 360 |   -> Either (lt m n) (m === n)
 361 |   -> Either (lt m n) (lt n m)
 362 |   -> lt m n
 363 | LTE_and_NEQ_to_LT (Left x)  _         = x
 364 | LTE_and_NEQ_to_LT (Right _) (Left x)  = x
 365 | LTE_and_NEQ_to_LT (Right x) (Right y) = void (EQ_not_GT x y)
 366 | 
 367 | ||| `m /= n` implies `Not (m === n)`.
 368 | export
 369 | 0 NEQ_not_EQ : Total a lt => Either (lt m n) (lt n m) -> Not (m === n)
 370 | NEQ_not_EQ = either LT_not_EQ GT_not_EQ
 371 | 
 372 | ||| `Not (m /= n)` implies `m === n`.
 373 | export
 374 | 0 Not_NEQ_to_EQ : Total a lt => Not (Either (lt m n) (lt n m)) -> m === n
 375 | Not_NEQ_to_EQ f = case trichotomy m n of
 376 |   LT x _ _ => void (f $ Left x)
 377 |   EQ _ x _ => x
 378 |   GT _ _ x => void (f $ Right x)
 379 | 
 380 | ||| `m /= n` and `m <= n` implies `m < n`.
 381 | export
 382 | 0 NEQ_and_LTE_to_LT :
 383 |      {auto _ : Total a lt}
 384 |   -> Either (lt m n) (lt n m)
 385 |   -> Either (lt m n) (m === n)
 386 |   -> lt m n
 387 | NEQ_and_LTE_to_LT = flip LTE_and_NEQ_to_LT
 388 | 
 389 | ||| `m /= n` and `m <= n` implies `m < n`.
 390 | export
 391 | 0 NEQ_and_GTE_to_GT :
 392 |      {auto _ : Total a lt}
 393 |   -> Either (lt m n) (lt n m)
 394 |   -> Either (lt n m) (n === m)
 395 |   -> lt n m
 396 | NEQ_and_GTE_to_GT (Right x) _         = x
 397 | NEQ_and_GTE_to_GT (Left _)  (Left y)  = y
 398 | NEQ_and_GTE_to_GT (Left x)  (Right y) = void (GT_not_EQ x y)
 399 | 
 400 | ||| `m >= n` implies `Not (m < n)`.
 401 | export
 402 | 0 GTE_not_LT : Total a lt => Either (lt n m) (n === m) -> Not (lt m n)
 403 | GTE_not_LT = either GT_not_LT EQ_not_GT
 404 | 
 405 | ||| `Not (m >= n)` implies `m < n`.
 406 | export
 407 | 0 Not_GTE_to_LT : Total a lt => Not (Either (lt n m) (n === m)) -> lt m n
 408 | Not_GTE_to_LT f = case trichotomy m n of
 409 |   LT x _ _ => x
 410 |   EQ _ x _ => void (f $ Right (sym x))
 411 |   GT _ _ x => void (f $ Left x)
 412 | 
 413 | ||| `m >= n` and `m <= n` implies `m === n`.
 414 | export
 415 | 0 GTE_and_LTE_to_EQ :
 416 |      {auto _ : Total a lt}
 417 |   -> Either (lt n m) (n === m)
 418 |   -> Either (lt m n) (m === n)
 419 |   -> m === n
 420 | GTE_and_LTE_to_EQ = flip LTE_and_GTE_to_EQ
 421 | 
 422 | ||| `m >= n` and `m /= n` implies `m > n`.
 423 | export
 424 | 0 GTE_and_NEQ_to_GT :
 425 |      {auto _ : Total a lt}
 426 |   -> Either (lt n m) (n === m)
 427 |   -> Either (lt m n) (lt n m)
 428 |   -> lt n m
 429 | GTE_and_NEQ_to_GT = flip NEQ_and_GTE_to_GT
 430 |