git.iko.soy/Idris-dev
on d9c3c21 help sign in
Idris-dev/lib/Decidable/Order.idr
87 lines 2.9 kB history raw
1module Decidable.Order
3%access public
5{-
6Doesn't work yet, see note in Decidable.idr
8import Decidable.Decidable
9import Decidable.Equality
11--------------------------------------------------------------------------------
12-- Utility Lemmas
13--------------------------------------------------------------------------------
15--------------------------------------------------------------------------------
16-- Preorders and Posets
17--------------------------------------------------------------------------------
19class Preorder t (po : t -> t -> Type) where
20 total transitive : (a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c
21 total reflexive : (a : t) -> po a a
23class (Preorder t po) => Poset t (po : t -> t -> Type) where
24 total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b
26--------------------------------------------------------------------------------
27-- Natural numbers
28--------------------------------------------------------------------------------
30data NatLTE : Nat -> Nat -> Type where
31 nEqn : NatLTE n n
32 nLTESm : NatLTE n m -> NatLTE n (S m)
34total NatLTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->
35 NatLTE m n -> NatLTE n o ->
36 NatLTE m o
37NatLTEIsTransitive m n n mLTEn (nEqn) = mLTEn
38NatLTEIsTransitive m n (S o) mLTEn (nLTESm nLTEo)
39 = nLTESm (NatLTEIsTransitive m n o mLTEn nLTEo)
41total NatLTEIsReflexive : (n : Nat) -> NatLTE n n
42NatLTEIsReflexive _ = nEqn
44instance Preorder Nat NatLTE where
45 transitive = NatLTEIsTransitive
46 reflexive = NatLTEIsReflexive
48total NatLTEIsAntisymmetric : (m : Nat) -> (n : Nat) ->
49 NatLTE m n -> NatLTE n m -> m = n
50NatLTEIsAntisymmetric n n nEqn nEqn = refl
51NatLTEIsAntisymmetric n m nEqn (nLTESm _) impossible
52NatLTEIsAntisymmetric n m (nLTESm _) nEqn impossible
53NatLTEIsAntisymmetric n m (nLTESm _) (nLTESm _) impossible
55instance Poset Nat NatLTE where
56 antisymmetric = NatLTEIsAntisymmetric
58total zeroNeverGreater : {n : Nat} -> NatLTE (S n) Z -> _|_
59zeroNeverGreater {n} (nLTESm _) impossible
60zeroNeverGreater {n} nEqn impossible
62total
63nGTSm : {n : Nat} -> {m : Nat} -> (NatLTE n m -> _|_) -> NatLTE n (S m) -> _|_
64nGTSm disprf (nLTESm nLTEm) = FalseElim (disprf nLTEm)
65nGTSm {n} {m} disprf (nEqn) impossible
67total
68decideNatLTE : (n : Nat) -> (m : Nat) -> Dec (NatLTE n m)
69decideNatLTE Z Z = Yes nEqn
70decideNatLTE (S x) Z = No zeroNeverGreater
71decideNatLTE x (S y) with (decEq x (S y))
72 | Yes eq = rewrite eq in Yes nEqn
73 | No _ with (decideNatLTE x y)
74 | Yes nLTEm = Yes (nLTESm nLTEm)
75 | No nGTm = No (nGTSm nGTm)
77instance Rel NatLTE where
78 liftRel P = (n : Nat) -> (m : Nat) -> P (NatLTE n m)
80instance Decidable NatLTE where
81 decide = decideNatLTE
83lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
84lte m n = decide {p = NatLTE} m n
86-}