0 | module Decidable.Finite.Fin
 1 |
 2 | import Data.Nat
 3 | import Data.Nat.Order
 4 | import Data.Fin
 5 | import Decidable.Decidable.Extra
 6 | import Data.Fin.Extra
 7 |
 8 | ||| Given a decidable predicate on Fin n,
 9 | ||| it's decidable whether any number in Fin n satisfies it.
10 | public export
11 | finiteDecEx : {n : Nat} -> {0 p : Fin n -> Type} ->
12 |   (pdec : (k : Fin n) -> Dec (p k)) ->
13 |   Dec (k ** p k)
14 | finiteDecEx {n = Z} pdec = No (absurd . fst)
15 | finiteDecEx {n = S n} pdec =
16 |   case pdec FZ of
17 |     Yes pz => Yes (FZ ** pz)
18 |     No npz => case finiteDecEx {n = n} (\ k => pdec (FS k)) of
19 |       Yes (k ** pk) => Yes (FS k ** pk)
20 |       No npk => No $ \case
21 |         (FZ ** pz) => absurd (npz pz)
22 |         (FS k ** pk) => absurd (npk (k ** pk))
23 |
24 |
25 |
26 | ||| Given a decidable predicate on Fin n,
27 | ||| it's decidable whether all numbers in Fin n satisfy it.
28 | public export
29 | finiteDecAll : {n : Nat} -> {0 p : Fin n -> Type} ->
30 |   (pdec : (k : Fin n) -> Dec (p k)) ->
31 |   Dec ((k : Fin n) -> p k)
32 | finiteDecAll pdec  = notExistsNotForall pdec $ finiteDecEx (\ x => negateDec (pdec x))
33 |