Data.List.Quantifiers

Definitions

data Any : (0 _ : (a -> Type)) -> List a -> Type

  A proof that some element of a list satisfies some property
  
  @ p the property to be satisfied

Totality: total
Visibility: public export
Constructors:

Here : p x -> Any p (x :: xs)

  A proof that the satisfying element is the first one in the `List`

There : Any p xs -> Any p (x :: xs)

  A proof that the satisfying element is in the tail of the `List`

Hints:

Uninhabited (Any p [])

Uninhabited (p x) => Uninhabited (Any p xs) => Uninhabited (Any p (x :: xs))

mapProperty : (p x -> q x) -> Any p l -> Any q l

  Modify the property given a pointwise function

Totality: total
Visibility: export

any : ((x : a) -> Dec (p x)) -> (xs : List a) -> Dec (Any p xs)

  Given a decision procedure for a property, determine if an element of a
  list satisfies it.
  
  @ p the property to be satisfied
  @ dec the decision procedure
  @ xs the list to examine

Totality: total
Visibility: public export

toExists : Any p xs -> Exists p

  Forget the membership proof

Totality: total
Visibility: export

data All : (0 _ : (a -> Type)) -> List a -> Type

  A proof that all elements of a list satisfy a property. It is a list of
  proofs, corresponding element-wise to the `List`.

Totality: total
Visibility: public export
Constructors:

Nil : All p []

(::) : p x -> All p xs -> All p (x :: xs)

Hints:

All (Ord . p) xs => All (Eq . p) xs

All (Monoid . p) xs => All (Semigroup . p) xs

All (Eq . p) xs => Eq (All p xs)

All (Monoid . p) xs => Monoid (All p xs)

All (Ord . p) xs => Ord (All p xs)

All (Semigroup . p) xs => Semigroup (All p xs)

All (Show . p) xs => Show (All p xs)

Either (Uninhabited (p x)) (Uninhabited (All p xs)) => Uninhabited (All p (x :: xs))

mapProperty : (p x -> q x) -> All p l -> All q l

  Modify the property given a pointwise function

Totality: total
Visibility: export

imapProperty : (0 i : (a -> Type)) -> (i x => p x -> q x) -> All i as => All p as -> All q as

  Modify the property given a pointwise interface function

Totality: total
Visibility: public export

forget : All (const type) types -> List type

  Forget property source for a homogeneous collection of properties

Totality: total
Visibility: public export

all : ((x : a) -> Dec (p x)) -> (xs : List a) -> Dec (All p xs)

  Given a decision procedure for a property, decide whether all elements of
  a list satisfy it.
  
  @ p the property
  @ dec the decision procedure
  @ xs the list to examine

Totality: total
Visibility: public export

zipPropertyWith : (p x -> q x -> r x) -> All p xs -> All q xs -> All r xs

Totality: total
Visibility: export

HList : List Type -> Type

  A heterogeneous list of arbitrary types

Totality: total
Visibility: public export

splitAt : (xs : List a) -> All p (xs ++ ys) -> (All p xs, All p ys)

Totality: total
Visibility: export

take : (xs : List a) -> All p (xs ++ ys) -> All p xs

Totality: total
Visibility: export

drop : (xs : List a) -> All p (xs ++ ys) -> All p ys

Totality: total
Visibility: export

negAnyAll : Not (Any p xs) -> All (Not . p) xs

  If there does not exist an element that satifies the property, then it is
  the case that all elements do not satisfy it.

Totality: total
Visibility: export

anyNegAll : Any (Not . p) xs -> Not (All p xs)

  If there exists an element that doesn't satify the property, then it is
  not the case that all elements satisfy it.

Totality: total
Visibility: export

allNegAny : All (Not . p) xs -> Not (Any p xs)

  If none of the elements satisfy the property, then not any single one can.

Totality: total
Visibility: export

indexAll : Elem x xs -> All p xs -> p x

  Given a proof of membership for some element, extract the property proof for it

Totality: total
Visibility: public export

pushIn : (xs : List a) -> (0 _ : All p xs) -> List (Subset a p)

  Push in the property from the list level with element level

Totality: total
Visibility: public export

pullOut : List (Subset a p) -> Subset (List a) (All p)

  Pull the elementwise property out to the list level

Totality: total
Visibility: public export

pushInOutInverse : (xs : List a) -> (0 prf : All p xs) -> pullOut (pushIn xs prf) = Element xs prf

Totality: total
Visibility: export

pushOutInInverse : (xs : List (Subset a p)) -> uncurry pushIn (pullOut xs) = xs

Totality: total
Visibility: export

data Interleaving : List a -> List a -> List a -> Type

  Two lists, `xs` and `ys`, whose elements are interleaved in the list `xys`.

Totality: total
Visibility: public export
Constructors:

Nil : Interleaving [] [] []

Left : Interleaving xs ys xys -> Interleaving (x :: xs) ys (x :: xys)

Right : Interleaving xs ys xys -> Interleaving xs (y :: ys) (y :: xys)

record Split : (a -> Type) -> List a -> Type

  A record for storing the result of splitting a list `xys` according to some
  property `p`.
  The `prfs` and `contras` are related to the original list (`xys`) via
  `Interleaving`.
  
  @ xys the list which has been split
  @ p   the property used for the split

Totality: total
Visibility: public export
Constructor: 

MkSplit : Interleaving ayes naws xys => All p ayes -> All (Not . p) naws -> Split p xys

Projections:

.ayes : Split p xys -> List a

.contras : ({rec:0} : Split p xys) -> All (Not . p) (naws {rec:0})

  A proof that all elements in `naws` do not satisfy the property used for
  the split.

.interleaving : ({rec:0} : Split p xys) -> Interleaving (ayes {rec:0}) (naws {rec:0}) xys

.naws : Split p xys -> List a

.prfs : ({rec:0} : Split p xys) -> All p (ayes {rec:0})

  A proof that all elements in `ayes` satisfies the property used for the
  split.

.naws : Split p xys -> List a

Totality: total
Visibility: public export

.ayes : Split p xys -> List a

Totality: total
Visibility: public export

naws : Split p xys -> List a

Totality: total
Visibility: public export

ayes : Split p xys -> List a

Totality: total
Visibility: public export

.interleaving : ({rec:0} : Split p xys) -> Interleaving (ayes {rec:0}) (naws {rec:0}) xys

Totality: total
Visibility: public export

interleaving : ({rec:0} : Split p xys) -> Interleaving (ayes {rec:0}) (naws {rec:0}) xys

Totality: total
Visibility: public export

.prfs : ({rec:0} : Split p xys) -> All p (ayes {rec:0})

  A proof that all elements in `ayes` satisfies the property used for the
  split.

Totality: total
Visibility: public export

prfs : ({rec:0} : Split p xys) -> All p (ayes {rec:0})

  A proof that all elements in `ayes` satisfies the property used for the
  split.

Totality: total
Visibility: public export

.contras : ({rec:0} : Split p xys) -> All (Not . p) (naws {rec:0})

  A proof that all elements in `naws` do not satisfy the property used for
  the split.

Totality: total
Visibility: public export

contras : ({rec:0} : Split p xys) -> All (Not . p) (naws {rec:0})

  A proof that all elements in `naws` do not satisfy the property used for
  the split.

Totality: total
Visibility: public export

splitOnto : ((x : a) -> Dec (p x)) -> (xs : List a) -> Split p acc -> Split p (reverseOnto acc xs)

  Split the list according to the given decidable property, putting the
  resulting proofs and contras in an accumulator.
  
  @ dec a function which returns a decidable property
  @ xs  a list of elements to split
  @ a   the accumulator

Totality: total
Visibility: public export

split : ((x : a) -> Dec (p x)) -> (xs : List a) -> Split p (reverse xs)

  Split the list according to the given decidable property, starting with an
  empty accumulator.
  Use `splitOnto` if you want to specify the accumulator.
  
  @ dec a function which returns a decidable property
  @ xs  a list of elements to split
  @ a   the accumulator

Totality: total
Visibility: public export

decide : ((x : a) -> Either (p x) (q x)) -> (xs : List a) -> Either (All p xs) (Any q xs)

  If any `a` either satisfies p or q then given a List of as,
  either all values satisfy p
  or at least one of them sastifies q

Totality: total
Visibility: public export