summaryrefslogtreecommitdiff
path: root/theories/Sets
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Sets')
-rw-r--r--theories/Sets/Classical_sets.v6
-rw-r--r--theories/Sets/Constructive_sets.v14
-rw-r--r--theories/Sets/Cpo.v12
-rw-r--r--theories/Sets/Ensembles.v38
-rw-r--r--theories/Sets/Finite_sets.v4
-rw-r--r--theories/Sets/Finite_sets_facts.v10
-rw-r--r--theories/Sets/Image.v26
-rw-r--r--theories/Sets/Infinite_sets.v14
-rw-r--r--theories/Sets/Integers.v24
-rw-r--r--theories/Sets/Multiset.v40
-rw-r--r--theories/Sets/Partial_Order.v14
-rw-r--r--theories/Sets/Permut.v12
-rw-r--r--theories/Sets/Powerset.v2
-rw-r--r--theories/Sets/Powerset_Classical_facts.v32
-rw-r--r--theories/Sets/Powerset_facts.v42
-rw-r--r--theories/Sets/Relations_1.v26
-rw-r--r--theories/Sets/Relations_1_facts.v2
-rw-r--r--theories/Sets/Relations_2.v2
-rw-r--r--theories/Sets/Relations_2_facts.v4
-rw-r--r--theories/Sets/Relations_3.v18
-rw-r--r--theories/Sets/Relations_3_facts.v2
-rw-r--r--theories/Sets/Uniset.v12
-rw-r--r--theories/Sets/vo.itarget22
23 files changed, 205 insertions, 173 deletions
diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
index e6755898..5f686099 100644
--- a/theories/Sets/Classical_sets.v
+++ b/theories/Sets/Classical_sets.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Classical_sets.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
Require Export Ensembles.
Require Export Constructive_sets.
@@ -56,7 +56,7 @@ Section Ensembles_classical.
forall X Y:Ensemble U,
Included U X Y -> ~ Included U Y X -> Inhabited U (Setminus U Y X).
Proof.
- intros X Y I NI.
+ intros X Y I NI.
elim (not_all_ex_not U (fun x:U => In U Y x -> In U X x) NI).
intros x YX.
apply Inhabited_intro with x.
@@ -78,7 +78,7 @@ Section Ensembles_classical.
unfold Subtract at 1 in |- *; auto with sets.
Qed.
Hint Resolve Subtract_intro : sets.
-
+
Lemma Subtract_inv :
forall (A:Ensemble U) (x y:U), In U (Subtract U A x) y -> In U A y /\ x <> y.
Proof.
diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index ad81316d..0719365f 100644
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.v
@@ -24,13 +24,13 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Constructive_sets.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
Require Export Ensembles.
Section Ensembles_facts.
Variable U : Type.
-
+
Lemma Extension : forall B C:Ensemble U, B = C -> Same_set U B C.
Proof.
intros B C H'; rewrite H'; auto with sets.
@@ -52,7 +52,7 @@ Section Ensembles_facts.
Proof.
unfold Add at 1 in |- *; auto with sets.
Qed.
-
+
Lemma Add_intro2 : forall (A:Ensemble U) (x:U), In U (Add U A x) x.
Proof.
unfold Add at 1 in |- *; auto with sets.
@@ -98,15 +98,15 @@ Section Ensembles_facts.
Proof.
intros B C x H'; elim H'; auto with sets.
Qed.
-
+
Lemma Add_inv :
forall (A:Ensemble U) (x y:U), In U (Add U A x) y -> In U A y \/ x = y.
Proof.
- intros A x y H'; induction H'.
+ intros A x y H'; induction H'.
left; assumption.
right; apply Singleton_inv; assumption.
Qed.
-
+
Lemma Intersection_inv :
forall (B C:Ensemble U) (x:U),
In U (Intersection U B C) x -> In U B x /\ In U C x.
@@ -125,7 +125,7 @@ Section Ensembles_facts.
Proof.
unfold Setminus at 1 in |- *; red in |- *; auto with sets.
Qed.
-
+
Lemma Strict_Included_intro :
forall X Y:Ensemble U, Included U X Y /\ X <> Y -> Strict_Included U X Y.
Proof.
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index 1e1b70d5..8c69e687 100644
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Cpo.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
Require Export Ensembles.
Require Export Relations_1.
@@ -35,7 +35,7 @@ Section Bounds.
Variable D : PO U.
Let C := Carrier_of U D.
-
+
Let R := Rel_of U D.
Inductive Upper_Bound (B:Ensemble U) (x:U) : Prop :=
@@ -45,7 +45,7 @@ Section Bounds.
Inductive Lower_Bound (B:Ensemble U) (x:U) : Prop :=
Lower_Bound_definition :
In U C x -> (forall y:U, In U B y -> R x y) -> Lower_Bound B x.
-
+
Inductive Lub (B:Ensemble U) (x:U) : Prop :=
Lub_definition :
Upper_Bound B x -> (forall y:U, Upper_Bound B y -> R x y) -> Lub B x.
@@ -57,7 +57,7 @@ Section Bounds.
Inductive Bottom (bot:U) : Prop :=
Bottom_definition :
In U C bot -> (forall y:U, In U C y -> R bot y) -> Bottom bot.
-
+
Inductive Totally_ordered (B:Ensemble U) : Prop :=
Totally_ordered_definition :
(Included U B C ->
@@ -77,7 +77,7 @@ Section Bounds.
Included U (Couple U x1 x2) X ->
exists x3 : _, In U X x3 /\ Upper_Bound (Couple U x1 x2) x3) ->
Directed X.
-
+
Inductive Complete : Prop :=
Definition_of_Complete :
(exists bot : _, Bottom bot) ->
@@ -102,7 +102,7 @@ Section Specific_orders.
Record Cpo : Type := Definition_of_cpo
{PO_of_cpo : PO U; Cpo_cond : Complete U PO_of_cpo}.
-
+
Record Chain : Type := Definition_of_chain
{PO_of_chain : PO U;
Chain_cond : Totally_ordered U PO_of_chain (Carrier_of U PO_of_chain)}.
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index c38a2fe1..0fa9c74a 100644
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.v
@@ -24,27 +24,27 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Ensembles.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
Section Ensembles.
Variable U : Type.
-
- Definition Ensemble := U -> Prop.
+
+ Definition Ensemble := U -> Prop.
Definition In (A:Ensemble) (x:U) : Prop := A x.
-
+
Definition Included (B C:Ensemble) : Prop := forall x:U, In B x -> In C x.
-
+
Inductive Empty_set : Ensemble :=.
-
+
Inductive Full_set : Ensemble :=
Full_intro : forall x:U, In Full_set x.
-(** NB: The following definition builds-in equality of elements in [U] as
- Leibniz equality.
+(** NB: The following definition builds-in equality of elements in [U] as
+ Leibniz equality.
- This may have to be changed if we replace [U] by a Setoid on [U]
- with its own equality [eqs], with
+ This may have to be changed if we replace [U] by a Setoid on [U]
+ with its own equality [eqs], with
[In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y)]. *)
Inductive Singleton (x:U) : Ensemble :=
@@ -55,7 +55,7 @@ Section Ensembles.
| Union_intror : forall x:U, In C x -> In (Union B C) x.
Definition Add (B:Ensemble) (x:U) : Ensemble := Union B (Singleton x).
-
+
Inductive Intersection (B C:Ensemble) : Ensemble :=
Intersection_intro :
forall x:U, In B x -> In C x -> In (Intersection B C) x.
@@ -63,29 +63,29 @@ Section Ensembles.
Inductive Couple (x y:U) : Ensemble :=
| Couple_l : In (Couple x y) x
| Couple_r : In (Couple x y) y.
-
+
Inductive Triple (x y z:U) : Ensemble :=
| Triple_l : In (Triple x y z) x
| Triple_m : In (Triple x y z) y
| Triple_r : In (Triple x y z) z.
-
+
Definition Complement (A:Ensemble) : Ensemble := fun x:U => ~ In A x.
-
+
Definition Setminus (B C:Ensemble) : Ensemble :=
fun x:U => In B x /\ ~ In C x.
-
+
Definition Subtract (B:Ensemble) (x:U) : Ensemble := Setminus B (Singleton x).
-
+
Inductive Disjoint (B C:Ensemble) : Prop :=
Disjoint_intro : (forall x:U, ~ In (Intersection B C) x) -> Disjoint B C.
Inductive Inhabited (B:Ensemble) : Prop :=
Inhabited_intro : forall x:U, In B x -> Inhabited B.
-
+
Definition Strict_Included (B C:Ensemble) : Prop := Included B C /\ B <> C.
-
+
Definition Same_set (B C:Ensemble) : Prop := Included B C /\ Included C B.
-
+
(** Extensionality Axiom *)
Axiom Extensionality_Ensembles : forall A B:Ensemble, Same_set A B -> A = B.
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index f5eae4ed..019c25a5 100644
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Finite_sets.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
Require Import Ensembles.
@@ -52,7 +52,7 @@ Require Import Constructive_sets.
Section Ensembles_finis_facts.
Variable U : Type.
-
+
Lemma cardinal_invert :
forall (X:Ensemble U) (p:nat),
cardinal U X p ->
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
index 91717f9e..fdcc4150 100644
--- a/theories/Sets/Finite_sets_facts.v
+++ b/theories/Sets/Finite_sets_facts.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Finite_sets_facts.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
Require Export Finite_sets.
Require Export Constructive_sets.
@@ -72,7 +72,7 @@ Section Finite_sets_facts.
Proof.
intros X Y H; induction H as [|A Fin_A Hind x].
rewrite (Empty_set_zero U Y). trivial.
- intros.
+ intros.
rewrite (Union_commutative U (Add U A x) Y).
rewrite <- (Union_add U Y A x).
rewrite (Union_commutative U Y A).
@@ -98,7 +98,7 @@ Section Finite_sets_facts.
Proof.
intros A H' X; apply Finite_downward_closed with A; auto with sets.
Qed.
-
+
Lemma cardinalO_empty :
forall X:Ensemble U, cardinal U X 0 -> X = Empty_set U.
Proof.
@@ -212,7 +212,7 @@ Section Finite_sets_facts.
Proof.
intros; apply cardinal_is_functional with X X; auto with sets.
Qed.
-
+
Lemma card_Add_gen :
forall (A:Ensemble U) (x:U) (n n':nat),
cardinal U A n -> cardinal U (Add U A x) n' -> n' <= S n.
@@ -279,7 +279,7 @@ Section Finite_sets_facts.
intro E; rewrite E; auto with sets arith.
apply cardinal_unicity with X; auto with sets arith.
Qed.
-
+
Lemma G_aux :
forall P:Ensemble U -> Prop,
(forall X:Ensemble U,
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index d3591acf..64c341bd 100644
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Image.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
Require Export Finite_sets.
Require Export Constructive_sets.
@@ -40,10 +40,10 @@ Require Export Finite_sets_facts.
Section Image.
Variables U V : Type.
-
+
Inductive Im (X:Ensemble U) (f:U -> V) : Ensemble V :=
Im_intro : forall x:U, In _ X x -> forall y:V, y = f x -> In _ (Im X f) y.
-
+
Lemma Im_def :
forall (X:Ensemble U) (f:U -> V) (x:U), In _ X x -> In _ (Im X f) (f x).
Proof.
@@ -62,13 +62,13 @@ Section Image.
rewrite H0.
elim Add_inv with U X x x1; auto using Im_def with sets.
destruct 1; auto using Im_def with sets.
- elim Add_inv with V (Im X f) (f x) x0.
+ elim Add_inv with V (Im X f) (f x) x0.
destruct 1 as [x0 H y H0].
rewrite H0; auto using Im_def with sets.
destruct 1; auto using Im_def with sets.
trivial.
Qed.
-
+
Lemma image_empty : forall f:U -> V, Im (Empty_set U) f = Empty_set V.
Proof.
intro f; try assumption.
@@ -88,7 +88,7 @@ Section Image.
rewrite (Im_add A x f); auto with sets.
apply Add_preserves_Finite; auto with sets.
Qed.
-
+
Lemma Im_inv :
forall (X:Ensemble U) (f:U -> V) (y:V),
In _ (Im X f) y -> exists x : U, In _ X x /\ f x = y.
@@ -97,9 +97,9 @@ Section Image.
intros x H'0 y0 H'1; rewrite H'1.
exists x; auto with sets.
Qed.
-
+
Definition injective (f:U -> V) := forall x y:U, f x = f y -> x = y.
-
+
Lemma not_injective_elim :
forall f:U -> V,
~ injective f -> exists x : _, (exists y : _, f x = f y /\ x <> y).
@@ -115,7 +115,7 @@ Section Image.
destruct 1 as [y D]; exists y.
apply imply_to_and; trivial with sets.
Qed.
-
+
Lemma cardinal_Im_intro :
forall (A:Ensemble U) (f:U -> V) (n:nat),
cardinal _ A n -> exists p : nat, cardinal _ (Im A f) p.
@@ -124,7 +124,7 @@ Section Image.
apply finite_cardinal; apply finite_image.
apply cardinal_finite with n; trivial with sets.
Qed.
-
+
Lemma In_Image_elim :
forall (A:Ensemble U) (f:U -> V),
injective f -> forall x:U, In _ (Im A f) (f x) -> In _ A x.
@@ -134,7 +134,7 @@ Section Image.
intros z C; elim C; intros InAz E.
elim (H z x E); trivial with sets.
Qed.
-
+
Lemma injective_preserves_cardinal :
forall (A:Ensemble U) (f:U -> V) (n:nat),
injective f ->
@@ -158,7 +158,7 @@ Section Image.
red in |- *; intro; apply H'2.
apply In_Image_elim with f; trivial with sets.
Qed.
-
+
Lemma cardinal_decreases :
forall (A:Ensemble U) (f:U -> V) (n:nat),
cardinal U A n -> forall n':nat, cardinal V (Im A f) n' -> n' <= n.
@@ -188,7 +188,7 @@ Section Image.
apply injective_preserves_cardinal with (A := A) (f := f) (n := n);
trivial with sets.
Qed.
-
+
Lemma Pigeonhole_principle :
forall (A:Ensemble U) (f:U -> V) (n:nat),
cardinal _ A n ->
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index ae2143c8..b63ec1d4 100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Infinite_sets.v 10637 2008-03-07 23:52:56Z letouzey $ i*)
+(*i $Id$ i*)
Require Export Finite_sets.
Require Export Constructive_sets.
@@ -50,7 +50,7 @@ Hint Resolve Defn_of_Approximant.
Section Infinite_sets.
Variable U : Type.
-
+
Lemma make_new_approximant :
forall A X:Ensemble U,
~ Finite U A -> Approximant U A X -> Inhabited U (Setminus U A X).
@@ -61,7 +61,7 @@ Section Infinite_sets.
red in |- *; intro H'3; apply H'.
rewrite <- H'3; auto with sets.
Qed.
-
+
Lemma approximants_grow :
forall A X:Ensemble U,
~ Finite U A ->
@@ -101,7 +101,7 @@ Section Infinite_sets.
apply Defn_of_Approximant; auto with sets.
apply cardinal_finite with (n := S n0); auto with sets.
Qed.
-
+
Lemma approximants_grow' :
forall A X:Ensemble U,
~ Finite U A ->
@@ -121,7 +121,7 @@ Section Infinite_sets.
apply cardinal_finite with (n := S n); auto with sets.
apply approximants_grow with (X := X); auto with sets.
Qed.
-
+
Lemma approximant_can_be_any_size :
forall A X:Ensemble U,
~ Finite U A ->
@@ -135,7 +135,7 @@ Section Infinite_sets.
Qed.
Variable V : Type.
-
+
Theorem Image_set_continuous :
forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
Finite V X ->
@@ -230,7 +230,7 @@ Section Infinite_sets.
rewrite H'4; auto with sets.
elim H'3; auto with sets.
Qed.
-
+
Theorem Pigeonhole_ter :
forall (A:Ensemble U) (f:U -> V) (n:nat),
injective U V f -> Finite V (Im U V A f) -> Finite U A.
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index 1786edf1..15c1b665 100644
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Integers.v 10637 2008-03-07 23:52:56Z letouzey $ i*)
+(*i $Id$ i*)
Require Export Finite_sets.
Require Export Constructive_sets.
@@ -45,7 +45,7 @@ Require Export Partial_Order.
Require Export Cpo.
Section Integers_sect.
-
+
Inductive Integers : Ensemble nat :=
Integers_defn : forall x:nat, In nat Integers x.
@@ -53,7 +53,7 @@ Section Integers_sect.
Proof.
red in |- *; auto with arith.
Qed.
-
+
Lemma le_antisym : Antisymmetric nat le.
Proof.
red in |- *; intros x y H H'; rewrite (le_antisym x y); auto.
@@ -63,12 +63,12 @@ Section Integers_sect.
Proof.
red in |- *; intros; apply le_trans with y; auto.
Qed.
-
+
Lemma le_Order : Order nat le.
Proof.
- split; [exact le_reflexive | exact le_trans | exact le_antisym].
+ split; [exact le_reflexive | exact le_trans | exact le_antisym].
Qed.
-
+
Lemma triv_nat : forall n:nat, In nat Integers n.
Proof.
exact Integers_defn.
@@ -77,11 +77,11 @@ Section Integers_sect.
Definition nat_po : PO nat.
apply Definition_of_PO with (Carrier_of := Integers) (Rel_of := le);
auto with sets arith.
- apply Inhabited_intro with (x := 0).
+ apply Inhabited_intro with (x := 0).
apply Integers_defn.
- exact le_Order.
+ exact le_Order.
Defined.
-
+
Lemma le_total_order : Totally_ordered nat nat_po Integers.
Proof.
apply Totally_ordered_definition.
@@ -92,7 +92,7 @@ Section Integers_sect.
intro H'1; right.
cut (y <= x); auto with sets arith.
Qed.
-
+
Lemma Finite_subset_has_lub :
forall X:Ensemble nat,
Finite nat X -> exists m : nat, Upper_Bound nat nat_po X m.
@@ -124,7 +124,7 @@ Section Integers_sect.
apply H'4 with (y := x0). elim H'3; simpl in |- *; auto with sets arith. trivial.
intros x1 H'4; elim H'4. unfold nat_po; simpl; trivial.
exists x0.
- apply Upper_Bound_definition.
+ apply Upper_Bound_definition.
unfold nat_po. simpl. apply triv_nat.
intros y H'1; elim H'1.
intros x1 H'4; try assumption.
@@ -148,7 +148,7 @@ Section Integers_sect.
absurd (S x <= x); auto with arith.
apply triv_nat.
Qed.
-
+
Lemma Integers_infinite : ~ Finite nat Integers.
Proof.
generalize Integers_has_no_ub.
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index d2bff488..7216ae33 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -6,11 +6,11 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Multiset.v 10616 2008-03-04 17:33:35Z letouzey $ i*)
+(*i $Id$ i*)
(* G. Huet 1-9-95 *)
-Require Import Permut.
+Require Import Permut Setoid.
Set Implicit Arguments.
@@ -18,11 +18,12 @@ Section multiset_defs.
Variable A : Type.
Variable eqA : A -> A -> Prop.
+ Hypothesis eqA_equiv : Equivalence eqA.
Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
Inductive multiset : Type :=
Bag : (A -> nat) -> multiset.
-
+
Definition EmptyBag := Bag (fun a:A => 0).
Definition SingletonBag (a:A) :=
Bag (fun a':A => match Aeq_dec a a' with
@@ -31,23 +32,23 @@ Section multiset_defs.
end).
Definition multiplicity (m:multiset) (a:A) : nat := let (f) := m in f a.
-
+
(** multiset equality *)
Definition meq (m1 m2:multiset) :=
forall a:A, multiplicity m1 a = multiplicity m2 a.
-
+
Lemma meq_refl : forall x:multiset, meq x x.
Proof.
destruct x; unfold meq; reflexivity.
Qed.
-
+
Lemma meq_trans : forall x y z:multiset, meq x y -> meq y z -> meq x z.
Proof.
unfold meq in |- *.
destruct x; destruct y; destruct z.
intros; rewrite H; auto.
Qed.
-
+
Lemma meq_sym : forall x y:multiset, meq x y -> meq y x.
Proof.
unfold meq in |- *.
@@ -62,7 +63,7 @@ Section multiset_defs.
Proof.
unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.
Qed.
-
+
Lemma munion_empty_right : forall x:multiset, meq x (munion x EmptyBag).
Proof.
unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.
@@ -70,7 +71,7 @@ Section multiset_defs.
Require Plus. (* comm. and ass. of plus *)
-
+
Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x).
Proof.
unfold meq in |- *; unfold multiplicity in |- *; unfold munion in |- *.
@@ -106,28 +107,28 @@ Section multiset_defs.
Lemma munion_rotate :
forall x y z:multiset, meq (munion x (munion y z)) (munion z (munion x y)).
Proof.
- intros; apply (op_rotate multiset munion meq).
+ intros; apply (op_rotate multiset munion meq).
apply munion_comm.
apply munion_ass.
exact meq_trans.
exact meq_sym.
trivial.
Qed.
-
+
Lemma meq_congr :
forall x y z t:multiset, meq x y -> meq z t -> meq (munion x z) (munion y t).
Proof.
intros; apply (cong_congr multiset munion meq); auto using meq_left, meq_right.
exact meq_trans.
Qed.
-
+
Lemma munion_perm_left :
forall x y z:multiset, meq (munion x (munion y z)) (munion y (munion x z)).
Proof.
intros; apply (perm_left multiset munion meq); auto using munion_comm, munion_ass, meq_left, meq_right, meq_sym.
exact meq_trans.
Qed.
-
+
Lemma multiset_twist1 :
forall x y z t:multiset,
meq (munion x (munion (munion y z) t)) (munion (munion y (munion x t)) z).
@@ -156,7 +157,7 @@ Section multiset_defs.
apply meq_right; apply meq_left; trivial.
apply multiset_twist1.
Qed.
-
+
Lemma treesort_twist2 :
forall x y z t u:multiset,
meq u (munion y z) ->
@@ -167,8 +168,17 @@ Section multiset_defs.
apply multiset_twist2.
Qed.
+ (** SingletonBag *)
+
+ Lemma meq_singleton : forall a a',
+ eqA a a' -> meq (SingletonBag a) (SingletonBag a').
+ Proof.
+ intros; red; simpl; intro a0.
+ destruct (Aeq_dec a a0) as [Ha|Ha]; rewrite H in Ha;
+ decide (Aeq_dec a' a0) with Ha; reflexivity.
+ Qed.
-(*i theory of minter to do similarly
+(*i theory of minter to do similarly
Require Min.
(* multiset intersection *)
Definition minter := [m1,m2:multiset]
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index 6210913c..4fe8f4f6 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -24,27 +24,27 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Partial_Order.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
Require Export Ensembles.
Require Export Relations_1.
Section Partial_orders.
Variable U : Type.
-
+
Definition Carrier := Ensemble U.
-
+
Definition Rel := Relation U.
-
+
Record PO : Type := Definition_of_PO
{ Carrier_of : Ensemble U;
Rel_of : Relation U;
PO_cond1 : Inhabited U Carrier_of;
PO_cond2 : Order U Rel_of }.
Variable p : PO.
-
+
Definition Strict_Rel_of : Rel := fun x y:U => Rel_of p x y /\ x <> y.
-
+
Inductive covers (y x:U) : Prop :=
Definition_of_covers :
Strict_Rel_of x y ->
@@ -60,7 +60,7 @@ Hint Resolve Definition_of_covers: sets v62.
Section Partial_order_facts.
Variable U : Type.
Variable D : PO U.
-
+
Lemma Strict_Rel_Transitive_with_Rel :
forall x y z:U,
Strict_Rel_of U D x y -> Rel_of U D y z -> Strict_Rel_of U D x z.
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v
index 4380f10c..f593031a 100644
--- a/theories/Sets/Permut.v
+++ b/theories/Sets/Permut.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Permut.v 10616 2008-03-04 17:33:35Z letouzey $ i*)
+(*i $Id$ i*)
(* G. Huet 1-9-95 *)
@@ -36,23 +36,23 @@ Section Axiomatisation.
apply cong_left; trivial.
apply cong_right; trivial.
Qed.
-
+
Lemma comm_right : forall x y z:U, cong (op x (op y z)) (op x (op z y)).
Proof.
intros; apply cong_right; apply op_comm.
Qed.
-
+
Lemma comm_left : forall x y z:U, cong (op (op x y) z) (op (op y x) z).
Proof.
intros; apply cong_left; apply op_comm.
Qed.
-
+
Lemma perm_right : forall x y z:U, cong (op (op x y) z) (op (op x z) y).
Proof.
intros.
apply cong_trans with (op x (op y z)).
apply op_ass.
- apply cong_trans with (op x (op z y)).
+ apply cong_trans with (op x (op z y)).
apply cong_right; apply op_comm.
apply cong_sym; apply op_ass.
Qed.
@@ -66,7 +66,7 @@ Section Axiomatisation.
apply cong_left; apply op_comm.
apply op_ass.
Qed.
-
+
Lemma op_rotate : forall x y z t:U, cong (op x (op y z)) (op z (op x y)).
Proof.
intros; apply cong_trans with (op (op x y) z).
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index c9a52ac2..c323ca35 100644
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Powerset.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id$ i*)
Require Export Ensembles.
Require Export Relations_1.
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index 34c49409..36d2150c 100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Powerset_Classical_facts.v 10855 2008-04-27 11:16:15Z msozeau $ i*)
+(*i $Id$ i*)
Require Export Ensembles.
Require Export Constructive_sets.
@@ -40,7 +40,7 @@ Require Export Classical_sets.
Section Sets_as_an_algebra.
Variable U : Type.
-
+
Lemma sincl_add_x :
forall (A B:Ensemble U) (x:U),
~ In U A x ->
@@ -63,7 +63,7 @@ Section Sets_as_an_algebra.
intros X x H'; red in |- *.
intros x0 H'0; elim H'0; auto with sets.
Qed.
-
+
Lemma incl_soustr :
forall (X Y:Ensemble U) (x:U),
Included U X Y -> Included U (Subtract U X x) (Subtract U Y x).
@@ -73,7 +73,7 @@ Section Sets_as_an_algebra.
intros H'1 H'2.
apply Subtract_intro; auto with sets.
Qed.
-
+
Lemma incl_soustr_add_l :
forall (X:Ensemble U) (x:U), Included U (Subtract U (Add U X x) x) X.
Proof.
@@ -93,7 +93,7 @@ Section Sets_as_an_algebra.
red in |- *; intro H'1; apply H'; rewrite H'1; auto with sets.
Qed.
Hint Resolve incl_soustr_add_r: sets v62.
-
+
Lemma add_soustr_2 :
forall (X:Ensemble U) (x:U),
In U X x -> Included U X (Add U (Subtract U X x) x).
@@ -103,7 +103,7 @@ Section Sets_as_an_algebra.
elim (classic (x = x0)); intro K; auto with sets.
elim K; auto with sets.
Qed.
-
+
Lemma add_soustr_1 :
forall (X:Ensemble U) (x:U),
In U X x -> Included U (Add U (Subtract U X x) x) X.
@@ -114,7 +114,7 @@ Section Sets_as_an_algebra.
intros t H'1; try assumption.
rewrite <- (Singleton_inv U x t); auto with sets.
Qed.
-
+
Lemma add_soustr_xy :
forall (X:Ensemble U) (x y:U),
x <> y -> Subtract U (Add U X x) y = Add U (Subtract U X y) x.
@@ -133,7 +133,7 @@ Section Sets_as_an_algebra.
intro H'0; elim H'0; auto with sets.
intro H'0; rewrite <- H'0; auto with sets.
Qed.
-
+
Lemma incl_st_add_soustr :
forall (X Y:Ensemble U) (x:U),
~ In U X x ->
@@ -151,13 +151,13 @@ Section Sets_as_an_algebra.
red in |- *; intro H'0; apply H'2.
rewrite H'0; auto 8 using add_soustr_xy, add_soustr_1, add_soustr_2 with sets.
Qed.
-
+
Lemma Sub_Add_new :
forall (X:Ensemble U) (x:U), ~ In U X x -> X = Subtract U (Add U X x) x.
Proof.
auto using incl_soustr_add_l with sets.
Qed.
-
+
Lemma Simplify_add :
forall (X X0:Ensemble U) (x:U),
~ In U X x -> ~ In U X0 x -> Add U X x = Add U X0 x -> X = X0.
@@ -167,7 +167,7 @@ Section Sets_as_an_algebra.
rewrite (Sub_Add_new X0 x); auto with sets.
rewrite H'1; auto with sets.
Qed.
-
+
Lemma Included_Add :
forall (X A:Ensemble U) (x:U),
Included U X (Add U A x) ->
@@ -201,7 +201,7 @@ Section Sets_as_an_algebra.
absurd (In U X x0); auto with sets.
rewrite <- H'5; auto with sets.
Qed.
-
+
Lemma setcover_inv :
forall A x y:Ensemble U,
covers (Ensemble U) (Power_set_PO U A) y x ->
@@ -219,7 +219,7 @@ Section Sets_as_an_algebra.
elim H'1.
exists z; auto with sets.
Qed.
-
+
Theorem Add_covers :
forall A a:Ensemble U,
Included U a A ->
@@ -255,7 +255,7 @@ Section Sets_as_an_algebra.
intros x1 H'10; elim H'10; auto with sets.
intros x2 H'11; elim H'11; auto with sets.
Qed.
-
+
Theorem covers_Add :
forall A a a':Ensemble U,
Included U a A ->
@@ -301,7 +301,7 @@ Section Sets_as_an_algebra.
intros x H'1; elim H'1; intros H'2 H'3; rewrite H'2; clear H'1.
apply Add_covers; intuition.
Qed.
-
+
Theorem Singleton_atomic :
forall (x:U) (A:Ensemble U),
In U A x ->
@@ -311,7 +311,7 @@ Section Sets_as_an_algebra.
rewrite <- (Empty_set_zero' U x).
apply Add_covers; auto with sets.
Qed.
-
+
Lemma less_than_singleton :
forall (X:Ensemble U) (x:U),
Strict_Included U X (Singleton U x) -> X = Empty_set U.
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index edb6a215..76f7f1ec 100644
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Powerset_facts.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
Require Export Ensembles.
Require Export Constructive_sets.
@@ -41,34 +41,34 @@ Section Sets_as_an_algebra.
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 in |- *; auto using Empty_set_zero with sets.
Qed.
-
+
Lemma less_than_empty :
forall X:Ensemble U, Included U X (Empty_set U) -> X = Empty_set U.
Proof.
auto with sets.
Qed.
-
+
Theorem Union_commutative : forall A B:Ensemble U, Union U A B = Union U B A.
Proof.
auto with sets.
Qed.
-
+
Theorem Union_associative :
forall A B C:Ensemble U, Union U (Union U A B) C = Union U A (Union U B C).
Proof.
auto 9 with sets.
Qed.
-
+
Theorem Union_idempotent : forall A:Ensemble U, Union U A A = A.
Proof.
auto 7 with sets.
Qed.
-
+
Lemma Union_absorbs :
forall A B:Ensemble U, Included U B A -> Union U A B = A.
Proof.
@@ -82,7 +82,7 @@ Section Sets_as_an_algebra.
intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets).
intros x0 H'; elim H'; auto with sets.
Qed.
-
+
Theorem Triple_as_union :
forall x y z:U,
Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z) =
@@ -94,7 +94,7 @@ Section Sets_as_an_algebra.
intros x1 H'0; elim H'0; auto with sets.
intros x0 H'; elim H'; auto with sets.
Qed.
-
+
Theorem Triple_as_Couple : forall x y:U, Couple U x y = Triple U x x y.
Proof.
intros x y.
@@ -102,7 +102,7 @@ Section Sets_as_an_algebra.
rewrite <- (Union_idempotent (Singleton U x)).
apply Triple_as_union.
Qed.
-
+
Theorem Triple_as_Couple_Singleton :
forall x y z:U, Triple U x y z = Union U (Couple U x y) (Singleton U z).
Proof.
@@ -110,7 +110,7 @@ Section Sets_as_an_algebra.
rewrite <- (Triple_as_union x y z).
rewrite <- (Couple_as_union x y); auto with sets.
Qed.
-
+
Theorem Intersection_commutative :
forall A B:Ensemble U, Intersection U A B = Intersection U B A.
Proof.
@@ -118,7 +118,7 @@ Section Sets_as_an_algebra.
apply Extensionality_Ensembles.
split; red in |- *; intros x H'; elim H'; auto with sets.
Qed.
-
+
Theorem Distributivity :
forall A B C:Ensemble U,
Intersection U A (Union U B C) =
@@ -132,7 +132,7 @@ Section Sets_as_an_algebra.
elim H'1; auto with sets.
elim H'; intros x0 H'0; elim H'0; auto with sets.
Qed.
-
+
Theorem Distributivity' :
forall A B C:Ensemble U,
Union U A (Intersection U B C) =
@@ -149,13 +149,13 @@ Section Sets_as_an_algebra.
generalize H'1.
elim H'2; auto with sets.
Qed.
-
+
Theorem Union_add :
forall (A B:Ensemble U) (x:U), Add U (Union U A B) x = Union U A (Add U B x).
Proof.
unfold Add in |- *; auto using Union_associative with sets.
Qed.
-
+
Theorem Non_disjoint_union :
forall (X:Ensemble U) (x:U), In U X x -> Add U X x = X.
Proof.
@@ -165,7 +165,7 @@ Section Sets_as_an_algebra.
intros x0 H'0; elim H'0; auto with sets.
intros t H'1; elim H'1; auto with sets.
Qed.
-
+
Theorem Non_disjoint_union' :
forall (X:Ensemble U) (x:U), ~ In U X x -> Subtract U X x = X.
Proof.
@@ -178,12 +178,12 @@ Section Sets_as_an_algebra.
lapply (Singleton_inv U x x0); auto with sets.
intro H'4; apply H'; rewrite H'4; auto with sets.
Qed.
-
+
Lemma singlx : forall x y:U, In U (Add U (Empty_set U) x) y -> x = y.
Proof.
intro x; rewrite (Empty_set_zero' x); auto with sets.
Qed.
-
+
Lemma incl_add :
forall (A B:Ensemble U) (x:U),
Included U A B -> Included U (Add U A x) (Add U B x).
@@ -209,7 +209,7 @@ Section Sets_as_an_algebra.
absurd (In U A x0); auto with sets.
rewrite <- H'4; auto with sets.
Qed.
-
+
Lemma Add_commutative :
forall (A:Ensemble U) (x y:U), Add U (Add U A x) y = Add U (Add U A y) x.
Proof.
@@ -220,7 +220,7 @@ Section Sets_as_an_algebra.
rewrite <- (Union_associative A (Singleton U y) (Singleton U x));
auto with sets.
Qed.
-
+
Lemma Add_commutative' :
forall (A:Ensemble U) (x y z:U),
Add U (Add U (Add U A x) y) z = Add U (Add U (Add U A z) x) y.
@@ -229,7 +229,7 @@ Section Sets_as_an_algebra.
rewrite (Add_commutative (Add U A x) y z).
rewrite (Add_commutative A x z); auto with sets.
Qed.
-
+
Lemma Add_distributes :
forall (A B:Ensemble U) (x y:U),
Included U B A -> Add U (Add U A x) y = Union U (Add U A x) (Add U B y).
diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v
index 64c4c654..85d0cffc 100644
--- a/theories/Sets/Relations_1.v
+++ b/theories/Sets/Relations_1.v
@@ -24,42 +24,42 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Relations_1.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id$ i*)
Section Relations_1.
Variable U : Type.
-
+
Definition Relation := U -> U -> Prop.
Variable R : Relation.
-
+
Definition Reflexive : Prop := forall x:U, R x x.
-
+
Definition Transitive : Prop := forall x y z:U, R x y -> R y z -> R x z.
-
+
Definition Symmetric : Prop := forall x y:U, R x y -> R y x.
-
+
Definition Antisymmetric : Prop := forall x y:U, R x y -> R y x -> x = y.
-
+
Definition contains (R R':Relation) : Prop :=
forall x y:U, R' x y -> R x y.
-
+
Definition same_relation (R R':Relation) : Prop :=
contains R R' /\ contains R' R.
-
+
Inductive Preorder : Prop :=
Definition_of_preorder : Reflexive -> Transitive -> Preorder.
-
+
Inductive Order : Prop :=
Definition_of_order :
Reflexive -> Transitive -> Antisymmetric -> Order.
-
+
Inductive Equivalence : Prop :=
Definition_of_equivalence :
Reflexive -> Transitive -> Symmetric -> Equivalence.
-
+
Inductive PER : Prop :=
Definition_of_PER : Symmetric -> Transitive -> PER.
-
+
End Relations_1.
Hint Unfold Reflexive Transitive Antisymmetric Symmetric contains
same_relation: sets v62.
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
index 6ee7f5e2..fd83b0e0 100644
--- a/theories/Sets/Relations_1_facts.v
+++ b/theories/Sets/Relations_1_facts.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Relations_1_facts.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id$ i*)
Require Export Relations_1.
diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v
index a74102fd..11ac85e8 100644
--- a/theories/Sets/Relations_2.v
+++ b/theories/Sets/Relations_2.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Relations_2.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id$ i*)
Require Export Relations_1.
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index 2374c2bf..3554901b 100644
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Relations_2_facts.v 10637 2008-03-07 23:52:56Z letouzey $ i*)
+(*i $Id$ i*)
Require Export Relations_1.
Require Export Relations_1_facts.
@@ -140,7 +140,7 @@ intros U R H' x b H'0; elim H'0.
intros x0 a H'1; exists a; auto with sets.
intros x0 y z H'1 H'2 H'3 a H'4.
red in H'.
-specialize H' with (x := x0) (a := a) (b := y); lapply H';
+specialize H' with (x := x0) (a := a) (b := y); lapply H';
[ intro H'8; lapply H'8;
[ intro H'9; try exact H'9; clear H'8 H' | clear H'8 H' ]
| clear H' ]; auto with sets.
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
index b8c65148..970db182 100644
--- a/theories/Sets/Relations_3.v
+++ b/theories/Sets/Relations_3.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Relations_3.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id$ i*)
Require Export Relations_1.
Require Export Relations_2.
@@ -32,26 +32,26 @@ Require Export Relations_2.
Section Relations_3.
Variable U : Type.
Variable R : Relation U.
-
+
Definition coherent (x y:U) : Prop :=
exists z : _, Rstar U R x z /\ Rstar U R y z.
-
+
Definition locally_confluent (x:U) : Prop :=
forall y z:U, R x y -> R x z -> coherent y z.
-
+
Definition Locally_confluent : Prop := forall x:U, locally_confluent x.
-
+
Definition confluent (x:U) : Prop :=
forall y z:U, Rstar U R x y -> Rstar U R x z -> coherent y z.
-
+
Definition Confluent : Prop := forall x:U, confluent x.
-
+
Inductive noetherian (x: U) : Prop :=
definition_of_noetherian :
(forall y:U, R x y -> noetherian y) -> noetherian x.
-
+
Definition Noetherian : Prop := forall x:U, noetherian x.
-
+
End Relations_3.
Hint Unfold coherent: sets v62.
Hint Unfold locally_confluent: sets v62.
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v
index 38ff9eae..d8bf7dc3 100644
--- a/theories/Sets/Relations_3_facts.v
+++ b/theories/Sets/Relations_3_facts.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Relations_3_facts.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id$ i*)
Require Export Relations_1.
Require Export Relations_1_facts.
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 42c96191..909c7983 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Uniset.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id$ i*)
(** Sets as characteristic functions *)
@@ -90,10 +90,10 @@ Qed.
Definition union (m1 m2:uniset) :=
Charac (fun a:A => orb (charac m1 a) (charac m2 a)).
-Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x).
-Proof.
-unfold seq in |- *; unfold union in |- *; simpl in |- *; auto.
-Qed.
+Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x).
+Proof.
+unfold seq in |- *; unfold union in |- *; simpl in |- *; auto.
+Qed.
Hint Resolve union_empty_left.
Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset).
@@ -203,7 +203,7 @@ apply uniset_twist2.
Qed.
-(*i theory of minter to do similarly
+(*i theory of minter to do similarly
Require Min.
(* uniset intersection *)
Definition minter := [m1,m2:uniset]
diff --git a/theories/Sets/vo.itarget b/theories/Sets/vo.itarget
new file mode 100644
index 00000000..9ebe92f5
--- /dev/null
+++ b/theories/Sets/vo.itarget
@@ -0,0 +1,22 @@
+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