Data.Int.Order

Implementation of ordering relations for the primitive type `Int`
This is full of tricks as `Int` is a primitive type that can only
be interacted with using either literals or built-in functions.
The exported interface should however be safe.

Definitions

strictRefl : a = b -> Lazy c -> c

  Pattern-match on an equality proof so that the second argument to
  strictRefl is only returned once the first is canonical.

Totality: total
Visibility: export

data LT : Int -> Int -> Type

  `LT a b` is a proof that `a` is less than `b` which is to say that
  the function call `a < b` returns `True`.
  
  NB: we do not re-export the constructor so that users cannot force
  our magic functions to blow up in absurd contexts by bypassing the
  safety measures introduced by the `strictX` functions.
  We do provide functions corresponding to the wrapping and unwrapping
  of `LT` but, crucially, they do not let people force `LT` proofs to
  be in canonical form.

Totality: total
Visibility: export
Constructor: 

MkLT : a < b = True -> LT a b

mkLT : a < b = True -> LT a b

  We may prove `LT a b` by using a proof that `a < b` returns `True`.

Totality: total
Visibility: export

runLT : LT a b -> a < b = True

  From a proof that `LT a b`, we may concluded that `a < b` returns `True`.

Totality: total
Visibility: export

strictLT : LT a b -> Lazy c -> c

  Do not trust arbitrary `LT` proofs when manufacturing magic ones:
  be strict!

Totality: total
Visibility: export

decide : (a : Int) -> (b : Int) -> Dec (LT a b)

  LT is decidable, by virtue of being the reflection of a boolean function

Totality: total
Visibility: export

trans : LT a b -> LT b c -> LT a (the Int c)

  LT is a transitive relation. This cannot be proven so we use a magic trick.

Totality: total
Visibility: export

irrefl : Not (LT a a)

  LT is an irreflexive relation.
  The crash will never happen because the `LT a a` argument will never reduce
  to a canonical form (unless the built-in function (<) is buggy).

Totality: total
Visibility: export

GT : Int -> Int -> Type

  GT is defined in terms of LT to avoid code duplication

Totality: total
Visibility: public export

LT_not_GT : LT a b -> Not (GT a b)

Totality: total
Visibility: export

GT_not_LT : GT a b -> Not (LT a b)

Totality: total
Visibility: export

data EQ : Int -> Int -> Type

  `EQ a b` is a proof that `a` is equal to `b` which is to say that
  the function call `a == b` returns `True`.
  
  NB: we do not re-export the constructor so that users cannot force
  our magic functions to blow up in absurd contexts by bypassing the
  safety measures introduced by the `strictX` functions.
  We do provide functions corresponding to the wrapping and unwrapping
  of `EQ` but, crucially, they do not let people force `EQ` proofs to
  be in canonical form.

Totality: total
Visibility: export
Constructor: 

MkEQ : a == b = True -> EQ a b

mkEQ : a == b = True -> EQ a b

  We may prove `EQ a b` by using a proof that `a == b` returns `True`.

Totality: total
Visibility: export

runEQ : EQ a b -> a == b = True

  From a proof that `EQ a b`, we may concluded that `a == b` returns `True`.

Totality: total
Visibility: export

strictEQ : EQ a b -> Lazy c -> c

  Do not trust arbitrary `EQ` proofs when manufacturing magic ones:
  be strict!

Totality: total
Visibility: export

decide : (a : Int) -> (b : Int) -> Dec (EQ a b)

  EQ is decidable, by virtue of being the reflection of a boolean function

Totality: total
Visibility: export

refl : EQ a a

  EQ is a reflexive relation

Totality: total
Visibility: export

elimEQ : (0 p : (Int -> Type)) -> EQ a b -> p a -> p b

  EQ is substitutive

Totality: total
Visibility: export

reflect : EQ a b -> a = b

  EQ implies propositional equality

Totality: total
Visibility: export

sym : EQ a b -> EQ b a

  EQ is a symmetric relation

Totality: total
Visibility: export

trans : EQ a b -> EQ b c -> EQ a c

  EQ is a transitive relation

Totality: total
Visibility: export

trans_LT_EQ : LT a b -> EQ b c -> LT a c

Totality: total
Visibility: export

trans_EQ_LT : EQ a b -> LT b c -> LT a c

Totality: total
Visibility: export

LT_not_EQ : LT a b -> Not (EQ a b)

Totality: total
Visibility: export

EQ_not_LT : EQ a b -> Not (LT a b)

Totality: total
Visibility: export

EQ_not_GT : EQ a b -> Not (GT a b)

Totality: total
Visibility: export

GT_not_EQ : GT a b -> Not (EQ a b)

Totality: total
Visibility: export

data LTE : Int -> Int -> Type

  `LTE a b` is a proof that `a` is less or equal to `b` which is to say that
  the function call `a < b` or `a == b` returns `True`.
  
  NB: we do not re-export the constructor so that users cannot force
  our magic functions to blow up in absurd contexts by bypassing the
  safety measures introduced by the `strictX` functions.

Totality: total
Visibility: export
Constructors:

MkLT : a < b = True -> LTE a b

MkEQ : a == b = True -> LTE a b

runLTE : LTE a b -> Either (LT a b) (EQ a b)

  Unwrap an LTE proof to get either an LT or an EQ one

Totality: total
Visibility: export

strictLTE : LTE a b -> Lazy c -> c

  Do not trust arbitrary `LTE` proofs when manufacturing magic ones:
  be strict!

Totality: total
Visibility: export

decide : (a : Int) -> (b : Int) -> Dec (LTE a b)

  LTE is decidable by virture of both LT and EQ being decidable

Totality: total
Visibility: export

refl : LTE a a

  LTE is a reflexive relation

Totality: total
Visibility: export

trans_LT_LTE : LT a b -> LTE b c -> LT a c

Totality: total
Visibility: export

trans_LTE_LT : LTE a b -> LT b c -> LT a c

Totality: total
Visibility: export

inject_LT_LTE : LT a b -> LTE a b

Totality: total
Visibility: export

inject_EQ_LTE : EQ a b -> LTE a b

Totality: total
Visibility: export

trans : LTE a b -> LTE b c -> LTE a c

  LTE is a transitive relation

Totality: total
Visibility: export

antisym : LTE a b -> LTE b a -> EQ a b

  LTE is an antisymmetric relation

Totality: total
Visibility: export

GTE : Int -> Int -> Type

  GTE is defined in terms of LTE to avoid code duplication

Totality: total
Visibility: public export

trichotomous : (a : Int) -> (b : Int) -> Trichotomous LT EQ GT a b

  Any pair of Ints is related either via LT, EQ, or GT

Totality: total
Visibility: export

decide_LT_GTE : (a : Int) -> (b : Int) -> Either (LT a b) (GTE a b)

  Any pair of Ints is related either via LT or GTE

Totality: total
Visibility: export

decide_LTE_GT : (a : Int) -> (b : Int) -> Either (LTE a b) (GT a b)

  Any pair of Ints is related either via LTE or GT

Totality: total
Visibility: export

suc_LT_LTE : LT a b -> LTE (a + 1) b

  Adding one to a strictly smaller Int, yields a smaller Int

Totality: total
Visibility: export

pred_LT_LTE : LT a b -> LTE a (b - 1)

  Subtracting one to a strictly larger Int, yields a larger Int

Totality: total
Visibility: export

sucBounded : LT a b -> LT a (a + 1)

  Adding one to an Int yields a strictly larger one,
  provided there is no overflow

Totality: total
Visibility: export