@@ -0,0 +1,102 @@
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 DecEq () where
25+ decEq () () = Yes refl
26+
27+--------------------------------------------------------------------------------
28+-- Booleans
29+--------------------------------------------------------------------------------
30+
31+total trueNotFalse : True = False -> _|_
32+trueNotFalse refl impossible
33+
34+instance DecEq Bool where
35+ decEq True True = Yes refl
36+ decEq False False = Yes refl
37+ decEq True False = No trueNotFalse
38+ decEq False True = No (negEqSym trueNotFalse)
39+
40+--------------------------------------------------------------------------------
41+-- Nat
42+--------------------------------------------------------------------------------
43+
44+total OnotS : O = S n -> _|_
45+OnotS refl impossible
46+
47+instance DecEq Nat where
48+ decEq O O = Yes refl
49+ decEq O (S _) = No OnotS
50+ decEq (S _) O = No (negEqSym OnotS)
51+ decEq (S n) (S m) with (decEq n m)
52+ | Yes p = Yes $ cong p
53+ | No p = No $ \h : (S n = S m) => p $ succInjective n m h
54+
55+--------------------------------------------------------------------------------
56+-- Maybe
57+--------------------------------------------------------------------------------
58+
59+total nothingNotJust : {x : t} -> (Nothing {a = t} = Just x) -> _|_
60+nothingNotJust refl impossible
61+
62+instance (DecEq t) => DecEq (Maybe t) where
63+ decEq Nothing Nothing = Yes refl
64+ decEq (Just x') (Just y') with (decEq x' y')
65+ | Yes p = Yes $ cong p
66+ | No p = No $ \h : Just x' = Just y' => p $ justInjective h
67+ decEq Nothing (Just _) = No nothingNotJust
68+ decEq (Just _) Nothing = No (negEqSym nothingNotJust)
69+
70+--------------------------------------------------------------------------------
71+-- Either
72+--------------------------------------------------------------------------------
73+
74+total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> _|_
75+leftNotRight refl impossible
76+
77+instance (DecEq a, DecEq b) => DecEq (Either a b) where
78+ decEq {b=b} (Left x') (Left y') with (decEq x' y')
79+ | Yes p = Yes $ cong p
80+ | No p = No $ \h : Left x' = Left y' => p $ leftInjective {b = b} h
81+ decEq (Right x') (Right y') with (decEq x' y')
82+ | Yes p = Yes $ cong p
83+ | No p = No $ \h : Right x' = Right y' => p $ rightInjective {a = a} h
84+ decEq (Left x') (Right y') = No leftNotRight
85+ decEq (Right x') (Left y') = No $ negEqSym leftNotRight
86+
87+--------------------------------------------------------------------------------
88+-- Fin
89+--------------------------------------------------------------------------------
90+
91+total fONotfS : {f : Fin n} -> fO {k = n} = fS f -> _|_
92+fONotfS refl impossible
93+
94+instance DecEq (Fin n) where
95+ decEq fO fO = Yes refl
96+ decEq fO (fS f) = No fONotfS
97+ decEq (fS f) fO = No $ negEqSym fONotfS
98+ decEq (fS f) (fS f') with (decEq f f')
99+ | Yes p = Yes $ cong p
100+ | No p = No $ \h => p $ fSinjective {f = f} {f' = f'} h
101+
102+