0 | module Libraries.Data.List01.Quantifiers
 1 |
 2 | import Data.DPair
 3 | import Libraries.Data.List01
 4 |
 5 | %default total
 6 |
 7 | namespace All
 8 |
 9 |   ||| A proof that all elements of a list satisfy a property. It is a list of
10 |   ||| proofs, corresponding element-wise to the `List`.
11 |   public export
12 |   data All : (0 p : a -> Type) -> List01 ne a -> Type where
13 |     Nil  : All p Nil
14 |     (::) : {0 xs : List01 ne a} -> p x -> All p xs -> All p (x :: xs)
15 |
16 |   ||| Push in the property from the list level with element level
17 |   public export
18 |   pushIn : (xs : List01 ne a) -> (0 _ : All p xs) -> List01 ne $ Subset a p
19 |   pushIn []        []      = []
20 |   pushIn (x :: xs) (p::ps) = Element x p :: pushIn xs ps
21 |
22 |   ||| Pull the elementwise property out to the list level
23 |   public export
24 |   pullOut : (xs : List01 ne $ Subset a p) -> Subset (List01 ne a) (All p)
25 |   pullOut [] = Element [] []
26 |   pullOut (Element x p :: xs) = bimap (x ::) (p ::) $ pullOut xs
27 |