git.iko.soy/Idris-dev
on a2fa0fa help sign in
Idris-dev/lib/Data/Vect/Quantifiers.idr
49 lines 1.7 kB history raw
1module Data.Vect.Quantifiers
3import Prelude
5data Any : (P : a -> Type) -> Vect n a -> Type where
6 Here : {P : a -> Type} -> {xs : Vect n a} -> P x -> Any P (x :: xs)
7 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
9anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
10anyNilAbsurd Here impossible
11anyNilAbsurd There impossible
13anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
14anyElim _ f (Here p) = f p
15anyElim f _ (There p) = f p
17any : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (Any P xs)
18any _ Nil = No anyNilAbsurd
19any p (x::xs) with (p x)
20 | Yes prf = Yes (Here prf)
21 | No prf =
22 case any p xs of
23 Yes prf' => Yes (There prf')
24 No prf' => No (anyElim prf' prf)
26data All : (P : a -> Type) -> Vect n a -> Type where
27 Nil : {P : a -> Type} -> All P Nil
28 (::) : {P : a -> Type} -> {xs : Vect n a} -> P x -> All P xs -> All P (x :: xs)
30negAnyAll : {P : a -> Type} -> {xs : Vect n a} -> Not (Any P xs) -> All (\x => Not (P x)) xs
31negAnyAll {xs=Nil} _ = Nil
32negAnyAll {xs=(x::xs)} f = (\x => f (Here x)) :: negAnyAll (\x => f (There x))
34notAllHere : {P : a -> Type} -> {xs : Vect n a} -> Not (P x) -> All P (x :: xs) -> _|_
35notAllHere _ Nil impossible
36notAllHere np (p :: _) = np p
38notAllThere : {P : a -> Type} -> {xs : Vect n a} -> Not (All P xs) -> All P (x :: xs) -> _|_
39notAllThere _ Nil impossible
40notAllThere np (_ :: ps) = np ps
42all : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (All P xs)
43all _ Nil = Yes Nil
44all d (x::xs) with (d x)
45 | No prf = No (notAllHere prf)
46 | Yes prf =
47 case all d xs of
48 Yes prf' => Yes (prf :: prf')
49 No prf' => No (notAllThere prf')