0 | module Decidable.Decidable.Extra
 1 |
 2 | import Data.Rel
 3 | import Data.Rel.Complement
 4 | import Data.Fun
 5 | import Data.Vect
 6 | import Data.Vect.Quantifiers
 7 | import Data.Fun.Extra
 8 | import Decidable.Decidable
 9 |
10 | %default total
11 |
12 | public export
13 | NotNot : {n : Nat} -> {ts : Vect n Type} -> (r : Rel ts) -> Rel ts
14 | NotNot r = map @{Nary} (Not . Not) r
15 |
16 | [DecidablePartialApplication] {x : t} -> (tts : Decidable (S n) (t :: ts) r) => Decidable n ts (r x) where
17 |   decide = decide @{tts} x
18 |
19 | public export
20 | doubleNegationElimination : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable n ts r =>
21 |   (witness : HVect ts) ->
22 |   uncurry (NotNot {ts} r) witness ->
23 |   uncurry              r  witness
24 | doubleNegationElimination {ts = []} @{dec} [] prfnn =
25 |   case decide @{dec} of
26 |     Yes prf  => prf
27 |     No  prfn => absurd $ prfnn prfn
28 | doubleNegationElimination {ts = t :: ts} @{dec} (w :: witness) prfnn =
29 |   doubleNegationElimination {ts} {r = r w} @{ DecidablePartialApplication @{dec} } witness prfnn
30 |
31 | doubleNegationForall : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable n ts r =>
32 |   All ts (NotNot {ts} r) -> All ts r
33 | doubleNegationForall @{dec} forall_prf =
34 |   let prfnn : (witness : HVect ts) -> uncurry (NotNot {ts} r) witness
35 |       prfnn = uncurryAll forall_prf
36 |       prf   : (witness : HVect ts) -> uncurry              r  witness
37 |       prf witness = doubleNegationElimination @{dec} witness (prfnn witness)
38 |   in curryAll prf
39 |
40 | public export
41 | doubleNegationExists : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable n ts r =>
42 |   Ex ts (NotNot {ts} r) ->
43 |   Ex ts r
44 | doubleNegationExists @{dec} nnxs =
45 |   let witness : HVect ts
46 |       witness = extractWitness nnxs
47 |       witnessingnn : uncurry (NotNot {ts} r) witness
48 |       witnessingnn = extractWitnessCorrect nnxs
49 |       witnessing   : uncurry              r  witness
50 |       witnessing   = doubleNegationElimination @{dec} witness witnessingnn
51 |   in introduceWitness witness witnessing
52 |
53 |
54 |
55 |
56 | decideTransform :
57 |   {n : Nat}
58 |   -> {ts : Vect n Type}
59 |   -> {r : Rel ts}
60 |   -> {t : Type -> Type}
61 |   -> (tDec : {a : Type} -> Dec a -> Dec (t a))
62 |   -> (posDec : IsDecidable n ts r)
63 |   -> IsDecidable n ts (chain {ts} t r)
64 | decideTransform tDec posDec =
65 |   curryAll $ \xs =>
66 |     replace {p = id} (chainUncurry (chain t r) Dec xs) $
67 |       replace {p = Dec} (chainUncurry r t xs) $
68 |         tDec $ replace {p = id} (sym $ chainUncurry r Dec xs) $
69 |           uncurryAll posDec xs
70 |
71 |
72 | ||| Convert a decision about a decidable property into one about its negation.
73 | public export
74 | negateDec : (dec : Dec a) -> Dec (Not a)
75 | negateDec (Yes pf) = No ($ pf)
76 | negateDec (No npf) = Yes npf
77 |
78 | ||| We can turn (Not (Exists Not)) into Forall for decidable types
79 | public export
80 | notExistsNotForall :
81 |   {0 p : a -> Type}
82 |   -> ((x : a) -> Dec (p x))
83 |   -> Dec (x : a ** Not (p x))
84 |   -> Dec ((x : a) -> p x)
85 | notExistsNotForall dec decEx =
86 |   case decEx of
87 |     Yes (x ** nx) => No $ \f => nx $ f x
88 |     No notNot => Yes $ \x => case (dec x) of
89 |       Yes px => px
90 |       No nx => void $ notNot $ (x ** nx)
91 |
92 |
93 | ||| If a relation is decidable, then so is its complement
94 | public export
95 | [DecidableComplement] {n : Nat} -> {ts : Vect n Type} -> {r : Rel ts} -> (posDec : Decidable n ts r) =>
96 |   Decidable n ts (complement {ts} r) where
97 |     decide = decideTransform negateDec (decide @{posDec})
98 |