0 | ||| Implementation of ordering relations for the primitive type `Int`
  1 | ||| This is full of tricks as `Int` is a primitive type that can only
  2 | ||| be interacted with using either literals or built-in functions.
  3 | ||| The exported interface should however be safe.
  4 | module Data.Int.Order
  5 |
  6 | import Data.Order
  7 |
  8 | %default total
  9 |
 10 | ------------------------------------------------------------------------
 11 | -- Introduction
 12 |
 13 | -- The type `Int` is a primitive type in Idris. The only handle we have on
 14 | -- it is provided by built-in functions. This is what we are going to use
 15 | -- to define relations on Int values. For instance, we will declare that
 16 | -- `a` is strictly less than `b` whenever `a < b` is provably equal to `True`.
 17 |
 18 | -- These built-in functions only reduce on literals. This means we will not
 19 | -- be able to rely on their computational behaviour to prove statements in
 20 | -- open contexts.
 21 |
 22 | -- For instance, no amount of pattern-matching will help us prove:
 23 | -- LT_not_EQ : LT a b -> Not (EQ a b)
 24 |
 25 | -- Our solution in this file is to use unsafe primitives to manufacture such
 26 | -- proofs. This means we are going to essentially postulate some *conditional*
 27 | -- results. We do not want such conditional results to reduce to canonical
 28 | -- forms too eagerly.
 29 |
 30 | -- Indeed the statement `GT 0 1 -> EQ 0 1` should be provable because 0 is not
 31 | -- greater than 1. But its proof should not reduce to a constant function
 32 | -- returning the value `Refl` because it is not true that `0` and `1` can be
 33 | -- unified. If the proof were to behave this way, we could, in an absurd context,
 34 | -- coerce values from any type to any other and cause segmentation faults.
 35 |
 36 | -- Our solution is to be extremely wary of proofs that are passed to us
 37 | -- and to only consider returning a magically-crafted output if we have
 38 | -- managed to observe that the input is itself in canonical form i.e. to
 39 | -- have evaluation stuck on open terms.
 40 |
 41 | -- This is the purpose of the `strictX : X -> Lazy c -> c` functions defined in
 42 | -- this file. They all will be waiting until their first argument is in canonical
 43 | -- form before returning their second.
 44 |
 45 |
 46 | ------------------------------------------------------------------------
 47 | -- Utility functions for equality
 48 |
 49 | ||| Pattern-match on an equality proof so that the second argument to
 50 | ||| strictRefl is only returned once the first is canonical.
 51 | export
 52 | strictRefl : a === b -> Lazy c -> c
 53 | strictRefl Refl p = p
 54 |
 55 | ||| Do NOT re-export
 56 | unsafeRefl : {0 a, b : t} -> a === b
 57 | unsafeRefl = believe_me (the (a === a) Refl)
 58 |
 59 | ------------------------------------------------------------------------
 60 | -- LT
 61 |
 62 | namespace LT
 63 |
 64 |   ||| `LT a b` is a proof that `a` is less than `b` which is to say that
 65 |   ||| the function call `a < b` returns `True`.
 66 |   |||
 67 |   ||| NB: we do not re-export the constructor so that users cannot force
 68 |   ||| our magic functions to blow up in absurd contexts by bypassing the
 69 |   ||| safety measures introduced by the `strictX` functions.
 70 |   ||| We do provide functions corresponding to the wrapping and unwrapping
 71 |   ||| of `LT` but, crucially, they do not let people force `LT` proofs to
 72 |   ||| be in canonical form.
 73 |   export
 74 |   data LT : Int -> Int -> Type where
 75 |     MkLT : (a < b) === True -> LT a b
 76 |
 77 |   ||| We may prove `LT a b` by using a proof that `a < b` returns `True`.
 78 |   export
 79 |   mkLT : (a < b) === True -> LT a b
 80 |   mkLT = MkLT
 81 |
 82 |   ||| From a proof that `LT a b`, we may concluded that `a < b` returns `True`.
 83 |   export
 84 |   runLT : LT a b -> (a < b) === True
 85 |   runLT (MkLT eq) = eq
 86 |
 87 |   ||| Do not trust arbitrary `LT` proofs when manufacturing magic ones:
 88 |   ||| be strict!
 89 |   export
 90 |   strictLT : LT a b -> Lazy c -> c
 91 |   strictLT (MkLT p) c = strictRefl p c
 92 |
 93 |   ||| LT is decidable, by virtue of being the reflection of a boolean function
 94 |   export
 95 |   decide : (a, b : Int) -> Dec (LT a b)
 96 |   decide a b with (the (test : Bool ** (a < b) === test) (a < b ** Refl))
 97 |     decide a b | (True ** p) = Yes (MkLT p)
 98 |     decide a b | (False ** p) = No (\ (MkLT q) => absurd (trans (sym p) q))
 99 |
100 |   ||| LT is a transitive relation. This cannot be proven so we use a magic trick.
101 |   export
102 |   trans : LT a b -> LT b c -> LT a (the Int c)
103 |   trans p q = strictLT p $ strictLT q $ MkLT unsafeRefl
104 |
105 |   ||| LT is an irreflexive relation.
106 |   ||| The crash will never happen because the `LT a a` argument will never reduce
107 |   ||| to a canonical form (unless the built-in function (<) is buggy).
108 |   export
109 |   irrefl : Not (LT a a)
110 |   irrefl p = strictLT p
111 |            $ assert_total $ idris_crash "IMPOSSIBLE: LT is irreflexive"
112 |
113 | ------------------------------------------------------------------------
114 | -- GT
115 |
116 | ||| GT is defined in terms of LT to avoid code duplication
117 | public export
118 | GT : Int -> Int -> Type
119 | GT = flip LT
120 |
121 | export
122 | LT_not_GT : LT a b -> Not (GT a b)
123 | LT_not_GT p q = irrefl (trans p q)
124 |
125 | export
126 | GT_not_LT : GT a b -> Not (LT a b)
127 | GT_not_LT = flip LT_not_GT
128 |
129 | ------------------------------------------------------------------------
130 | -- EQ
131 |
132 | namespace EQ
133 |
134 |   ||| `EQ a b` is a proof that `a` is equal to `b` which is to say that
135 |   ||| the function call `a == b` returns `True`.
136 |   |||
137 |   ||| NB: we do not re-export the constructor so that users cannot force
138 |   ||| our magic functions to blow up in absurd contexts by bypassing the
139 |   ||| safety measures introduced by the `strictX` functions.
140 |   ||| We do provide functions corresponding to the wrapping and unwrapping
141 |   ||| of `EQ` but, crucially, they do not let people force `EQ` proofs to
142 |   ||| be in canonical form.
143 |   export
144 |   data EQ : Int -> Int -> Type where
145 |     MkEQ : (a == b) === True -> EQ a b
146 |
147 |   ||| We may prove `EQ a b` by using a proof that `a == b` returns `True`.
148 |   export
149 |   mkEQ : (a == b) === True -> EQ a b
150 |   mkEQ = MkEQ
151 |
152 |   ||| From a proof that `EQ a b`, we may concluded that `a == b` returns `True`.
153 |   export
154 |   runEQ : EQ a b -> (a == b) === True
155 |   runEQ (MkEQ eq) = eq
156 |
157 |   ||| Do not trust arbitrary `EQ` proofs when manufacturing magic ones:
158 |   ||| be strict!
159 |   export
160 |   strictEQ : EQ a b -> Lazy c -> c
161 |   strictEQ (MkEQ p) c = strictRefl p c
162 |
163 |   ||| EQ is decidable, by virtue of being the reflection of a boolean function
164 |   export
165 |   decide : (a, b : Int) -> Dec (EQ a b)
166 |   decide a b with (the (test : Bool ** (a == b) === test) (a == b ** Refl))
167 |     decide a b | (True  ** p) = Yes (MkEQ p)
168 |     decide a b | (False ** p) = No (\ (MkEQ q) => absurd (trans (sym p) q))
169 |
170 |   ||| EQ is a reflexive relation
171 |   export
172 |   refl : EQ a a
173 |   refl = MkEQ unsafeRefl
174 |
175 |   ||| EQ is substitutive
176 |   export
177 |   elimEQ : (0 p : Int -> Type) -> EQ a b -> p a -> p b
178 |   elimEQ _ p v = strictEQ p $ believe_me v
179 |
180 |   ||| EQ implies propositional equality
181 |   export
182 |   reflect : EQ a b -> a === b
183 |   reflect p = elimEQ (\ b => a === b) p Refl
184 |
185 |   ||| EQ is a symmetric relation
186 |   export
187 |   sym : EQ a b -> EQ b a
188 |   sym p = elimEQ (\ b => EQ b a) p refl
189 |
190 |   ||| EQ is a transitive relation
191 |   export
192 |   trans : EQ a b -> EQ b c -> EQ a c
193 |   trans p q = elimEQ (\ b => EQ b c) (sym p) q
194 |
195 | export
196 | trans_LT_EQ : LT a b -> EQ b c -> LT a c
197 | trans_LT_EQ p q = elimEQ (LT a) q p
198 |
199 | export
200 | trans_EQ_LT : EQ a b -> LT b c -> LT a c
201 | trans_EQ_LT p q = elimEQ (\ b => LT b c) (sym p) q
202 |
203 | export
204 | LT_not_EQ : LT a b -> Not (EQ a b)
205 | LT_not_EQ p q = irrefl (trans_LT_EQ p (sym q))
206 |
207 | export
208 | EQ_not_LT : EQ a b -> Not (LT a b)
209 | EQ_not_LT = flip LT_not_EQ
210 |
211 | export
212 | EQ_not_GT : EQ a b -> Not (GT a b)
213 | EQ_not_GT = EQ_not_LT . sym
214 |
215 | export
216 | GT_not_EQ : GT a b -> Not (EQ a b)
217 | GT_not_EQ = flip EQ_not_GT
218 |
219 | ------------------------------------------------------------------------
220 | -- LTE
221 |
222 | namespace LTE
223 |
224 |   ||| `LTE a b` is a proof that `a` is less or equal to `b` which is to say that
225 |   ||| the function call `a < b` or `a == b` returns `True`.
226 |   |||
227 |   ||| NB: we do not re-export the constructor so that users cannot force
228 |   ||| our magic functions to blow up in absurd contexts by bypassing the
229 |   ||| safety measures introduced by the `strictX` functions.
230 |   export
231 |   data LTE : Int -> Int -> Type where
232 |     MkLT : (a < b)  === True -> LTE a b
233 |     MkEQ : (a == b) === True -> LTE a b
234 |
235 |   ||| Unwrap an LTE proof to get either an LT or an EQ one
236 |   export
237 |   runLTE : LTE a b -> Either (LT a b) (EQ a b)
238 |   runLTE (MkLT p) = Left (mkLT p)
239 |   runLTE (MkEQ p) = Right (mkEQ p)
240 |
241 |   ||| Do not trust arbitrary `LTE` proofs when manufacturing magic ones:
242 |   ||| be strict!
243 |   export
244 |   strictLTE : LTE a b -> Lazy c -> c
245 |   strictLTE (MkLT p) q = strictRefl p q
246 |   strictLTE (MkEQ p) q = strictRefl p q
247 |
248 |   ||| LTE is decidable by virture of both LT and EQ being decidable
249 |   export
250 |   decide : (a, b : Int) -> Dec (LTE a b)
251 |   decide a b with (LT.decide a b)
252 |     decide a b | Yes p = Yes (MkLT (runLT p))
253 |     decide a b | No notLT with (EQ.decide a b)
254 |       decide a b | No notLT | Yes p = Yes (MkEQ (runEQ p))
255 |       decide a b | No notLT | No notEQ = No $ \ case
256 |         MkLT p => notLT (mkLT p)
257 |         MkEQ p => notEQ (mkEQ p)
258 |
259 |   ||| LTE is a reflexive relation
260 |   export
261 |   refl : LTE a a
262 |   refl = MkEQ unsafeRefl
263 |
264 |   export
265 |   trans_LT_LTE : LT a b -> LTE b c -> LT a c
266 |   trans_LT_LTE p (MkLT q) = trans p (mkLT q)
267 |   trans_LT_LTE p (MkEQ q) = trans_LT_EQ p (mkEQ q)
268 |
269 |   export
270 |   trans_LTE_LT : LTE a b -> LT b c -> LT a c
271 |   trans_LTE_LT (MkLT p) q = trans (mkLT p) q
272 |   trans_LTE_LT (MkEQ p) q = trans_EQ_LT (mkEQ p) q
273 |
274 |   export
275 |   inject_LT_LTE : LT a b -> LTE a b
276 |   inject_LT_LTE = MkLT . runLT
277 |
278 |   export
279 |   inject_EQ_LTE : EQ a b -> LTE a b
280 |   inject_EQ_LTE p = MkEQ (runEQ p)
281 |
282 |   ||| LTE is a transitive relation
283 |   export
284 |   trans : LTE a b -> LTE b c -> LTE a c
285 |   trans (MkLT p) q = inject_LT_LTE (trans_LT_LTE (mkLT p) q)
286 |   trans p (MkLT q) = inject_LT_LTE (trans_LTE_LT p (mkLT q))
287 |   trans (MkEQ p) (MkEQ q) = inject_EQ_LTE (trans (mkEQ p) (mkEQ q))
288 |
289 |   ||| LTE is an antisymmetric relation
290 |   export
291 |   antisym : LTE a b -> LTE b a -> EQ a b
292 |   antisym (MkEQ p) _ = mkEQ p
293 |   antisym _ (MkEQ p) = EQ.sym (mkEQ p)
294 |   antisym (MkLT p) (MkLT q) = absurd $ LT.irrefl (LT.trans (mkLT p) (mkLT q))
295 |
296 | ------------------------------------------------------------------------
297 | -- GTE
298 |
299 | ||| GTE is defined in terms of LTE to avoid code duplication
300 | public export
301 | GTE : Int -> Int -> Type
302 | GTE = flip LTE
303 |
304 | ------------------------------------------------------------------------
305 | -- Trichotomy and other decidability results
306 |
307 | ||| Any pair of Ints is related either via LT, EQ, or GT
308 | export
309 | trichotomous : (a, b : Int) -> Trichotomous LT EQ GT a b
310 | trichotomous a b with (LTE.decide a b)
311 |   trichotomous a b | Yes lte = case runLTE lte of
312 |     Left lt  => MkLT lt (LT_not_EQ lt) (LT_not_GT lt)
313 |     Right eq => MkEQ (EQ_not_LT eq) eq (EQ_not_GT eq)
314 |   trichotomous a b | No notLTE = let gt = mkLT unsafeRefl in MkGT (GT_not_LT gt) (GT_not_EQ gt) gt
315 |
316 | ||| Any pair of Ints is related either via LT or GTE
317 | export
318 | decide_LT_GTE : (a, b : Int) -> Either (LT a b) (GTE a b)
319 | decide_LT_GTE a b with (trichotomous a b)
320 |   decide_LT_GTE a b | MkLT lt _ _ = Left lt
321 |   decide_LT_GTE a b | MkEQ _ eq _ = Right (inject_EQ_LTE (sym eq))
322 |   decide_LT_GTE a b | MkGT _ _ gt = Right (inject_LT_LTE gt)
323 |
324 | ||| Any pair of Ints is related either via LTE or GT
325 | export
326 | decide_LTE_GT : (a, b : Int) -> Either (LTE a b) (GT a b)
327 | decide_LTE_GT a b with (trichotomous a b)
328 |   decide_LTE_GT a b | MkLT lt _ _ = Left (inject_LT_LTE lt)
329 |   decide_LTE_GT a b | MkEQ _ eq _ = Left (inject_EQ_LTE eq)
330 |   decide_LTE_GT a b | MkGT _ _ gt = Right gt
331 |
332 | ------------------------------------------------------------------------
333 | -- Some properties
334 |
335 | ||| Adding one to a strictly smaller Int, yields a smaller Int
336 | export
337 | suc_LT_LTE : {a, b : Int} -> LT a b -> LTE (a + 1) b
338 | suc_LT_LTE p with (the (test : Bool ** (a + 1 == b) === test) (a + 1 == b ** Refl))
339 |   suc_LT_LTE p | (True  ** q) = inject_EQ_LTE $ mkEQ q
340 |   suc_LT_LTE p | (False ** q) = strictLT p $ inject_LT_LTE $ mkLT unsafeRefl
341 |
342 | ||| Subtracting one to a strictly larger Int, yields a larger Int
343 | export
344 | pred_LT_LTE : {a, b : Int} -> LT a b -> LTE a (b - 1)
345 | pred_LT_LTE p with (the (test : Bool ** (a == b - 1) === test) (a == b - 1 ** Refl))
346 |   pred_LT_LTE p | (True  ** q) = inject_EQ_LTE $ mkEQ q
347 |   pred_LT_LTE p | (False ** q) = strictLT p $ inject_LT_LTE $ mkLT unsafeRefl
348 |
349 | ||| Adding one to an Int yields a strictly larger one,
350 | ||| provided there is no overflow
351 | export
352 | sucBounded : LT a b -> LT a (a + 1)
353 | sucBounded p = strictLT p $ mkLT unsafeRefl
354 |