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