@@ -0,0 +1,47 @@
1+module Data.Vect.Quantifiers
3+data Any : (P : a -> Type) -> Vect a n -> Type where
4+ Here : {P : a -> Type} -> {xs : Vect a n} -> P x -> Any P (x :: xs)
5+ There : {P : a -> Type} -> {xs : Vect a n} -> Any P xs -> Any P (x :: xs)
7+anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
8+anyNilAbsurd Here impossible
9+anyNilAbsurd There impossible
11+anyElim : {xs : Vect a n} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
12+anyElim _ f (Here p) = f p
13+anyElim f _ (There p) = f p
15+any : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect a n) -> Dec (Any P xs)
16+any _ Nil = No anyNilAbsurd
17+any p (x::xs) with (p x)
18+ | Yes prf = Yes (Here prf)
21+ Yes prf' => Yes (There prf')
22+ No prf' => No (anyElim prf' prf)
24+data All : (P : a -> Type) -> Vect a n -> Type where
25+ Nil : {P : a -> Type} -> All P Nil
26+ (::) : {P : a -> Type} -> {xs : Vect a n} -> P x -> All P xs -> All P (x :: xs)
28+negAnyAll : {P : a -> Type} -> {xs : Vect a n} -> Not (Any P xs) -> All (\x => Not (P x)) xs
29+negAnyAll {xs=Nil} _ = Nil
30+negAnyAll {xs=(x::xs)} f = (\x => f (Here x)) :: negAnyAll (\x => f (There x))
32+notAllHere : {P : a -> Type} -> {xs : Vect a n} -> Not (P x) -> All P (x :: xs) -> _|_
33+notAllHere _ Nil impossible
34+notAllHere np (p :: _) = np p
36+notAllThere : {P : a -> Type} -> {xs : Vect a n} -> Not (All P xs) -> All P (x :: xs) -> _|_
37+notAllThere _ Nil impossible
38+notAllThere np (_ :: ps) = np ps
40+all : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect a n) -> Dec (All P xs)
42+all d (x::xs) with (d x)
43+ | No prf = No (notAllHere prf)
46+ Yes prf' => Yes (prf :: prf')
47+ No prf' => No (notAllThere prf')