1
1
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-29 06:32:07 +03:00
Idris2/libs/base/Data/Vect/Quantifiers.idr
2021-06-12 21:06:08 -05:00

83 lines
2.6 KiB
Idris

module Data.Vect.Quantifiers
import Data.Vect
%default total
||| A proof that some element of a vector satisfies some property
|||
||| @ p the property to be satsified
public export
data Any : (0 p : a -> Type) -> Vect n a -> Type where
||| A proof that the satisfying element is the first one in the `Vect`
Here : {0 xs : Vect n a} -> p x -> Any p (x :: xs)
||| A proof that the satsifying element is in the tail of the `Vect`
There : {0 xs : Vect n a} -> Any p xs -> Any p (x :: xs)
export
implementation Uninhabited (Any p Nil) where
uninhabited (Here _) impossible
uninhabited (There _) impossible
||| Eliminator for `Any`
public export
anyElim : {0 xs : Vect n a} -> {0 p : a -> Type} -> (Any p xs -> b) -> (p x -> b) -> Any p (x :: xs) -> b
anyElim _ f (Here p) = f p
anyElim f _ (There p) = f p
||| Given a decision procedure for a property, determine if an element of a
||| vector satisfies it.
|||
||| @ p the property to be satisfied
||| @ dec the decision procedure
||| @ xs the vector to examine
export
any : (dec : (x : a) -> Dec (p x)) -> (xs : Vect n a) -> Dec (Any p xs)
any _ Nil = No uninhabited
any p (x::xs) with (p x)
any p (x::xs) | Yes prf = Yes (Here prf)
any p (x::xs) | No prf =
case any p xs of
Yes prf' => Yes (There prf')
No prf' => No (anyElim prf' prf)
||| A proof that all elements of a vector satisfy a property. It is a list of
||| proofs, corresponding element-wise to the `Vect`.
public export
data All : (0 p : a -> Type) -> Vect n a -> Type where
Nil : All p Nil
(::) : {0 xs : Vect n a} -> p x -> All p xs -> All p (x :: xs)
||| If there does not exist an element that satifies the property, then it is
||| the case that all elements do not satisfy.
export
negAnyAll : {xs : Vect n a} -> Not (Any p xs) -> All (Not . p) xs
negAnyAll {xs=Nil} _ = Nil
negAnyAll {xs=(x::xs)} f = (f . Here) :: negAnyAll (f . There)
export
notAllHere : {0 p : a -> Type} -> {xs : Vect n a} -> Not (p x) -> All p (x :: xs) -> Void
notAllHere _ Nil impossible
notAllHere np (p :: _) = np p
export
notAllThere : {0 p : a -> Type} -> {xs : Vect n a} -> Not (All p xs) -> All p (x :: xs) -> Void
notAllThere _ Nil impossible
notAllThere np (_ :: ps) = np ps
||| Given a decision procedure for a property, decide whether all elements of
||| a vector satisfy it.
|||
||| @ p the property
||| @ dec the decision procedure
||| @ xs the vector to examine
export
all : (dec : (x : a) -> Dec (p x)) -> (xs : Vect n a) -> Dec (All p xs)
all _ Nil = Yes Nil
all d (x::xs) with (d x)
all d (x::xs) | No prf = No (notAllHere prf)
all d (x::xs) | Yes prf =
case all d xs of
Yes prf' => Yes (prf :: prf')
No prf' => No (notAllThere prf')