git.iko.soy/Idris-dev
on d79a445 help sign in
Idris-dev/lib/Decidable/Order.idr
77 lines 2.7 kB history raw
1module Decidable.Order
3import Decidable.Decidable
4import Decidable.Equality
6--------------------------------------------------------------------------------
7-- Utility Lemmas
8--------------------------------------------------------------------------------
10--------------------------------------------------------------------------------
11-- Preorders and Posets
12--------------------------------------------------------------------------------
14class Preorder t (po : t -> t -> Type) where
15 total transitive : (a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c
16 total reflexive : (a : t) -> po a a
18class (Preorder t po) => Poset t (po : t -> t -> Type) where
19 total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b
21--------------------------------------------------------------------------------
22-- Natural numbers
23--------------------------------------------------------------------------------
25data NatLTE : Nat -> Nat -> Type where
26 nEqn : NatLTE n n
27 nLTESm : NatLTE n m -> NatLTE n (S m)
29total NatLTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->
30 NatLTE m n -> NatLTE n o ->
31 NatLTE m o
32NatLTEIsTransitive m n n mLTEn (nEqn) = mLTEn
33NatLTEIsTransitive m n (S o) mLTEn (nLTESm nLTEo)
34 = nLTESm (NatLTEIsTransitive m n o mLTEn nLTEo)
36total NatLTEIsReflexive : (n : Nat) -> NatLTE n n
37NatLTEIsReflexive _ = nEqn
39instance Preorder Nat NatLTE where
40 transitive = NatLTEIsTransitive
41 reflexive = NatLTEIsReflexive
43total NatLTEIsAntisymmetric : (m : Nat) -> (n : Nat) -> po m n -> po n m -> m = n
44NatLTEIsAntisymmetric n n nEqn nEqn = refl
45NatLTEIsAntisymmetric n m nEqn (nLTESm _) impossible
46NatLTEIsAntisymmetric n m (nLTESm _) nEqn impossible
48instance Poset Nat NatLTE where
49 antisymmetric = NatLTEIsAntisymmetric
51total zeroNeverGreater : {n : Nat} -> NatLTE (S n) O -> _|_
52zeroNeverGreater {n} (nLTESm _) impossible
53zeroNeverGreater {n} nEqn impossible
55total
56nGTSm : {n : Nat} -> {m : Nat} -> (NatLTE n m -> _|_) -> NatLTE n (S m) -> _|_
57nGTSm disprf (nLTESm nLTEm) = FalseElim (disprf nLTEm)
58nGTSm {n} {m} disprf (nEqn) impossible
60total
61decideNatLTE : (n : Nat) -> (m : Nat) -> Dec (NatLTE n m)
62decideNatLTE O O = Yes nEqn
63decideNatLTE (S x) O = No zeroNeverGreater
64decideNatLTE x (S y) with (decEq x (S y))
65 | Yes eq = rewrite eq in Yes nEqn
66 | No _ with (decideNatLTE x y)
67 | Yes nLTEm = Yes (nLTESm nLTEm)
68 | No nGTm = No (nGTSm nGTm)
70instance Rel NatLTE where
71 liftRel P = (n : Nat) -> (m : Nat) -> P (NatLTE n m)
73instance Decidable NatLTE where
74 decide = decideNatLTE
76lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
77lte m n = decide {p = NatLTE} m n