0 | ||| Implementation of ordering relations for `Nat`ural numbers
 1 | module Data.Nat.Order
 2 |
 3 | import Data.Nat
 4 | import Data.Fun
 5 | import Data.Rel
 6 | import Decidable.Decidable
 7 |
 8 | %default total
 9 |
10 | public export
11 | zeroNeverGreater : Not (LTE (S n) Z)
12 | zeroNeverGreater LTEZero     impossible
13 | zeroNeverGreater (LTESucc _) impossible
14 |
15 | public export
16 | zeroAlwaysSmaller : {n : Nat} -> LTE Z n
17 | zeroAlwaysSmaller = LTEZero
18 |
19 | public export
20 | ltesuccinjective : {0 n, m : Nat} -> Not (LTE n m) -> Not (LTE (S n) (S m))
21 | ltesuccinjective disprf (LTESucc nLTEm) = void (disprf nLTEm)
22 | ltesuccinjective disprf LTEZero         impossible
23 |
24 | ||| If a predicate is decidable then we can decide whether it holds on
25 | ||| a bounded domain.
26 | public export
27 | decideLTBounded :
28 |   {0 p : Nat -> Type} ->
29 |   ((n : Nat) -> Dec (p n)) ->
30 |   (n : Nat) -> Dec ((k : Nat) -> k `LT` n -> p k)
31 | decideLTBounded pdec 0 = Yes (\ k, bnd => absurd bnd)
32 | decideLTBounded pdec (S n) with (pdec 0)
33 |   _ | No np0 = No (\ prf => np0 (prf 0 (LTESucc LTEZero)))
34 |   _ | Yes p0 with (decideLTBounded (\ n => pdec (S n)) n)
35 |     _ | No nprf = No (\ prf => nprf (\ k, bnd => prf (S k) (LTESucc bnd)))
36 |     _ | Yes prf = Yes $ \ k, bnd =>
37 |       case view bnd of
38 |         LTZero => p0
39 |         (LTSucc bnd) => prf _ bnd
40 |
41 | ||| If a predicate is decidable then we can decide whether it holds on
42 | ||| a bounded domain.
43 | public export
44 | decideLTEBounded :
45 |   {0 p : Nat -> Type} ->
46 |   ((n : Nat) -> Dec (p n)) ->
47 |   (n : Nat) -> Dec ((k : Nat) -> k `LTE` n -> p k)
48 | decideLTEBounded pdec n with (decideLTBounded pdec (S n))
49 |   _ | Yes prf = Yes (\ k, bnd => prf k (LTESucc bnd))
50 |   _ | No nprf = No (\ prf => nprf (\ k, bnd => prf k (fromLteSucc bnd)))
51 |
52 | public export
53 | Decidable 2 [Nat,Nat] LTE where
54 |   decide = isLTE
55 |
56 | public export
57 | Decidable 2 [Nat,Nat] LT where
58 |   decide m = isLTE (S m)
59 |
60 | public export
61 | lte : (m : Nat) -> (n : Nat) -> Dec (LTE m n)
62 | lte m n = decide {ts = [Nat,Nat]} {p = LTE} m n
63 |
64 | public export
65 | shift : (m : Nat) -> (n : Nat) -> LTE m n -> LTE (S m) (S n)
66 | shift m n mLTEn = LTESucc mLTEn
67 |