git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/libs/base/Decidable/Order.idr
153 lines 5.6 kB history raw
1module Decidable.Order
3import Decidable.Decidable
4import Decidable.Equality
6%access public
8--------------------------------------------------------------------------------
9-- Utility Lemmas
10--------------------------------------------------------------------------------
12--------------------------------------------------------------------------------
13-- Preorders, Posets, total Orders, Equivalencies, Congruencies
14--------------------------------------------------------------------------------
16class Preorder t (po : t -> t -> Type) where
17 total transitive : (a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c
18 total reflexive : (a : t) -> po a a
20class (Preorder t po) => Poset t (po : t -> t -> Type) where
21 total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b
23class (Poset t to) => Ordered t (to : t -> t -> Type) where
24 total order : (a : t) -> (b : t) -> Either (to a b) (to b a)
26class (Preorder t eq) => Equivalence t (eq : t -> t -> Type) where
27 total symmetric : (a : t) -> (b : t) -> eq a b -> eq b a
29class (Equivalence t eq) => Congruence t (f : t -> t) (eq : t -> t -> Type) where
30 total congruent : (a : t) ->
31 (b : t) ->
32 eq a b ->
33 eq (f a) (f b)
35minimum : (Ordered t to) => t -> t -> t
36minimum x y with (order x y)
37 | Left _ = x
38 | Right _ = y
40maximum : (Ordered t to) => t -> t -> t
41maximum x y with (order x y)
42 | Left _ = y
43 | Right _ = x
45--------------------------------------------------------------------------------
46-- Syntactic equivalence (=)
47--------------------------------------------------------------------------------
49instance Preorder t ((=) {A = t} {B = t}) where
50 transitive a b c = trans {a = a} {b = b} {c = c}
51 reflexive a = Refl
53instance Equivalence t ((=) {A = t} {B = t}) where
54 symmetric a b prf = sym prf
56instance Congruence t f ((=) {A = t} {B = t}) where
57 congruent a b = cong {a = a} {b = b} {f = f}
59--------------------------------------------------------------------------------
60-- Natural numbers
61--------------------------------------------------------------------------------
63total LTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->
64 LTE m n -> LTE n o ->
65 LTE m o
66LTEIsTransitive Z n o LTEZero nlteo = LTEZero
67LTEIsTransitive (S m) (S n) (S o) (LTESucc mlten) (LTESucc nlteo) = LTESucc (LTEIsTransitive m n o mlten nlteo)
69total LTEIsReflexive : (n : Nat) -> LTE n n
70LTEIsReflexive Z = LTEZero
71LTEIsReflexive (S n) = LTESucc (LTEIsReflexive n)
73instance Preorder Nat LTE where
74 transitive = LTEIsTransitive
75 reflexive = LTEIsReflexive
77total LTEIsAntisymmetric : (m : Nat) -> (n : Nat) ->
78 LTE m n -> LTE n m -> m = n
79LTEIsAntisymmetric Z Z LTEZero LTEZero = Refl
80LTEIsAntisymmetric (S n) (S m) (LTESucc mLTEn) (LTESucc nLTEm) with (LTEIsAntisymmetric n m mLTEn nLTEm)
81 LTEIsAntisymmetric (S n) (S n) (LTESucc mLTEn) (LTESucc nLTEm) | Refl = Refl
84instance Poset Nat LTE where
85 antisymmetric = LTEIsAntisymmetric
87total zeroNeverGreater : {n : Nat} -> LTE (S n) Z -> Void
88zeroNeverGreater {n} LTEZero impossible
89zeroNeverGreater {n} (LTESucc _) impossible
91total zeroAlwaysSmaller : {n : Nat} -> LTE Z n
92zeroAlwaysSmaller = LTEZero
94total ltesuccinjective : {n : Nat} -> {m : Nat} -> (LTE n m -> Void) -> LTE (S n) (S m) -> Void
95ltesuccinjective {n} {m} disprf (LTESucc nLTEm) = void (disprf nLTEm)
96ltesuccinjective {n} {m} disprf LTEZero impossible
99total decideLTE : (n : Nat) -> (m : Nat) -> Dec (LTE n m)
100decideLTE Z y = Yes LTEZero
101decideLTE (S x) Z = No zeroNeverGreater
102decideLTE (S x) (S y) with (decEq (S x) (S y))
103 | Yes eq = rewrite eq in Yes (reflexive x)
104 | No _ with (decideLTE x y)
105 | Yes nLTEm = Yes (LTESucc nLTEm)
106 | No nGTm = No (ltesuccinjective nGTm)
108instance Decidable [Nat,Nat] LTE where
109 decide = decideLTE
111total
112lte : (m : Nat) -> (n : Nat) -> Dec (LTE m n)
113lte m n = decide {ts = [Nat,Nat]} {p = LTE} m n
115total
116shift : (m : Nat) -> (n : Nat) -> LTE m n -> LTE (S m) (S n)
117shift m n mLTEn = LTESucc mLTEn
119instance Ordered Nat LTE where
120 order Z n = Left LTEZero
121 order m Z = Right LTEZero
122 order (S k) (S j) with (order k j)
123 order (S k) (S j) | Left prf = Left (shift k j prf)
124 order (S k) (S j) | Right prf = Right (shift j k prf)
126----------------------------------------------------------------------------------
127---- Finite numbers
128----------------------------------------------------------------------------------
130using (k : Nat)
131 data FinLTE : Fin k -> Fin k -> Type where
132 FromNatPrf : {m : Fin k} -> {n : Fin k} -> LTE (finToNat m) (finToNat n) -> FinLTE m n
134 instance Preorder (Fin k) FinLTE where
135 transitive m n o (FromNatPrf p1) (FromNatPrf p2) =
136 FromNatPrf (LTEIsTransitive (finToNat m) (finToNat n) (finToNat o) p1 p2)
137 reflexive n = FromNatPrf (LTEIsReflexive (finToNat n))
139 instance Poset (Fin k) FinLTE where
140 antisymmetric m n (FromNatPrf p1) (FromNatPrf p2) =
141 finToNatInjective m n (LTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)
143 instance Decidable [Fin k, Fin k] FinLTE where
144 decide m n with (decideLTE (finToNat m) (finToNat n))
145 | Yes prf = Yes (FromNatPrf prf)
146 | No disprf = No (\ (FromNatPrf prf) => disprf prf)
148 instance Ordered (Fin k) FinLTE where
149 order m n =
150 either (Left . FromNatPrf)
151 (Right . FromNatPrf)
152 (order (finToNat m) (finToNat n))