adds lemmas on interactions between existsb, forallb, and app

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12284 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 15 insertions, 0 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 6582b2a87..dca217d50 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1294,6 +1294,14 @@ End Fold_Right_Recursor.
       rewrite IHl; auto with arith.
     Qed.
 
+    Lemma existsb_app : forall l1 l2, 
+      existsb (l1++l2) = existsb l1 || existsb l2.
+    Proof.
+      induction l1; intros l2; simpl.
+        solve[auto].
+      case (f a); simpl; solve[auto].
+    Qed.
+
   (** find whether a boolean function is satisfied by 
     all the elements of a list. *)
 
@@ -1315,6 +1323,13 @@ End Fold_Right_Recursor.
       rewrite H1; auto. 
     Qed.
 
+    Lemma forallb_app :
+      forall l1 l2, forallb (l1++l2) = forallb l1 && forallb l2.
+    Proof.
+      induction l1; simpl.
+        solve[auto].
+      case (f a); simpl; solve[auto].
+    Qed.
   (** [filter] *)
 
     Fixpoint filter (l:list A) : list A :=