diff options
Diffstat (limited to 'theories/Sets')
-rw-r--r-- | theories/Sets/Classical_sets.v | 10 | ||||
-rw-r--r-- | theories/Sets/Constructive_sets.v | 10 | ||||
-rw-r--r-- | theories/Sets/Cpo.v | 10 | ||||
-rw-r--r-- | theories/Sets/Ensembles.v | 10 | ||||
-rw-r--r-- | theories/Sets/Finite_sets.v | 10 | ||||
-rw-r--r-- | theories/Sets/Finite_sets_facts.v | 10 | ||||
-rw-r--r-- | theories/Sets/Image.v | 10 | ||||
-rw-r--r-- | theories/Sets/Infinite_sets.v | 10 | ||||
-rw-r--r-- | theories/Sets/Integers.v | 10 | ||||
-rw-r--r-- | theories/Sets/Multiset.v | 14 | ||||
-rw-r--r-- | theories/Sets/Partial_Order.v | 10 | ||||
-rw-r--r-- | theories/Sets/Permut.v | 10 | ||||
-rw-r--r-- | theories/Sets/Powerset.v | 10 | ||||
-rw-r--r-- | theories/Sets/Powerset_Classical_facts.v | 10 | ||||
-rw-r--r-- | theories/Sets/Powerset_facts.v | 101 | ||||
-rw-r--r-- | theories/Sets/Relations_1.v | 10 | ||||
-rw-r--r-- | theories/Sets/Relations_1_facts.v | 10 | ||||
-rw-r--r-- | theories/Sets/Relations_2.v | 10 | ||||
-rw-r--r-- | theories/Sets/Relations_2_facts.v | 10 | ||||
-rw-r--r-- | theories/Sets/Relations_3.v | 10 | ||||
-rw-r--r-- | theories/Sets/Relations_3_facts.v | 10 | ||||
-rw-r--r-- | theories/Sets/Uniset.v | 14 | ||||
-rw-r--r-- | theories/Sets/vo.itarget | 22 |
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 |