@@ -0,0 +1,75 @@
1+module Data.List.Quantifiers
5+||| A proof that some element of a list satisfies some property
7+||| @ P the property to be satsified
8+data Any : (P : a -> Type) -> List a -> Type where
9+ ||| A proof that the satisfying element is the first one in the `List`
10+ Here : {P : a -> Type} -> {xs : List a} -> P x -> Any P (x :: xs)
11+ ||| A proof that the satsifying element is in the tail of the `List`
12+ There : {P : a -> Type} -> {xs : List a} -> Any P xs -> Any P (x :: xs)
14+||| No element of an empty list satisfies any property
15+anyNilAbsurd : {P : a -> Type} -> Any P Nil -> Void
16+anyNilAbsurd (Here _) impossible
17+anyNilAbsurd (There _) impossible
19+instance Uninhabited (Any p Nil) where
20+ uninhabited = anyNilAbsurd
22+||| Eliminator for `Any`
23+anyElim : {xs : List a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
24+anyElim _ f (Here p) = f p
25+anyElim f _ (There p) = f p
27+||| Given a decision procedure for a property, determine if an element of a
28+||| list satisfies it.
30+||| @ P the property to be satisfied
31+||| @ dec the decision procedure
32+||| @ xs the list to examine
33+any : {P : a -> Type} -> (dec : (x : a) -> Dec (P x)) -> (xs : List a) -> Dec (Any P xs)
34+any _ Nil = No anyNilAbsurd
35+any p (x::xs) with (p x)
36+ | Yes prf = Yes (Here prf)
39+ Yes prf' => Yes (There prf')
40+ No prf' => No (anyElim prf' prf)
42+||| A proof that all elements of a list satisfy a property. It is a list of
43+||| proofs, corresponding element-wise to the `List`.
44+data All : (P : a -> Type) -> List a -> Type where
45+ Nil : {P : a -> Type} -> All P Nil
46+ (::) : {P : a -> Type} -> {xs : List a} -> P x -> All P xs -> All P (x :: xs)
48+||| If there does not exist an element that satifies the property, then it is
49+||| the case that all elements do not satisfy.
50+negAnyAll : {P : a -> Type} -> {xs : List a} -> Not (Any P xs) -> All (\x => Not (P x)) xs
51+negAnyAll {xs=Nil} _ = Nil
52+negAnyAll {xs=(x::xs)} f = (\x => f (Here x)) :: negAnyAll (\x => f (There x))
54+notAllHere : {P : a -> Type} -> {xs : List a} -> Not (P x) -> All P (x :: xs) -> Void
55+notAllHere _ Nil impossible
56+notAllHere np (p :: _) = np p
58+notAllThere : {P : a -> Type} -> {xs : List a} -> Not (All P xs) -> All P (x :: xs) -> Void
59+notAllThere _ Nil impossible
60+notAllThere np (_ :: ps) = np ps
62+||| Given a decision procedure for a property, decide whether all elements of
63+||| a list satisfy it.
66+||| @ dec the decision procedure
67+||| @ xs the list to examine
68+all : {P : a -> Type} -> (dec : (x : a) -> Dec (P x)) -> (xs : List a) -> Dec (All P xs)
70+all d (x::xs) with (d x)
71+ | No prf = No (notAllHere prf)
74+ Yes prf' => Yes (prf :: prf')
75+ No prf' => No (notAllThere prf')