diff options
| author | llee454@gmail.com | 2018-10-23 10:44:16 -0400 |
|---|---|---|
| committer | Larry D. Lee Jr | 2018-11-27 22:07:30 -0800 |
| commit | dd4e039129c99558afc9150dc891ac3932e19fc5 (patch) | |
| tree | d53f60de8b0f6ddccd15205bd8b3661dd689e584 | |
| parent | e2444700206fe25a25f7f7cdabf9bc3eddfb2760 (diff) | |
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.
| -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. |