@@ -0,0 +1,47 @@
1+module Data.Vect.Quantifiers
2+
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)
6+
7+anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
8+anyNilAbsurd Here impossible
9+anyNilAbsurd There impossible
10+
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
14+
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)
19+ | No prf =
20+ case any p xs of
21+ Yes prf' => Yes (There prf')
22+ No prf' => No (anyElim prf' prf)
23+
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)
27+
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))
31+
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
35+
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
39+
40+all : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect a n) -> Dec (All P xs)
41+all _ Nil = Yes Nil
42+all d (x::xs) with (d x)
43+ | No prf = No (notAllHere prf)
44+ | Yes prf =
45+ case all d xs of
46+ Yes prf' => Yes (prf :: prf')
47+ No prf' => No (notAllThere prf')