summaryrefslogtreecommitdiff
path: root/theories/Lists
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Lists')
-rw-r--r--theories/Lists/List.v42
-rw-r--r--theories/Lists/ListDec.v10
-rw-r--r--theories/Lists/ListSet.v10
-rw-r--r--theories/Lists/ListTactics.v10
-rw-r--r--theories/Lists/SetoidList.v16
-rw-r--r--theories/Lists/SetoidPermutation.v16
-rw-r--r--theories/Lists/StreamMemo.v10
-rw-r--r--theories/Lists/Streams.v12
-rw-r--r--theories/Lists/vo.itarget8
9 files changed, 75 insertions, 59 deletions
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.
diff --git a/theories/Lists/ListDec.v b/theories/Lists/ListDec.v
index 3e2eeac0..e7e2cfc8 100644
--- a/theories/Lists/ListDec.v
+++ b/theories/Lists/ListDec.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) *)
(************************************************************************)
(** Decidability results about lists *)
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index 655d3940..cc7d6f55 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.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) *)
(************************************************************************)
(** A library for finite sets, implemented as lists *)
diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v
index 537d5f68..843e3835 100644
--- a/theories/Lists/ListTactics.v
+++ b/theories/Lists/ListTactics.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 Import BinPos.
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index c95fb4d5..0c5fe55b 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -1,10 +1,12 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \VV/ *************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(***********************************************************************)
+(************************************************************************)
+(* * 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 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
Require Export List.
Require Export Sorted.
diff --git a/theories/Lists/SetoidPermutation.v b/theories/Lists/SetoidPermutation.v
index cea3e839..24b96514 100644
--- a/theories/Lists/SetoidPermutation.v
+++ b/theories/Lists/SetoidPermutation.v
@@ -1,10 +1,12 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \VV/ *************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(***********************************************************************)
+(************************************************************************)
+(* * 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 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
Require Import Permutation SetoidList.
(* Set Universe Polymorphism. *)
diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v
index 5a16cc43..57f558de 100644
--- a/theories/Lists/StreamMemo.v
+++ b/theories/Lists/StreamMemo.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 Import Eqdep_dec.
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 1c302b22..8a01b8fb 100644
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.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) *)
(************************************************************************)
Set Implicit Arguments.
@@ -194,7 +196,7 @@ Lemma ForAll_map : forall (P:Stream B -> Prop) (S:Stream A), ForAll (fun s => P
(map s)) S <-> ForAll P (map S).
Proof.
intros P S.
-split; generalize S; clear S; cofix; intros S; constructor;
+split; generalize S; clear S; cofix ForAll_map; intros S; constructor;
destruct H as [H0 H]; firstorder.
Qed.
diff --git a/theories/Lists/vo.itarget b/theories/Lists/vo.itarget
deleted file mode 100644
index 82dd1be8..00000000
--- a/theories/Lists/vo.itarget
+++ /dev/null
@@ -1,8 +0,0 @@
-ListSet.vo
-ListTactics.vo
-List.vo
-ListDec.vo
-SetoidList.vo
-SetoidPermutation.vo
-StreamMemo.vo
-Streams.vo
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 03:49:04 +0000