mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 20:23:11 +03:00
34 lines
1.0 KiB
Idris
34 lines
1.0 KiB
Idris
|
module Decidable.Finite.Fin
|
||
|
|
|
||
|
|
import Data.Nat
|
||
|
|
import Data.Nat.Order
|
||
|
|
import Data.Fin
|
||
|
|
import Decidable.Decidable.Extra
|
||
|
|
import Data.Fin.Extra
|
||
|
|
|
||
|
|
||| Given a decidable predicate on Fin n,
|
||
|
|
||| it's decidable whether any number in Fin n satisfies it.
|
||
|
|
public export
|
||
|
|
finiteDecEx : {n : Nat} -> {0 p : Fin n -> Type} ->
|
||
|
|
(pdec : (k : Fin n) -> Dec (p k)) ->
|
||
|
|
Dec (k ** p k)
|
||
|
|
finiteDecEx {n = Z} pdec = No (absurd . fst)
|
||
|
|
finiteDecEx {n = S n} pdec =
|
||
|
|
case pdec FZ of
|
||
|
|
Yes pz => Yes (FZ ** pz)
|
||
|
|
No npz => case finiteDecEx {n = n} (\ k => pdec (FS k)) of
|
||
|
|
Yes (k ** pk) => Yes (FS k ** pk)
|
||
|
|
No npk => No $ \case
|
||
|
|
(FZ ** pz) => absurd (npz pz)
|
||
|
|
(FS k ** pk) => absurd (npk (k ** pk))
|
||
|
|
|
||
|
|
|
||
|
|
|
||
|
|
||| Given a decidable predicate on Fin n,
|
||
|
|
||| it's decidable whether all numbers in Fin n satisfy it.
|
||
|
|
public export
|
||
|
|
finiteDecAll : {n : Nat} -> {0 p : Fin n -> Type} ->
|
||
|
|
(pdec : (k : Fin n) -> Dec (p k)) ->
|
||
|
|
Dec ((k : Fin n) -> p k)
|
||
|
|
finiteDecAll pdec = notExistsNotForall pdec $ finiteDecEx (\ x => negateDec (pdec x))
|