git.iko.soy/Idris-dev
on 1280aea help sign in
Idris-dev/lib/Data/Vect/Quantifiers.idr
47 lines 1.7 kB history raw
1module Data.Vect.Quantifiers
3data 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)
7anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
8anyNilAbsurd Here impossible
9anyNilAbsurd There impossible
11anyElim : {xs : Vect a n} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
12anyElim _ f (Here p) = f p
13anyElim f _ (There p) = f p
15any : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect a n) -> Dec (Any P xs)
16any _ Nil = No anyNilAbsurd
17any 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)
24data 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)
28negAnyAll : {P : a -> Type} -> {xs : Vect a n} -> Not (Any P xs) -> All (\x => Not (P x)) xs
29negAnyAll {xs=Nil} _ = Nil
30negAnyAll {xs=(x::xs)} f = (\x => f (Here x)) :: negAnyAll (\x => f (There x))
32notAllHere : {P : a -> Type} -> {xs : Vect a n} -> Not (P x) -> All P (x :: xs) -> _|_
33notAllHere _ Nil impossible
34notAllHere np (p :: _) = np p
36notAllThere : {P : a -> Type} -> {xs : Vect a n} -> Not (All P xs) -> All P (x :: xs) -> _|_
37notAllThere _ Nil impossible
38notAllThere np (_ :: ps) = np ps
40all : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect a n) -> Dec (All P xs)
41all _ Nil = Yes Nil
42all 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')