0 | module Decidable.Decidable
 1 |
 2 | import Data.Rel
 3 | import Data.Fun
 4 |
 5 | %default total
 6 |
 7 | public export
 8 | isNo : Dec a -> Bool
 9 | isNo (Yes _) = False
10 | isNo (No _) = True
11 |
12 | public export
13 | isYes : Dec a -> Bool
14 | isYes (Yes _) = True
15 | isYes (No _) = False
16 |
17 | export
18 | Injective Yes where
19 |   injective Refl = Refl
20 |
21 | export
22 | Injective No where
23 |   injective Refl = Refl
24 |
25 | ||| Proof that some `Dec` is actually `Yes`
26 | public export
27 | data IsYes : Dec a -> Type where
28 |   ItIsYes : IsYes (Yes prf)
29 |
30 | public export
31 | Uninhabited (IsYes (No contra)) where
32 |   uninhabited ItIsYes impossible
33 |
34 | ||| Decide whether a 'Dec' is 'Yes'
35 | public export
36 | isItYes : (v : Dec a) -> Dec (IsYes v)
37 | isItYes (Yes _) = Yes ItIsYes
38 | isItYes (No _) = No absurd
39 |
40 | ||| An n-ary relation is decidable if we can make a `Dec`
41 | ||| of its result type for each combination of inputs
42 | public export
43 | IsDecidable : (k : Nat) -> (ts : Vect k Type) -> Rel ts -> Type
44 | IsDecidable k ts p = liftRel ts p Dec
45 |
46 | ||| Interface for decidable n-ary Relations
47 | public export
48 | interface Decidable k ts p where
49 |   total decide : IsDecidable k ts p
50 |
51 | ||| Given a `Decidable` n-ary relation, provides a decision procedure for
52 | ||| this relation.
53 | public export
54 | decision : (ts : Vect k Type) -> (p : Rel ts) -> Decidable k ts p => liftRel ts p Dec
55 | decision ts p = decide {ts} {p}
56 |