git.iko.soy/Idris-dev
on master help sign in
Added typeclass for decidable equality plus instances for commonly-used datatypes
b92b12eDavid Christiansen
lib/Decidable/Equality.idrnew file+105
compare with master
unifiedsplit
@@ -0,0 +1,105 @@
1+module Decidable.Equality
2+
3+import Builtins
4+
5+--------------------------------------------------------------------------------
6+-- Utility lemmas
7+--------------------------------------------------------------------------------
8+
9+total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_)
10+negEqSym p h = p (sym h)
11+
12+
13+--------------------------------------------------------------------------------
14+-- Decidable equality
15+--------------------------------------------------------------------------------
16+
17+class DecEq t where
18+ total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
19+
20+--------------------------------------------------------------------------------
21+--- Unit
22+--------------------------------------------------------------------------------
23+
24+instance Eq () where
25+ () == () = True
26+
27+instance DecEq () where
28+ decEq () () = Yes refl
29+
30+--------------------------------------------------------------------------------
31+-- Booleans
32+--------------------------------------------------------------------------------
33+
34+total trueNotFalse : True = False -> _|_
35+trueNotFalse refl impossible
36+
37+instance DecEq Bool where
38+ decEq True True = Yes refl
39+ decEq False False = Yes refl
40+ decEq True False = No trueNotFalse
41+ decEq False True = No (negEqSym trueNotFalse)
42+
43+--------------------------------------------------------------------------------
44+-- Nat
45+--------------------------------------------------------------------------------
46+
47+total OnotS : O = S n -> _|_
48+OnotS refl impossible
49+
50+instance DecEq Nat where
51+ decEq O O = Yes refl
52+ decEq O (S _) = No OnotS
53+ decEq (S _) O = No (negEqSym OnotS)
54+ decEq (S n) (S m) with (decEq n m)
55+ | Yes p = Yes $ cong p
56+ | No p = No $ \h : (S n = S m) => p $ succInjective n m h
57+
58+--------------------------------------------------------------------------------
59+-- Maybe
60+--------------------------------------------------------------------------------
61+
62+total nothingNotJust : {x : t} -> (Nothing {a = t} = Just x) -> _|_
63+nothingNotJust refl impossible
64+
65+instance (DecEq t) => DecEq (Maybe t) where
66+ decEq Nothing Nothing = Yes refl
67+ decEq (Just x') (Just y') with (decEq x' y')
68+ | Yes p = Yes $ cong p
69+ | No p = No $ \h : Just x' = Just y' => p $ justInjective h
70+ decEq Nothing (Just _) = No nothingNotJust
71+ decEq (Just _) Nothing = No (negEqSym nothingNotJust)
72+
73+--------------------------------------------------------------------------------
74+-- Either
75+--------------------------------------------------------------------------------
76+
77+total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> _|_
78+leftNotRight refl impossible
79+
80+instance (DecEq a, DecEq b) => DecEq (Either a b) where
81+ decEq {b=b} (Left x') (Left y') with (decEq x' y')
82+ | Yes p = Yes $ cong p
83+ | No p = No $ \h : Left x' = Left y' => p $ leftInjective {b = b} h
84+ decEq (Right x') (Right y') with (decEq x' y')
85+ | Yes p = Yes $ cong p
86+ | No p = No $ \h : Right x' = Right y' => p $ rightInjective {a = a} h
87+ decEq (Left x') (Right y') = No leftNotRight
88+ decEq (Right x') (Left y') = No $ negEqSym leftNotRight
89+
90+--------------------------------------------------------------------------------
91+-- Fin
92+--------------------------------------------------------------------------------
93+
94+total fONotfS : {f : Fin n} -> fO {k = n} = fS f -> _|_
95+fONotfS refl impossible
96+
97+instance DecEq (Fin n) where
98+ decEq fO fO = Yes refl
99+ decEq fO (fS f) = No fONotfS
100+ decEq (fS f) fO = No $ negEqSym fONotfS
101+ decEq (fS f) (fS f') with (decEq f f')
102+ | Yes p = Yes $ cong p
103+ | No p = No $ \h => p $ fSinjective {f = f} {f' = f'} h
104+
105+
lib/Prelude/Either.idr+13
@@ -61,3 +61,16 @@ fromEither (Right r) = r
61maybeToEither : e -> Maybe a -> Either e a
61maybeToEither : e -> Maybe a -> Either e a
62maybeToEither def (Just j) = Right j
62maybeToEither def (Just j) = Right j
63maybeToEither def Nothing = Left def
63maybeToEither def Nothing = Left def
64+
65+
66+--------------------------------------------------------------------------------
67+-- Injectivity of constructors
68+--------------------------------------------------------------------------------
69+
70+total leftInjective : {b : Type} -> {x : a} -> {y : a}
71+ -> (Left {b = b} x = Left {b = b} y) -> (x = y)
72+leftInjective refl = refl
73+
74+total rightInjective : {a : Type} -> {x : b} -> {y : b}
75+ -> (Right {a = a} x = Right {a = a} y) -> (x = y)
76+rightInjective refl = refl
lib/Prelude/Fin.idr+3
@@ -40,3 +40,6 @@ strengthen f = Left f
40last : Fin (S n)
40last : Fin (S n)
41last {n=O} = fO
41last {n=O} = fO
42last {n=S _} = fS last
42last {n=S _} = fS last
43+
44+total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'
45+fSinjective refl = refl
lib/Prelude/Maybe.idr+4
@@ -39,6 +39,10 @@ toMaybe : Bool -> a -> Maybe a
39toMaybe True j = Just j
39toMaybe True j = Just j
40toMaybe False j = Nothing
40toMaybe False j = Nothing
41
41
42+justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y
43+justInjective refl = refl
44+
45+
42--------------------------------------------------------------------------------
46--------------------------------------------------------------------------------
43-- Class instances
47-- Class instances
44--------------------------------------------------------------------------------
48--------------------------------------------------------------------------------
lib/base.ipkg+2
@@ -13,6 +13,8 @@ modules = Builtins, Prelude, IO, System,
13
13
14 System.Concurrency.Raw, System.Concurrency.Process,
14 System.Concurrency.Raw, System.Concurrency.Process,
15
15
16+ Decidable.Equality,
17+
16 Language.Reflection,
18 Language.Reflection,
17
19
18 Data.Morphisms, Data.Bits, Data.Mod2,
20 Data.Morphisms, Data.Bits, Data.Mod2,