git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/libs/base/Data/Vect/Quantifiers.idr
77 lines 2.9 kB history raw
1module Data.Vect.Quantifiers
3import Data.Vect
5%access public export
7||| A proof that some element of a vector satisfies some property
8|||
9||| @ P the property to be satsified
10data Any : (P : a -> Type) -> Vect n a -> Type where
11 ||| A proof that the satisfying element is the first one in the `Vect`
12 Here : {P : a -> Type} -> {xs : Vect n a} -> P x -> Any P (x :: xs)
13 ||| A proof that the satsifying element is in the tail of the `Vect`
14 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
16||| No element of an empty vector satisfies any property
17anyNilAbsurd : {P : a -> Type} -> Any P Nil -> Void
18anyNilAbsurd (Here _) impossible
19anyNilAbsurd (There _) impossible
21implementation Uninhabited (Any p Nil) where
22 uninhabited = anyNilAbsurd
24||| Eliminator for `Any`
25anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
26anyElim _ f (Here p) = f p
27anyElim f _ (There p) = f p
29||| Given a decision procedure for a property, determine if an element of a
30||| vector satisfies it.
31|||
32||| @ P the property to be satisfied
33||| @ dec the decision procedure
34||| @ xs the vector to examine
35any : {P : a -> Type} -> (dec : (x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (Any P xs)
36any _ Nil = No anyNilAbsurd
37any p (x::xs) with (p x)
38 | Yes prf = Yes (Here prf)
39 | No prf =
40 case any p xs of
41 Yes prf' => Yes (There prf')
42 No prf' => No (anyElim prf' prf)
44||| A proof that all elements of a vector satisfy a property. It is a list of
45||| proofs, corresponding element-wise to the `Vect`.
46data All : (P : a -> Type) -> Vect n a -> Type where
47 Nil : {P : a -> Type} -> All P Nil
48 (::) : {P : a -> Type} -> {xs : Vect n a} -> P x -> All P xs -> All P (x :: xs)
50||| If there does not exist an element that satifies the property, then it is
51||| the case that all elements do not satisfy.
52negAnyAll : {P : a -> Type} -> {xs : Vect n a} -> Not (Any P xs) -> All (\x => Not (P x)) xs
53negAnyAll {xs=Nil} _ = Nil
54negAnyAll {xs=(x::xs)} f = (\x => f (Here x)) :: negAnyAll (\x => f (There x))
56notAllHere : {P : a -> Type} -> {xs : Vect n a} -> Not (P x) -> All P (x :: xs) -> Void
57notAllHere _ Nil impossible
58notAllHere np (p :: _) = np p
60notAllThere : {P : a -> Type} -> {xs : Vect n a} -> Not (All P xs) -> All P (x :: xs) -> Void
61notAllThere _ Nil impossible
62notAllThere np (_ :: ps) = np ps
64||| Given a decision procedure for a property, decide whether all elements of
65||| a vector satisfy it.
66|||
67||| @ P the property
68||| @ dec the decision procedure
69||| @ xs the vector to examine
70all : {P : a -> Type} -> (dec : (x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (All P xs)
71all _ Nil = Yes Nil
72all d (x::xs) with (d x)
73 | No prf = No (notAllHere prf)
74 | Yes prf =
75 case all d xs of
76 Yes prf' => Yes (prf :: prf')
77 No prf' => No (notAllThere prf')