From 4e8967788669ad3f06497b46640c687e9525c0e3 Mon Sep 17 00:00:00 2001 From: bertot Date: Wed, 19 Aug 2009 06:24:58 +0000 Subject: 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 --- theories/Lists/List.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) 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 := -- cgit v1.2.3