Add list lemmas (#491)

libs/base/Data/List.idr

@@ -1,5 +1,7 @@
 module Data.List
 
+import Data.Nat
+
 public export
 isNil : List a -> Bool
 isNil [] = True
@@ -620,3 +622,12 @@ revAppend (v :: vs) ns
           rewrite sym (revAppend vs ns) in
             rewrite appendAssociative (reverse ns) (reverse vs) [v] in
               Refl
+
+export
+dropFusion : (n, m : Nat) -> (l : List t) -> drop n (drop m l) = drop (n+m) l
+dropFusion  Z     m    l      = Refl
+dropFusion (S n)  Z    l      = rewrite plusZeroRightNeutral n in Refl
+dropFusion (S n) (S m) []     = Refl
+dropFusion (S n) (S m) (x::l) = rewrite plusAssociative n 1 m in
+                                rewrite plusCommutative n 1 in
+                                dropFusion (S n) m l

libs/base/Data/List/Elem.idr

@@ -76,3 +76,9 @@ indexElem : Nat -> (xs : List a) -> Maybe (x ** Elem x xs)
 indexElem  _    []        = Nothing
 indexElem  Z    (y :: _)  = Just (y ** Here)
 indexElem (S n) (_ :: ys) = map (\(x ** p) => (x ** There p)) (indexElem n ys)
+
+||| Lift the membership proof to a mapped list
+export
+elemMap : (0 f : a -> b) -> Elem x xs -> Elem (f x) (map f xs)
+elemMap f  Here      = Here
+elemMap f (There el) = There $ elemMap f el

libs/base/Data/List/Quantifiers.idr

@@ -78,3 +78,9 @@ export
 indexAll : Elem x xs -> All p xs -> p x
 indexAll  Here     (p::_  ) = p
 indexAll (There e) ( _::ps) = indexAll e ps
+
+||| Modify the property given a pointwise function
+export
+mapProperty : (f : {0 x : a} -> p x -> q x) -> All p l -> All q l
+mapProperty f [] = []
+mapProperty f (p::pl) = f p :: mapProperty f pl