Added two proofs to the Lists library. The first, Forall_inv_tail, extends Forall_inv to assert that a property that is true for every element of a list is true for every element in the tail of the list. The second, Exists_impl, parallels Forall_impl and proves that if there exists an element in a list that satisfies a given predicate, and the predicate implies another proposition, then there exists an element in the list that satisfies the implied proposition. Both of these proofs fill natural gaps within the List library.

1 files changed, 26 insertions, 0 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index d5241e622c..af9050da29 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -2250,6 +2250,32 @@ Section Exists_Forall.
 
   End One_predicate.
 
+  Theorem Forall_inv_tail
+    :  forall (P : A -> Prop) (x0 : A) (xs : list A), Forall P (x0 :: xs) -> Forall P xs.
+  Proof.
+    intros P x0 xs H.
+    apply Forall_forall with (l := xs).
+    assert (H0 : forall x : A, In x (x0 :: xs) -> P x).
+    apply Forall_forall with (P := P) (l := x0 :: xs).
+    exact H.
+    assert (H1 : forall (x : A) (H2 : In x xs), P x).
+    intros x H2.
+    apply (H0 x).
+    right.
+    exact H2.
+    intros x H2.
+    apply (H1 x H2).
+  Qed.
+
+  Theorem Exists_impl
+    :  forall (P Q : A -> Prop), (forall x : A, P x -> Q x) -> forall xs : list A, Exists P xs -> Exists Q xs.
+  Proof.
+    intros P Q H xs H0.
+    induction H0.
+    apply (Exists_cons_hd Q x l (H x H0)).
+    apply (Exists_cons_tl x IHExists).
+  Qed.
+
   Lemma Forall_Exists_neg (P:A->Prop)(l:list A) :
    Forall (fun x => ~ P x) l <-> ~(Exists P l).
   Proof.