
   0 | module Data.Prim.Integer
   1 | 
   2 | import public Control.WellFounded
   3 | import public Data.Prim.Ord
   4 | import public Algebra.Solver.Ring
   5 | import Syntax.PreorderReasoning
   6 | 
   7 | %default total
   8 | 
   9 | unsafeRefl : a === b
  10 | unsafeRefl = believe_me (Refl {x = a})
  11 | 
  12 | --------------------------------------------------------------------------------
  13 | --          (<)
  14 | --------------------------------------------------------------------------------
  15 | 
  16 | ||| Witness that `m < n === True`.
  17 | export
  18 | data (<) : (m,n : Integer) -> Type where
  19 |   LT : {0 m,n : Integer} -> (0 prf : (m < n) === True) -> m < n
  20 | 
  21 | ||| Contructor for `(<)`.
  22 | |||
  23 | ||| This can only be used in an erased context.
  24 | export %hint
  25 | 0 mkLT : (0 prf : (m < n) === True) -> m < n
  26 | mkLT = LT
  27 | 
  28 | ||| Extractor for `(<)`.
  29 | |||
  30 | ||| This can only be used in an erased context.
  31 | export
  32 | 0 runLT : m < n -> (m < n) === True
  33 | runLT (LT prf) = prf
  34 | 
  35 | ||| We don't trust values of type `(<)` too much,
  36 | ||| so we use this when creating magical results.
  37 | export
  38 | strictLT : (0 p : m < n) -> Lazy c -> c
  39 | strictLT (LT prf) x = x
  40 | 
  41 | --------------------------------------------------------------------------------
  42 | --          Aliases
  43 | --------------------------------------------------------------------------------
  44 | 
  45 | ||| Flipped version of `(<)`.
  46 | public export
  47 | 0 (>) : (m,n : Integer) -> Type
  48 | m > n = n < m
  49 | 
  50 | ||| `m <= n` mean that either `m < n` or `m === n` holds.
  51 | public export
  52 | 0 (<=) : (m,n : Integer) -> Type
  53 | m <= n = Either (m < n) (m === n)
  54 | 
  55 | ||| Flipped version of `(<=)`.
  56 | public export
  57 | 0 (>=) : (m,n : Integer) -> Type
  58 | m >= n = n <= m
  59 | 
  60 | ||| `m /= n` mean that either `m < n` or `m > n` holds.
  61 | public export
  62 | 0 (/=) : (m,n : Integer) -> Type
  63 | m /= n = Either (m < n) (m > n)
  64 | 
  65 | --------------------------------------------------------------------------------
  66 | --          Order
  67 | --------------------------------------------------------------------------------
  68 | 
  69 | 0 ltNotEQ : m < n -> Not (m === n)
  70 | ltNotEQ x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and EQ")
  71 | 
  72 | 0 ltNotGT : m < n -> Not (n < m)
  73 | ltNotGT x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and GT")
  74 | 
  75 | 0 eqNotLT : m === n -> Not (m < n)
  76 | eqNotLT = flip ltNotEQ
  77 | 
  78 | export
  79 | comp : (m,n : Integer) -> Trichotomy (<) m n
  80 | comp m n = case prim__lt_Integer m n of
  81 |   0 => case prim__eq_Integer m n of
  82 |     0 => GT (ltNotGT $ LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (LT unsafeRefl)
  83 |     x => EQ (eqNotLT unsafeRefl) (unsafeRefl) (eqNotLT unsafeRefl)
  84 |   x => LT (LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (ltNotGT $ LT unsafeRefl)
  85 | 
  86 | export
  87 | Total Integer (<) where
  88 |   trichotomy   = comp
  89 |   transLT p q  = strictLT p $ strictLT q $ LT unsafeRefl
  90 | 
  91 | --------------------------------------------------------------------------------
  92 | --          Arithmetics
  93 | --------------------------------------------------------------------------------
  94 | 
  95 | replace' : (0 p : a -> Type) -> (0 _ : x = y) -> p x -> p y
  96 | replace' p prf px = replace {p} prf px
  97 | 
  98 | derive :  {0 a,b : Type}
  99 |        -> (x : a)
 100 |        -> FastDerivation a b
 101 |        -> b
 102 | derive x z = case Calc z of Refl => x
 103 | 
 104 | ---------
 105 | -- Axioms
 106 | 
 107 | ||| This axiom, which only holds for unbounded integers, relates
 108 | ||| addition and the ordering of integers:
 109 | |||
 110 | ||| From `k < m` follows `n + k < n + m` for all integers `k`, `m`, and `n`.
 111 | export
 112 | 0 plusGT : (k,m,n : Integer) -> k < m -> n + k < n + m
 113 | plusGT k m n x = strictLT x $ mkLT unsafeRefl
 114 | 
 115 | ||| This axiom, which only holds for unbounded integers, relates
 116 | ||| multiplication and the ordering of integers:
 117 | |||
 118 | ||| From `0 < m` and `0 < n` follows `0 < m * n` for all integers `m` and `n`.
 119 | export
 120 | 0 multPosPosGT0 : (m,n : Integer) -> 0 < m -> 0 < n -> 0 < m * n
 121 | multPosPosGT0 _ _ p1 p2 = strictLT p1 $ strictLT p2 $ mkLT unsafeRefl
 122 | 
 123 | ||| There is no integer between 0 and 1.
 124 | export
 125 | 0 oneAfterZero : (n : Integer) -> 0 < n -> 1 <= n
 126 | oneAfterZero n gt0 = case comp 1 n of
 127 |   LT x _ _ => Left x
 128 |   EQ _ x _ => Right x
 129 |   GT _ _ x =>
 130 |       strictLT gt0
 131 |     $ strictLT x
 132 |     $ assert_total
 133 |     $ idris_crash "IMPOSSIBLE: Integer between 0 and 1"
 134 | 
 135 | ||| For positive `d`, `mod n d` is a non-negative number
 136 | ||| strictly smaller than `d`.
 137 | export
 138 | 0 modLT : (n,d : Integer) -> 0 < d -> (0 <= mod n d, mod n d < d)
 139 | modLT n d x with (mod n d)
 140 |   _ | 0 = (Right Refl, x)
 141 |   _ | _ = strictLT x (Left $ mkLT unsafeRefl, mkLT unsafeRefl)
 142 | 
 143 | export
 144 | 0 modNegEQ : (n,d : Integer) -> d < 0 -> mod n d === mod n (neg d)
 145 | modNegEQ n d x = strictLT x unsafeRefl
 146 | 
 147 | export
 148 | 0 lawDivMod : (n,d : Integer) -> d /= 0 -> d * div n d + mod n d === n
 149 | lawDivMod n d (Left x)  = strictLT x unsafeRefl
 150 | lawDivMod n d (Right x) = strictLT x unsafeRefl
 151 | 
 152 | ----------------------------
 153 | -- Division
 154 | 
 155 | ||| Safe division.
 156 | export %inline
 157 | sdiv : (n,d : Integer) -> (0 prf : d /= 0) => Integer
 158 | sdiv n d = n `div` d
 159 | 
 160 | ||| Safe modulo.
 161 | export %inline
 162 | smod : (n,d : Integer) -> (0 prf : d /= 0) => Integer
 163 | smod n d = n `mod` d
 164 | 
 165 | --------------------------------------------------------------------------------
 166 | --          Well-Foundedness
 167 | --------------------------------------------------------------------------------
 168 | 
 169 | public export
 170 | 0 BoundedLT : (lowerBound : Integer) -> Integer -> Integer -> Type
 171 | BoundedLT lowerBound x y = (lowerBound <= x, x < y)
 172 | 
 173 | public export
 174 | 0 BoundedGT : (upperBound : Integer) -> Integer -> Integer -> Type
 175 | BoundedGT upperBound x y = (upperBound >= x, x > y)
 176 | 
 177 | ||| Every value of type `Integer` with a fixed lower bound
 178 | ||| is accessible with relation to `(<)`.
 179 | export
 180 | accessLT : (m : Integer) -> Accessible (BoundedLT lb) m
 181 | accessLT m = Access $ \n,lt => accessLT (assert_smaller m n)
 182 | 
 183 | ||| Every value of type `Integer` with a fixed upper bound
 184 | ||| is accessible with relation to `(>)`.
 185 | export
 186 | accessGT : (m : Integer) -> Accessible (BoundedGT ub) m
 187 | accessGT m = Access $ \n,gt => accessGT (assert_smaller m n)
 188 | 
 189 |