git.iko.soy/Idris-dev
on fa29447 help sign in
Idris-dev/lib/Decidable/Equality.idr
102 lines 3.5 kB history raw
1module Decidable.Equality
3import Builtins
5--------------------------------------------------------------------------------
6-- Utility lemmas
7--------------------------------------------------------------------------------
9total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_)
10negEqSym p h = p (sym h)
13--------------------------------------------------------------------------------
14-- Decidable equality
15--------------------------------------------------------------------------------
17class DecEq t where
18 total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
20--------------------------------------------------------------------------------
21--- Unit
22--------------------------------------------------------------------------------
24instance DecEq () where
25 decEq () () = Yes refl
27--------------------------------------------------------------------------------
28-- Booleans
29--------------------------------------------------------------------------------
31total trueNotFalse : True = False -> _|_
32trueNotFalse refl impossible
34instance 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)
40--------------------------------------------------------------------------------
41-- Nat
42--------------------------------------------------------------------------------
44total OnotS : O = S n -> _|_
45OnotS refl impossible
47instance 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
55--------------------------------------------------------------------------------
56-- Maybe
57--------------------------------------------------------------------------------
59total nothingNotJust : {x : t} -> (Nothing {a = t} = Just x) -> _|_
60nothingNotJust refl impossible
62instance (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)
70--------------------------------------------------------------------------------
71-- Either
72--------------------------------------------------------------------------------
74total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> _|_
75leftNotRight refl impossible
77instance (DecEq a, DecEq b) => DecEq (Either a b) where
78 decEq (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
87--------------------------------------------------------------------------------
88-- Fin
89--------------------------------------------------------------------------------
91total fONotfS : {f : Fin n} -> fO {k = n} = fS f -> _|_
92fONotfS refl impossible
94instance 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