@@ -0,0 +1,79 @@
1+module Decidable.Order
2+
3+import Decidable.Decidable
4+import Decidable.Equality
5+
6+--------------------------------------------------------------------------------
7+-- Utility Lemmas
8+--------------------------------------------------------------------------------
9+
10+--------------------------------------------------------------------------------
11+-- Preorders and Posets
12+--------------------------------------------------------------------------------
13+
14+using (t : Type)
15+ data Preorder : (t -> t -> Type) -> Type where
16+ transRefl : ((a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c) ->
17+ ((a : t) -> po a a) ->
18+ Preorder po
19+
20+
21+ data Poset : (t -> t -> Type) -> Type where
22+ preorderAntisym : Preorder {t = t} po ->
23+ ((a : t) -> (b : t) -> po a b -> po b a -> a = b) ->
24+ Poset po
25+
26+--------------------------------------------------------------------------------
27+-- Natural numbers
28+--------------------------------------------------------------------------------
29+
30+data NatLTE : Nat -> Nat -> Type where
31+ nEqn : NatLTE n n
32+ nLTESm : NatLTE n m -> NatLTE n (S m)
33+
34+total NatLTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->
35+ NatLTE m n -> NatLTE n o ->
36+ NatLTE m o
37+NatLTEIsTransitive m n n mLTEn (nEqn) = mLTEn
38+NatLTEIsTransitive m n (S o) mLTEn (nLTESm nLTEo)
39+ = nLTESm (NatLTEIsTransitive m n o mLTEn nLTEo)
40+
41+total NatLTEIsReflexive : (n : Nat) -> NatLTE n n
42+NatLTEIsReflexive _ = nEqn
43+
44+NatLTEIsPreorder : Preorder NatLTE
45+NatLTEIsPreorder = transRefl NatLTEIsTransitive NatLTEIsReflexive
46+
47+total NatLTEIsAntisymmetric : (m : Nat) -> (n : Nat) -> po m n -> po n m -> m = n
48+NatLTEIsAntisymmetric n n nEqn nEqn = refl
49+NatLTEIsAntisymmetric n m nEqn (nLTESm _) impossible
50+NatLTEIsAntisymmetric n m (nLTESm _) nEqn impossible
51+
52+NatLTEIsPoset : Poset NatLTE
53+NatLTEIsPoset = preorderAntisym NatLTEIsPreorder NatLTEIsAntisymmetric
54+
55+total zeroNeverGreater : {n : Nat} -> NatLTE (S n) O -> _|_
56+zeroNeverGreater {n} (nLTESm _) impossible
57+zeroNeverGreater {n} nEqn impossible
58+
59+total
60+nGTSm : {n : Nat} -> {m : Nat} -> (NatLTE n m -> _|_) -> NatLTE n (S m) -> _|_
61+nGTSm disprf (nLTESm nLTEm) = FalseElim (disprf nLTEm)
62+nGTSm {n} {m} disprf (nEqn) impossible
63+
64+total
65+decideNatLTE : (n : Nat) -> (m : Nat) -> Dec (NatLTE n m)
66+decideNatLTE O O = Yes nEqn
67+decideNatLTE (S x) O = No zeroNeverGreater
68+decideNatLTE x (S y) with (decEq x (S y))
69+ | Yes eq = rewrite eq in Yes nEqn
70+ | No _ with (decideNatLTE x y)
71+ | Yes nLTEm = Yes (nLTESm nLTEm)
72+ | No nGTm = No (nGTSm nGTm)
73+
74+instance Rel NatLTE where
75+ liftRel P = (n : Nat) -> (m : Nat) -> P (NatLTE n m)
76+
77+instance Decidable NatLTE where
78+ decide = decideNatLTE
79+