From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 theories/Lists/List.v | 42 ++++++++++++++++++++++++++----------------
 1 file changed, 26 insertions(+), 16 deletions(-)

(limited to 'theories/Lists/List.v')

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 30f1dec2..ca5f154e 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 Require Setoid.
@@ -27,7 +29,6 @@ Module ListNotations.
 Notation "[ ]" := nil (format "[ ]") : list_scope.
 Notation "[ x ]" := (cons x nil) : list_scope.
 Notation "[ x ; y ; .. ; z ]" :=  (cons x (cons y .. (cons z nil) ..)) : list_scope.
-Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..) (compat "8.4") : list_scope.
 End ListNotations.
 
 Import ListNotations.
@@ -419,7 +420,7 @@ Section Elts.
   Proof.
     unfold lt; induction n as [| n hn]; simpl.
     - destruct l; simpl; [ inversion 2 | auto ].
-    - destruct l as [| a l hl]; simpl.
+    - destruct l; simpl.
       * inversion 2.
       * intros d ie; right; apply hn; auto with arith.
   Qed.
@@ -1280,7 +1281,7 @@ End Fold_Right_Recursor.
     partition l = ([], []) <-> l = [].
   Proof.
     split.
-    - destruct l as [|a l' _].
+    - destruct l as [|a l'].
       * intuition.
       * simpl. destruct (f a), (partition l'); now intros [= -> ->].
     - now intros ->.
@@ -2110,13 +2111,13 @@ Section Exists_Forall.
       {Exists l} + {~ Exists l}.
     Proof.
       intro Pdec. induction l as [|a l' Hrec].
-      - right. now rewrite Exists_nil.
+      - right. abstract now rewrite Exists_nil.
       - destruct Hrec as [Hl'|Hl'].
         * left. now apply Exists_cons_tl.
         * destruct (Pdec a) as [Ha|Ha].
           + left. now apply Exists_cons_hd.
-          + right. now inversion_clear 1.
-    Qed.
+          + right. abstract now inversion 1.
+    Defined.
 
     Inductive Forall : list A -> Prop :=
       | Forall_nil : Forall nil
@@ -2152,9 +2153,9 @@ Section Exists_Forall.
       - destruct Hrec as [Hl'|Hl'].
         + destruct (Pdec a) as [Ha|Ha].
           * left. now apply Forall_cons.
-          * right. now inversion_clear 1.
-        + right. now inversion_clear 1.
-    Qed.
+          * right. abstract now inversion 1.
+        + right. abstract now inversion 1.
+    Defined.
 
   End One_predicate.
 
@@ -2179,6 +2180,16 @@ Section Exists_Forall.
        * now apply Exists_cons_hd.
   Qed.
 
+  Lemma neg_Forall_Exists_neg (P:A->Prop) (l:list A) :
+    (forall x:A, {P x} + { ~ P x }) ->
+    ~ Forall P l ->
+    Exists (fun x => ~ P x) l.
+  Proof.
+    intro Dec.
+    apply Exists_Forall_neg; intros.
+    destruct (Dec x); auto.
+  Qed.
+
   Lemma Forall_Exists_dec (P:A->Prop) :
     (forall x:A, {P x} + { ~ P x }) ->
     forall l:list A,
@@ -2186,9 +2197,8 @@ Section Exists_Forall.
   Proof.
     intros Pdec l.
     destruct (Forall_dec P Pdec l); [left|right]; trivial.
-    apply Exists_Forall_neg; trivial.
-    intro x. destruct (Pdec x); [now left|now right].
-  Qed.
+    now apply neg_Forall_Exists_neg.
+  Defined.
 
   Lemma Forall_impl : forall (P Q : A -> Prop), (forall a, P a -> Q a) ->
     forall l, Forall P l -> Forall Q l.
-- 
cgit v1.2.3