From dd4e039129c99558afc9150dc891ac3932e19fc5 Mon Sep 17 00:00:00 2001
From: llee454@gmail.com
Date: Tue, 23 Oct 2018 10:44:16 -0400
Subject: 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.

---
 CREDITS               |  1 +
 theories/Lists/List.v | 26 ++++++++++++++++++++++++++
 2 files changed, 27 insertions(+)

diff --git a/CREDITS b/CREDITS
index f9aa0cb94d..afb5f14c89 100644
--- a/CREDITS
+++ b/CREDITS
@@ -86,6 +86,7 @@ list of persons and groups:
   J.-P. Jouannaud, S. Lescuyer, A. Miquel, J.-F. Monin, P.-Y. Strub
   the Foundations Group (Radboud University, Nijmegen, The Netherlands),
   Laboratoire J.-A. Dieudonné (University of Nice-Sophia Antipolis),
+  L. Lee (https://orcid.org/0000-0002-7128-9257, 2018),
   INRIA-Gallium project,
   the CS dept at Yale, the CIS dept at U. Penn,
   the CSE dept at Harvard, the CS dept at Princeton, the CS dept at MIT
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.
-- 
cgit v1.2.3