git.iko.soy/Idris-dev
on master help sign in
Merge pull request #282 from JanBessai/DecidableOrder
b4d856aEdwin Brady
lib/Decidable/Decidable.idr+5
compare with master
unifiedsplit
@@ -12,3 +12,8 @@ using (t : Type)
12
12
13 class (Rel p) => Decidable (p : t) where
13 class (Rel p) => Decidable (p : t) where
14 total decide : liftRel Dec
14 total decide : liftRel Dec
15+
16+using (P : Type, p : P)
17+ data Given : Dec P -> Type where
18+ always : Given (Yes p)
19+
lib/Decidable/Order.idr+12−14
@@ -11,17 +11,12 @@ import Decidable.Equality
11-- Preorders and Posets
11-- Preorders and Posets
12--------------------------------------------------------------------------------
12--------------------------------------------------------------------------------
13
13
14−using (t : Type)
15− data Preorder : (t -> t -> Type) -> Type where
14+class Preorder t (po : t -> t -> Type) where
16− transRefl : ((a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c) ->
15+ total transitive : (a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c
17− ((a : t) -> po a a) ->
16+ total reflexive : (a : t) -> po a a
18− Preorder po
19
17
20−
18+class (Preorder t po) => Poset t (po : t -> t -> Type) where
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) ->
19+ total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b
24− Poset po
25
20
26--------------------------------------------------------------------------------
21--------------------------------------------------------------------------------
27-- Natural numbers
22-- Natural numbers
@@ -41,16 +36,17 @@ NatLTEIsTransitive m n (S o) mLTEn (nLTESm nLTEo)
41total NatLTEIsReflexive : (n : Nat) -> NatLTE n n
36total NatLTEIsReflexive : (n : Nat) -> NatLTE n n
42NatLTEIsReflexive _ = nEqn
37NatLTEIsReflexive _ = nEqn
43
38
44−NatLTEIsPreorder : Preorder NatLTE
39+instance Preorder Nat NatLTE where
45−NatLTEIsPreorder = transRefl NatLTEIsTransitive NatLTEIsReflexive
40+ transitive = NatLTEIsTransitive
41+ reflexive = NatLTEIsReflexive
46
42
47total NatLTEIsAntisymmetric : (m : Nat) -> (n : Nat) -> po m n -> po n m -> m = n
43total NatLTEIsAntisymmetric : (m : Nat) -> (n : Nat) -> po m n -> po n m -> m = n
48NatLTEIsAntisymmetric n n nEqn nEqn = refl
44NatLTEIsAntisymmetric n n nEqn nEqn = refl
49NatLTEIsAntisymmetric n m nEqn (nLTESm _) impossible
45NatLTEIsAntisymmetric n m nEqn (nLTESm _) impossible
50NatLTEIsAntisymmetric n m (nLTESm _) nEqn impossible
46NatLTEIsAntisymmetric n m (nLTESm _) nEqn impossible
51
47
52−NatLTEIsPoset : Poset NatLTE
48+instance Poset Nat NatLTE where
53−NatLTEIsPoset = preorderAntisym NatLTEIsPreorder NatLTEIsAntisymmetric
49+ antisymmetric = NatLTEIsAntisymmetric
54
50
55total zeroNeverGreater : {n : Nat} -> NatLTE (S n) O -> _|_
51total zeroNeverGreater : {n : Nat} -> NatLTE (S n) O -> _|_
56zeroNeverGreater {n} (nLTESm _) impossible
52zeroNeverGreater {n} (nLTESm _) impossible
@@ -77,3 +73,5 @@ instance Rel NatLTE where
77instance Decidable NatLTE where
73instance Decidable NatLTE where
78 decide = decideNatLTE
74 decide = decideNatLTE
79
75
76+lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
77+lte m n = decide {p = NatLTE} m n