0 | ||| A form of decidable equality compatible with Eq
  1 | module Decidable.Equality.Eq
  2 |
  3 | import Data.Nat
  4 | import Decidable.Equality
  5 |
  6 |
  7 | ||| Compatibility between a boolean and a proposition
  8 | public export
  9 | data Decides : Bool -> Type -> Type where
 10 |   Yes : p -> Decides True p
 11 |   No : (p -> Void) -> Decides False p
 12 |
 13 |
 14 | ||| Decidable equality compatible with an Eq instance
 15 | public export
 16 | interface Eq x => EqIsDec x where
 17 |   eqDecides : (a : x) -> (b : x) -> Decides (a == b) (a = b)
 18 |
 19 |
 20 | public export
 21 | decidesToDec : Decides t p -> Dec p
 22 | decidesToDec (Yes x) = Yes x
 23 | decidesToDec (No x) = No x
 24 |
 25 |
 26 | public export
 27 | EqIsDec () where
 28 |   eqDecides () () = Yes Refl
 29 |
 30 | public export
 31 | EqIsDec Bool where
 32 |   eqDecides True True = Yes Refl
 33 |   eqDecides False False = Yes Refl
 34 |   eqDecides True False = No absurd
 35 |   eqDecides False True = No absurd
 36 |
 37 |
 38 | public export
 39 | eqPrec : S l = S r -> l = r
 40 | eqPrec Refl = Refl
 41 |
 42 | public export
 43 | neSucc : (l = r -> Void) -> S l = S r -> Void
 44 | neSucc f p = f (eqPrec p)
 45 |
 46 | public export
 47 | decSucc : Decides (m == n) (m = n) -> Decides (S m == S n) (S m = S n)
 48 | decSucc d with 0 (m == n)
 49 |   decSucc (Yes r) | True = Yes (cong S r)
 50 |   decSucc (No r) | False = No (neSucc r)
 51 |
 52 |
 53 | public export
 54 | EqIsDec Nat where
 55 |   eqDecides 0 0 = Yes Refl
 56 |   eqDecides (S m) 0 = No absurd
 57 |   eqDecides 0 (S n) = No absurd
 58 |   eqDecides (S m) (S n) = decSucc (eqDecides m n)
 59 |
 60 |
 61 | uncongL : Left x = Left y -> x = y
 62 | uncongL Refl = Refl
 63 |
 64 | uncongR : Right x = Right y -> x = y
 65 | uncongR Refl = Refl
 66 |
 67 | public export
 68 | (EqIsDec a, EqIsDec b) => EqIsDec (Either a b) where
 69 |   eqDecides (Left x) (Left y) with (eqDecides x y) | (x == y)
 70 |     eqDecides (Left x) (Left y) | No p | False = No (p . uncongL)
 71 |     eqDecides (Left x) (Left y) | Yes p | True = Yes (cong Left p)
 72 |   eqDecides (Left x) (Right y) = No absurd
 73 |   eqDecides (Right x) (Left y) = No absurd
 74 |   eqDecides (Right x) (Right y) with (eqDecides x y) | (x == y)
 75 |     eqDecides (Right x) (Right y) | No p | False = No (p . uncongR)
 76 |     eqDecides (Right x) (Right y) | Yes p | True = Yes (cong Right p)
 77 |
 78 |
 79 |
 80 |
 81 | congFst : (x1,y1) = (x2,y2) -> x1 = x2
 82 | congFst Refl = Refl
 83 |
 84 | congSnd : (x1,y1) = (x2,y2) -> y1 = y2
 85 | congSnd Refl = Refl
 86 |
 87 | public export
 88 | (EqIsDec a, EqIsDec b) => EqIsDec (a, b) where
 89 |   eqDecides (x1,y1) (x2,y2) with (eqDecides x1 x2) | (x1 == x2)
 90 |     eqDecides (x1,y1) (x2,y2) | No p | False = No (p . congFst)
 91 |     eqDecides (x1,y1) (x2,y2) | Yes p | True with (eqDecides y1 y2) | (y1 == y2)
 92 |       eqDecides (x1,y1) (x2,y2) | Yes p | True | No q | False = No (q . congSnd)
 93 |       eqDecides (x1,y1) (x1,y1) | Yes Refl | True | Yes Refl | True = Yes Refl
 94 |
 95 | {-
 96 | -- Fails to find an Eq instance for DPair
 97 | public export
 98 | (EqIsDec a, (x : a) -> EqIsDec (b x)) => EqIsDec (DPair a b) where
 99 |   eqDecides (MkDPair x1 y1) (MkDPair x2 y2) = ?what
100 | -}
101 |
102 |
103 | nilNeqCons : ([] = a :: as) -> Void
104 | nilNeqCons Refl impossible
105 |
106 | consNeqNil : (a :: as = []) -> Void
107 | consNeqNil Refl impossible
108 |
109 | uncongHead : {0 as : List x} -> {0 bs : List x} -> (a :: as = b :: bs) -> a = b
110 | uncongHead Refl = Refl
111 |
112 | uncongTail : {0 as : List x} -> {0 bs : List x} -> (a :: as = b :: bs) -> as = bs
113 | uncongTail Refl = Refl
114 |
115 | public export
116 | EqIsDec a => EqIsDec (List a) where
117 |   eqDecides [] [] = Yes Refl
118 |   eqDecides [] (_ :: _) = No nilNeqCons
119 |   eqDecides (_ :: _) [] = No consNeqNil
120 |   eqDecides (x :: xs) (y :: ys) with (eqDecides x y) | (x == y)
121 |     eqDecides (x :: xs) (y :: ys) | No p | False = No (p . uncongHead)
122 |     eqDecides (x :: xs) (y :: ys) | Yes p | True with (eqDecides xs ys) | (xs == ys)
123 |       eqDecides (x :: xs) (y :: ys) | Yes p | True | No q | False = No (q . uncongTail)
124 |       eqDecides (x :: xs) (x :: xs) | Yes Refl | True | Yes Refl | True = Yes Refl
125 |