Merge pull request idris-lang#193 from david-christiansen/decidable

Decidable equality typeclass

lib/Builtins.idr

@@ -75,6 +75,10 @@ f $ a = f a
 cong : {f : t -> u} -> (a = b) -> f a = f b
 cong refl = refl
 
+data Dec : Type -> Type where
+    Yes : {A : Type} -> A          -> Dec A
+    No  : {A : Type} -> (A -> _|_) -> Dec A
+
 data Bool = False | True
 
 boolElim : Bool -> |(t : a) -> |(f : a) -> a 
@@ -83,10 +87,6 @@ boolElim False t e = e
 
 data so : Bool -> Type where oh : so True
 
-data Equality : {A : Type} -> (x : A) -> (y : A) -> Type where
-    Unequal : {A : Type} -> {x : A} -> {y : A} -> (x = y -> _|_) -> Equality x y
-    Equal : {A : Type} -> {x : A} -> {y : A} -> (x = y) -> Equality x y
-
 syntax if [test] then [t] else [e] = boolElim test t e
 syntax [test] "?" [t] ":" [e] = if test then t else e
 

lib/Decidable/Equality.idr

@@ -0,0 +1,102 @@
+module Decidable.Equality
+
+import Builtins
+
+--------------------------------------------------------------------------------
+-- Utility lemmas
+--------------------------------------------------------------------------------
+
+total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_)
+negEqSym p h = p (sym h)
+
+
+--------------------------------------------------------------------------------
+-- Decidable equality
+--------------------------------------------------------------------------------
+
+class DecEq t where
+  total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
+
+--------------------------------------------------------------------------------
+--- Unit
+--------------------------------------------------------------------------------
+
+instance DecEq () where
+  decEq () () = Yes refl
+
+--------------------------------------------------------------------------------
+-- Booleans
+--------------------------------------------------------------------------------
+
+total trueNotFalse : True = False -> _|_
+trueNotFalse refl impossible
+
+instance DecEq Bool where
+  decEq True  True  = Yes refl
+  decEq False False = Yes refl
+  decEq True  False = No trueNotFalse
+  decEq False True  = No (negEqSym trueNotFalse)
+
+--------------------------------------------------------------------------------
+-- Nat
+--------------------------------------------------------------------------------
+
+total OnotS : O = S n -> _|_
+OnotS refl impossible
+
+instance DecEq Nat where
+  decEq O     O     = Yes refl
+  decEq O     (S _) = No OnotS
+  decEq (S _) O     = No (negEqSym OnotS)
+  decEq (S n) (S m) with (decEq n m)
+    | Yes p = Yes $ cong p
+    | No p = No $ \h : (S n = S m) => p $ succInjective n m h
+
+--------------------------------------------------------------------------------
+-- Maybe
+--------------------------------------------------------------------------------
+
+total nothingNotJust : {x : t} -> (Nothing {a = t} = Just x) -> _|_
+nothingNotJust refl impossible
+
+instance (DecEq t) => DecEq (Maybe t) where
+  decEq Nothing Nothing = Yes refl
+  decEq (Just x') (Just y') with (decEq x' y')
+    | Yes p = Yes $ cong p
+    | No p = No $ \h : Just x' = Just y' => p $ justInjective h
+  decEq Nothing (Just _) = No nothingNotJust
+  decEq (Just _) Nothing = No (negEqSym nothingNotJust)
+
+--------------------------------------------------------------------------------
+-- Either
+--------------------------------------------------------------------------------
+
+total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> _|_
+leftNotRight refl impossible
+
+instance (DecEq a, DecEq b) => DecEq (Either a b) where
+  decEq {b=b} (Left x') (Left y') with (decEq x' y')
+    | Yes p = Yes $ cong p
+    | No p = No $ \h : Left x' = Left y' => p $ leftInjective {b = b} h
+  decEq (Right x') (Right y') with (decEq x' y')
+    | Yes p = Yes $ cong p
+    | No p = No $ \h : Right x' = Right y' => p $ rightInjective {a = a} h
+  decEq (Left x') (Right y') = No leftNotRight
+  decEq (Right x') (Left y') = No $ negEqSym leftNotRight
+
+--------------------------------------------------------------------------------
+-- Fin
+--------------------------------------------------------------------------------
+
+total fONotfS : {f : Fin n} -> fO {k = n} = fS f -> _|_
+fONotfS refl impossible
+
+instance DecEq (Fin n) where
+  decEq fO fO = Yes refl
+  decEq fO (fS f) = No fONotfS
+  decEq (fS f) fO = No $ negEqSym fONotfS
+  decEq (fS f) (fS f') with (decEq f f')
+    | Yes p = Yes $ cong p
+    | No p = No $ \h => p $ fSinjective {f = f} {f' = f'} h
+
+

lib/Prelude/Either.idr

@@ -61,3 +61,16 @@ fromEither (Right r) = r
 maybeToEither : e -> Maybe a -> Either e a
 maybeToEither def (Just j) = Right j
 maybeToEither def Nothing  = Left  def
+
+
+--------------------------------------------------------------------------------
+-- Injectivity of constructors
+--------------------------------------------------------------------------------
+
+total leftInjective : {b : Type} -> {x : a} -> {y : a}
+                    -> (Left {b = b} x = Left {b = b} y) -> (x = y)
+leftInjective refl = refl
+
+total rightInjective : {a : Type} -> {x : b} -> {y : b}
+                     -> (Right {a = a} x = Right {a = a} y) -> (x = y)
+rightInjective refl = refl

lib/Prelude/Fin.idr

@@ -40,3 +40,6 @@ strengthen f = Left f
 last : Fin (S n)
 last {n=O} = fO
 last {n=S _} = fS last
+
+total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'
+fSinjective refl = refl

lib/Prelude/Maybe.idr

@@ -39,6 +39,10 @@ toMaybe : Bool -> a -> Maybe a
 toMaybe True  j = Just j
 toMaybe False j = Nothing
 
+justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y
+justInjective refl = refl
+
+
 --------------------------------------------------------------------------------
 -- Class instances
 --------------------------------------------------------------------------------

lib/base.ipkg

@@ -13,6 +13,8 @@ modules = Builtins, Prelude, IO, System,
 
           System.Concurrency.Raw, System.Concurrency.Process,
 
+          Decidable.Equality,
+
           Language.Reflection,
 
           Data.Morphisms, Data.Bits, Data.Mod2,