summaryrefslogtreecommitdiff
path: root/theories/Sets
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Sets')
-rw-r--r--theories/Sets/Classical_sets.v10
-rw-r--r--theories/Sets/Constructive_sets.v10
-rw-r--r--theories/Sets/Cpo.v10
-rw-r--r--theories/Sets/Ensembles.v10
-rw-r--r--theories/Sets/Finite_sets.v10
-rw-r--r--theories/Sets/Finite_sets_facts.v10
-rw-r--r--theories/Sets/Image.v10
-rw-r--r--theories/Sets/Infinite_sets.v10
-rw-r--r--theories/Sets/Integers.v10
-rw-r--r--theories/Sets/Multiset.v14
-rw-r--r--theories/Sets/Partial_Order.v10
-rw-r--r--theories/Sets/Permut.v10
-rw-r--r--theories/Sets/Powerset.v10
-rw-r--r--theories/Sets/Powerset_Classical_facts.v10
-rw-r--r--theories/Sets/Powerset_facts.v101
-rw-r--r--theories/Sets/Relations_1.v10
-rw-r--r--theories/Sets/Relations_1_facts.v10
-rw-r--r--theories/Sets/Relations_2.v10
-rw-r--r--theories/Sets/Relations_2_facts.v10
-rw-r--r--theories/Sets/Relations_3.v10
-rw-r--r--theories/Sets/Relations_3_facts.v10
-rw-r--r--theories/Sets/Uniset.v14
-rw-r--r--theories/Sets/vo.itarget22
23 files changed, 225 insertions, 116 deletions
diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
index 837437a2..b68022f8 100644
--- a/theories/Sets/Classical_sets.v
+++ b/theories/Sets/Classical_sets.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) *)
(************************************************************************)
(****************************************************************************)
(* *)
diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index 6291248e..f2475af1 100644
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.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) *)
(************************************************************************)
(****************************************************************************)
(* *)
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index b5db9030..3977097e 100644
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.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) *)
(************************************************************************)
(****************************************************************************)
(* *)
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index 0fefb354..c3713207 100644
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.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) *)
(************************************************************************)
(****************************************************************************)
(* *)
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index edbc1efe..5c42cbe6 100644
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.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) *)
(************************************************************************)
(****************************************************************************)
(* *)
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
index 31cc11e1..1c191613 100644
--- a/theories/Sets/Finite_sets_facts.v
+++ b/theories/Sets/Finite_sets_facts.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) *)
(************************************************************************)
(****************************************************************************)
(* *)
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index e74ef41e..3e28bbe9 100644
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.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) *)
(************************************************************************)
(****************************************************************************)
(* *)
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index 98eeb7d7..bdeeb6a7 100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.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) *)
(************************************************************************)
(****************************************************************************)
(* *)
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index 057fc9b6..225e388b 100644
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.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) *)
(************************************************************************)
(****************************************************************************)
(* *)
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index 42d0c76d..a79ddead 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -1,14 +1,17 @@
(************************************************************************)
-(* 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) *)
(************************************************************************)
(* G. Huet 1-9-95 *)
Require Import Permut Setoid.
+Require Plus. (* comm. and ass. of plus *)
Set Implicit Arguments.
@@ -67,9 +70,6 @@ Section multiset_defs.
unfold meq; unfold munion; simpl; auto.
Qed.
-
- Require Plus. (* comm. and ass. of plus *)
-
Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x).
Proof.
unfold meq; unfold multiplicity; unfold munion.
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index 335fec5b..17fc0ed2 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.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) *)
(************************************************************************)
(****************************************************************************)
(* *)
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v
index adbde18e..86a500df 100644
--- a/theories/Sets/Permut.v
+++ b/theories/Sets/Permut.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) *)
(************************************************************************)
(* G. Huet 1-9-95 *)
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index 7c2435da..88bcd655 100644
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.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) *)
(************************************************************************)
(****************************************************************************)
(* *)
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index e802beac..7975a026 100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.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) *)
(************************************************************************)
(****************************************************************************)
(* *)
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index e9696a1c..81b475ac 100644
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.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) *)
(************************************************************************)
(****************************************************************************)
(* *)
@@ -40,6 +42,11 @@ Section Sets_as_an_algebra.
auto 6 with sets.
Qed.
+ Theorem Empty_set_zero_right : forall X:Ensemble U, Union U X (Empty_set U) = X.
+ Proof.
+ auto 6 with sets.
+ Qed.
+
Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x.
Proof.
unfold Add at 1; auto using Empty_set_zero with sets.
@@ -131,6 +138,17 @@ Section Sets_as_an_algebra.
elim H'; intros x0 H'0; elim H'0; auto with sets.
Qed.
+ Lemma Distributivity_l
+ : forall (A B C : Ensemble U),
+ Intersection U (Union U A B) C =
+ Union U (Intersection U A C) (Intersection U B C).
+ Proof.
+ intros A B C.
+ rewrite Intersection_commutative.
+ rewrite Distributivity.
+ f_equal; apply Intersection_commutative.
+ Qed.
+
Theorem Distributivity' :
forall A B C:Ensemble U,
Union U A (Intersection U B C) =
@@ -251,6 +269,81 @@ Section Sets_as_an_algebra.
intros; apply Definition_of_covers; auto with sets.
Qed.
+ Lemma Disjoint_Intersection:
+ forall A s1 s2, Disjoint A s1 s2 -> Intersection A s1 s2 = Empty_set A.
+ Proof.
+ intros. apply Extensionality_Ensembles. split.
+ * destruct H.
+ intros x H1. unfold In in *. exfalso. intuition. apply (H _ H1).
+ * intuition.
+ Qed.
+
+ Lemma Intersection_Empty_set_l:
+ forall A s, Intersection A (Empty_set A) s = Empty_set A.
+ Proof.
+ intros. auto with sets.
+ Qed.
+
+ Lemma Intersection_Empty_set_r:
+ forall A s, Intersection A s (Empty_set A) = Empty_set A.
+ Proof.
+ intros. auto with sets.
+ Qed.
+
+ Lemma Seminus_Empty_set_l:
+ forall A s, Setminus A (Empty_set A) s = Empty_set A.
+ Proof.
+ intros. apply Extensionality_Ensembles. split.
+ * intros x H1. destruct H1. unfold In in *. assumption.
+ * intuition.
+ Qed.
+
+ Lemma Seminus_Empty_set_r:
+ forall A s, Setminus A s (Empty_set A) = s.
+ Proof.
+ intros. apply Extensionality_Ensembles. split.
+ * intros x H1. destruct H1. unfold In in *. assumption.
+ * intuition.
+ Qed.
+
+ Lemma Setminus_Union_l:
+ forall A s1 s2 s3,
+ Setminus A (Union A s1 s2) s3 = Union A (Setminus A s1 s3) (Setminus A s2 s3).
+ Proof.
+ intros. apply Extensionality_Ensembles. split.
+ * intros x H. inversion H. inversion H0; intuition.
+ * intros x H. constructor; inversion H; inversion H0; intuition.
+ Qed.
+
+ Lemma Setminus_Union_r:
+ forall A s1 s2 s3,
+ Setminus A s1 (Union A s2 s3) = Setminus A (Setminus A s1 s2) s3.
+ Proof.
+ intros. apply Extensionality_Ensembles. split.
+ * intros x H. inversion H. constructor. intuition. contradict H1. intuition.
+ * intros x H. inversion H. inversion H0. constructor; intuition. inversion H4; intuition.
+ Qed.
+
+ Lemma Setminus_Disjoint_noop:
+ forall A s1 s2,
+ Intersection A s1 s2 = Empty_set A -> Setminus A s1 s2 = s1.
+ Proof.
+ intros. apply Extensionality_Ensembles. split.
+ * intros x H1. inversion_clear H1. intuition.
+ * intros x H1. constructor; intuition. contradict H.
+ apply Inhabited_not_empty.
+ exists x. intuition.
+ Qed.
+
+ Lemma Setminus_Included_empty:
+ forall A s1 s2,
+ Included A s1 s2 -> Setminus A s1 s2 = Empty_set A.
+ Proof.
+ intros. apply Extensionality_Ensembles. split.
+ * intros x H1. inversion_clear H1. contradiction H2. intuition.
+ * intuition.
+ Qed.
+
End Sets_as_an_algebra.
Hint Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add
diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v
index 45fb8134..1ed74599 100644
--- a/theories/Sets/Relations_1.v
+++ b/theories/Sets/Relations_1.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) *)
(************************************************************************)
(****************************************************************************)
(* *)
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
index bf8a4261..296ec42a 100644
--- a/theories/Sets/Relations_1_facts.v
+++ b/theories/Sets/Relations_1_facts.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) *)
(************************************************************************)
(****************************************************************************)
(* *)
diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v
index 1e0b83fe..cc839506 100644
--- a/theories/Sets/Relations_2.v
+++ b/theories/Sets/Relations_2.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) *)
(************************************************************************)
(****************************************************************************)
(* *)
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index da93e922..36da3684 100644
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.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) *)
(************************************************************************)
(****************************************************************************)
(* *)
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
index c05b5ee7..de3212e2 100644
--- a/theories/Sets/Relations_3.v
+++ b/theories/Sets/Relations_3.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) *)
(************************************************************************)
(****************************************************************************)
(* *)
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v
index 89fb900c..0c1f670d 100644
--- a/theories/Sets/Relations_3_facts.v
+++ b/theories/Sets/Relations_3_facts.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) *)
(************************************************************************)
(****************************************************************************)
(* *)
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index e297d97e..7940bda1 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.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) *)
(************************************************************************)
(** Sets as characteristic functions *)
@@ -11,7 +13,7 @@
(* G. Huet 1-9-95 *)
(* Updated Papageno 12/98 *)
-Require Import Bool.
+Require Import Bool Permut.
Set Implicit Arguments.
@@ -138,8 +140,6 @@ Hint Resolve seq_right.
(** Here we should make uniset an abstract datatype, by hiding [Charac],
[union], [charac]; all further properties are proved abstractly *)
-Require Import Permut.
-
Lemma union_rotate :
forall x y z:uniset, seq (union x (union y z)) (union z (union x y)).
Proof.
diff --git a/theories/Sets/vo.itarget b/theories/Sets/vo.itarget
deleted file mode 100644
index 9ebe92f5..00000000
--- a/theories/Sets/vo.itarget
+++ /dev/null
@@ -1,22 +0,0 @@
-Classical_sets.vo
-Constructive_sets.vo
-Cpo.vo
-Ensembles.vo
-Finite_sets_facts.vo
-Finite_sets.vo
-Image.vo
-Infinite_sets.vo
-Integers.vo
-Multiset.vo
-Partial_Order.vo
-Permut.vo
-Powerset_Classical_facts.vo
-Powerset_facts.vo
-Powerset.vo
-Relations_1_facts.vo
-Relations_1.vo
-Relations_2_facts.vo
-Relations_2.vo
-Relations_3_facts.vo
-Relations_3.vo
-Uniset.vo
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 06:36:10 +0000