diff options
| -rw-r--r-- | CREDITS | 1 | ||||
| -rw-r--r-- | theories/Lists/List.v | 26 |
2 files changed, 27 insertions, 0 deletions
@@ -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. |