mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-19 01:01:59 +03:00
81 lines
2.6 KiB
Idris
81 lines
2.6 KiB
Idris
module Data.Vect.Quantifiers
|
|
|
|
import Data.Vect
|
|
|
|
||| 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')
|