summaryrefslogtreecommitdiff
path: root/theories/Sets
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /theories/Sets
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'theories/Sets')
-rwxr-xr-xtheories/Sets/Classical_sets.v132
-rwxr-xr-xtheories/Sets/Constructive_sets.v159
-rwxr-xr-xtheories/Sets/Cpo.v109
-rwxr-xr-xtheories/Sets/Ensembles.v101
-rwxr-xr-xtheories/Sets/Finite_sets.v81
-rwxr-xr-xtheories/Sets/Finite_sets_facts.v347
-rwxr-xr-xtheories/Sets/Image.v205
-rwxr-xr-xtheories/Sets/Infinite_sets.v244
-rwxr-xr-xtheories/Sets/Integers.v167
-rwxr-xr-xtheories/Sets/Multiset.v191
-rwxr-xr-xtheories/Sets/Partial_Order.v100
-rwxr-xr-xtheories/Sets/Permut.v91
-rwxr-xr-xtheories/Sets/Powerset.v190
-rwxr-xr-xtheories/Sets/Powerset_Classical_facts.v342
-rwxr-xr-xtheories/Sets/Powerset_facts.v268
-rwxr-xr-xtheories/Sets/Relations_1.v67
-rwxr-xr-xtheories/Sets/Relations_1_facts.v112
-rwxr-xr-xtheories/Sets/Relations_2.v56
-rwxr-xr-xtheories/Sets/Relations_2_facts.v153
-rwxr-xr-xtheories/Sets/Relations_3.v62
-rwxr-xr-xtheories/Sets/Relations_3_facts.v171
-rw-r--r--theories/Sets/Uniset.v215
-rwxr-xr-xtheories/Sets/intro.tex24
23 files changed, 3587 insertions, 0 deletions
diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
new file mode 100755
index 00000000..98cb14e4
--- /dev/null
+++ b/theories/Sets/Classical_sets.v
@@ -0,0 +1,132 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(****************************************************************************)
+(* *)
+(* Naive Set Theory in Coq *)
+(* *)
+(* INRIA INRIA *)
+(* Rocquencourt Sophia-Antipolis *)
+(* *)
+(* Coq V6.1 *)
+(* *)
+(* Gilles Kahn *)
+(* Gerard Huet *)
+(* *)
+(* *)
+(* *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
+(* to the Newton Institute for providing an exceptional work environment *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
+(****************************************************************************)
+
+(*i $Id: Classical_sets.v,v 1.4.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
+
+Require Export Ensembles.
+Require Export Constructive_sets.
+Require Export Classical_Type.
+
+(* Hints Unfold not . *)
+
+Section Ensembles_classical.
+Variable U : Type.
+
+Lemma not_included_empty_Inhabited :
+ forall A:Ensemble U, ~ Included U A (Empty_set U) -> Inhabited U A.
+Proof.
+intros A NI.
+elim (not_all_ex_not U (fun x:U => ~ In U A x)).
+intros x H; apply Inhabited_intro with x.
+apply NNPP; auto with sets.
+red in |- *; intro.
+apply NI; red in |- *.
+intros x H'; elim (H x); trivial with sets.
+Qed.
+Hint Resolve not_included_empty_Inhabited.
+
+Lemma not_empty_Inhabited :
+ forall A:Ensemble U, A <> Empty_set U -> Inhabited U A.
+Proof.
+intros; apply not_included_empty_Inhabited.
+red in |- *; auto with sets.
+Qed.
+
+Lemma Inhabited_Setminus :
+ 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.
+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.
+apply Setminus_intro.
+apply not_imply_elim with (In U X x); trivial with sets.
+auto with sets.
+Qed.
+Hint Resolve Inhabited_Setminus.
+
+Lemma Strict_super_set_contains_new_element :
+ forall X Y:Ensemble U,
+ Included U X Y -> X <> Y -> Inhabited U (Setminus U Y X).
+Proof.
+auto 7 with sets.
+Qed.
+Hint Resolve Strict_super_set_contains_new_element.
+
+Lemma Subtract_intro :
+ forall (A:Ensemble U) (x y:U), In U A y -> x <> y -> In U (Subtract U A x) y.
+Proof.
+unfold Subtract at 1 in |- *; auto with sets.
+Qed.
+Hint Resolve Subtract_intro.
+
+Lemma Subtract_inv :
+ forall (A:Ensemble U) (x y:U), In U (Subtract U A x) y -> In U A y /\ x <> y.
+Proof.
+intros A x y H'; elim H'; auto with sets.
+Qed.
+
+Lemma Included_Strict_Included :
+ forall X Y:Ensemble U, Included U X Y -> Strict_Included U X Y \/ X = Y.
+Proof.
+intros X Y H'; try assumption.
+elim (classic (X = Y)); auto with sets.
+Qed.
+
+Lemma Strict_Included_inv :
+ forall X Y:Ensemble U,
+ Strict_Included U X Y -> Included U X Y /\ Inhabited U (Setminus U Y X).
+Proof.
+intros X Y H'; red in H'.
+split; [ tauto | idtac ].
+elim H'; intros H'0 H'1; try exact H'1; clear H'.
+apply Strict_super_set_contains_new_element; auto with sets.
+Qed.
+
+Lemma not_SIncl_empty :
+ forall X:Ensemble U, ~ Strict_Included U X (Empty_set U).
+Proof.
+intro X; red in |- *; intro H'; try exact H'.
+lapply (Strict_Included_inv X (Empty_set U)); auto with sets.
+intro H'0; elim H'0; intros H'1 H'2; elim H'2; clear H'0.
+intros x H'0; elim H'0.
+intro H'3; elim H'3.
+Qed.
+
+Lemma Complement_Complement :
+ forall A:Ensemble U, Complement U (Complement U A) = A.
+Proof.
+unfold Complement in |- *; intros; apply Extensionality_Ensembles;
+ auto with sets.
+red in |- *; split; auto with sets.
+red in |- *; intros; apply NNPP; auto with sets.
+Qed.
+
+End Ensembles_classical.
+
+Hint Resolve Strict_super_set_contains_new_element Subtract_intro
+ not_SIncl_empty: sets v62. \ No newline at end of file
diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
new file mode 100755
index 00000000..a2bc781d
--- /dev/null
+++ b/theories/Sets/Constructive_sets.v
@@ -0,0 +1,159 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(****************************************************************************)
+(* *)
+(* Naive Set Theory in Coq *)
+(* *)
+(* INRIA INRIA *)
+(* Rocquencourt Sophia-Antipolis *)
+(* *)
+(* Coq V6.1 *)
+(* *)
+(* Gilles Kahn *)
+(* Gerard Huet *)
+(* *)
+(* *)
+(* *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
+(* to the Newton Institute for providing an exceptional work environment *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
+(****************************************************************************)
+
+(*i $Id: Constructive_sets.v,v 1.5.2.1 2004/07/16 19:31:17 herbelin Exp $ 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.
+Qed.
+
+Lemma Noone_in_empty : forall x:U, ~ In U (Empty_set U) x.
+Proof.
+red in |- *; destruct 1.
+Qed.
+Hint Resolve Noone_in_empty.
+
+Lemma Included_Empty : forall A:Ensemble U, Included U (Empty_set U) A.
+Proof.
+intro; red in |- *.
+intros x H; elim (Noone_in_empty x); auto with sets.
+Qed.
+Hint Resolve Included_Empty.
+
+Lemma Add_intro1 :
+ forall (A:Ensemble U) (x y:U), In U A y -> In U (Add U A x) y.
+Proof.
+unfold Add at 1 in |- *; auto with sets.
+Qed.
+Hint Resolve Add_intro1.
+
+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.
+Qed.
+Hint Resolve Add_intro2.
+
+Lemma Inhabited_add : forall (A:Ensemble U) (x:U), Inhabited U (Add U A x).
+Proof.
+intros A x.
+apply Inhabited_intro with (x := x); auto with sets.
+Qed.
+Hint Resolve Inhabited_add.
+
+Lemma Inhabited_not_empty :
+ forall X:Ensemble U, Inhabited U X -> X <> Empty_set U.
+Proof.
+intros X H'; elim H'.
+intros x H'0; red in |- *; intro H'1.
+absurd (In U X x); auto with sets.
+rewrite H'1; auto with sets.
+Qed.
+Hint Resolve Inhabited_not_empty.
+
+Lemma Add_not_Empty : forall (A:Ensemble U) (x:U), Add U A x <> Empty_set U.
+Proof.
+auto with sets.
+Qed.
+Hint Resolve Add_not_Empty.
+
+Lemma not_Empty_Add : forall (A:Ensemble U) (x:U), Empty_set U <> Add U A x.
+Proof.
+intros; red in |- *; intro H; generalize (Add_not_Empty A x); auto with sets.
+Qed.
+Hint Resolve not_Empty_Add.
+
+Lemma Singleton_inv : forall x y:U, In U (Singleton U x) y -> x = y.
+Proof.
+intros x y H'; elim H'; trivial with sets.
+Qed.
+Hint Resolve Singleton_inv.
+
+Lemma Singleton_intro : forall x y:U, x = y -> In U (Singleton U x) y.
+Proof.
+intros x y H'; rewrite H'; trivial with sets.
+Qed.
+Hint Resolve Singleton_intro.
+
+Lemma Union_inv :
+ forall (B C:Ensemble U) (x:U), In U (Union U B C) x -> In U B x \/ In U C x.
+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'; elim H'; auto with sets.
+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.
+Proof.
+intros B C x H'; elim H'; auto with sets.
+Qed.
+Hint Resolve Intersection_inv.
+
+Lemma Couple_inv : forall x y z:U, In U (Couple U x y) z -> z = x \/ z = y.
+Proof.
+intros x y z H'; elim H'; auto with sets.
+Qed.
+Hint Resolve Couple_inv.
+
+Lemma Setminus_intro :
+ forall (A B:Ensemble U) (x:U),
+ In U A x -> ~ In U B x -> In U (Setminus U A B) x.
+Proof.
+unfold Setminus at 1 in |- *; red in |- *; auto with sets.
+Qed.
+Hint Resolve Setminus_intro.
+
+Lemma Strict_Included_intro :
+ forall X Y:Ensemble U, Included U X Y /\ X <> Y -> Strict_Included U X Y.
+Proof.
+auto with sets.
+Qed.
+Hint Resolve Strict_Included_intro.
+
+Lemma Strict_Included_strict : forall X:Ensemble U, ~ Strict_Included U X X.
+Proof.
+intro X; red in |- *; intro H'; elim H'.
+intros H'0 H'1; elim H'1; auto with sets.
+Qed.
+Hint Resolve Strict_Included_strict.
+
+End Ensembles_facts.
+
+Hint Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2
+ Intersection_inv Couple_inv Setminus_intro Strict_Included_intro
+ Strict_Included_strict Noone_in_empty Inhabited_not_empty Add_not_Empty
+ not_Empty_Add Inhabited_add Included_Empty: sets v62. \ No newline at end of file
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
new file mode 100755
index 00000000..9fae12f5
--- /dev/null
+++ b/theories/Sets/Cpo.v
@@ -0,0 +1,109 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(****************************************************************************)
+(* *)
+(* Naive Set Theory in Coq *)
+(* *)
+(* INRIA INRIA *)
+(* Rocquencourt Sophia-Antipolis *)
+(* *)
+(* Coq V6.1 *)
+(* *)
+(* Gilles Kahn *)
+(* Gerard Huet *)
+(* *)
+(* *)
+(* *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
+(* to the Newton Institute for providing an exceptional work environment *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
+(****************************************************************************)
+
+(*i $Id: Cpo.v,v 1.5.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
+
+Require Export Ensembles.
+Require Export Relations_1.
+Require Export Partial_Order.
+
+Section Bounds.
+Variable U : Type.
+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 :=
+ Upper_Bound_definition :
+ In U C x -> (forall y:U, In U B y -> R y x) -> Upper_Bound B x.
+
+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.
+
+Inductive Glb (B:Ensemble U) (x:U) : Prop :=
+ Glb_definition :
+ Lower_Bound B x -> (forall y:U, Lower_Bound B y -> R y x) -> Glb B x.
+
+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 ->
+ forall x y:U, Included U (Couple U x y) B -> R x y \/ R y x) ->
+ Totally_ordered B.
+
+Definition Compatible : Relation U :=
+ fun x y:U =>
+ In U C x ->
+ In U C y -> exists z : _, In U C z /\ Upper_Bound (Couple U x y) z.
+
+Inductive Directed (X:Ensemble U) : Prop :=
+ Definition_of_Directed :
+ Included U X C ->
+ Inhabited U X ->
+ (forall x1 x2:U,
+ 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) ->
+ (forall X:Ensemble U, Directed X -> exists bsup : _, Lub X bsup) ->
+ Complete.
+
+Inductive Conditionally_complete : Prop :=
+ Definition_of_Conditionally_complete :
+ (forall X:Ensemble U,
+ Included U X C ->
+ (exists maj : _, Upper_Bound X maj) ->
+ exists bsup : _, Lub X bsup) -> Conditionally_complete.
+End Bounds.
+Hint Resolve Totally_ordered_definition Upper_Bound_definition
+ Lower_Bound_definition Lub_definition Glb_definition Bottom_definition
+ Definition_of_Complete Definition_of_Complete
+ Definition_of_Conditionally_complete.
+
+Section Specific_orders.
+Variable U : Type.
+
+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)}.
+
+End Specific_orders. \ No newline at end of file
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
new file mode 100755
index 00000000..05afc298
--- /dev/null
+++ b/theories/Sets/Ensembles.v
@@ -0,0 +1,101 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(****************************************************************************)
+(* *)
+(* Naive Set Theory in Coq *)
+(* *)
+(* INRIA INRIA *)
+(* Rocquencourt Sophia-Antipolis *)
+(* *)
+(* Coq V6.1 *)
+(* *)
+(* Gilles Kahn *)
+(* Gerard Huet *)
+(* *)
+(* *)
+(* *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
+(* to the Newton Institute for providing an exceptional work environment *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
+(****************************************************************************)
+
+(*i $Id: Ensembles.v,v 1.7.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
+
+Section Ensembles.
+Variable U : Type.
+
+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.
+
+ 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 :=
+ In_singleton : In (Singleton x) x.
+
+Inductive Union (B C:Ensemble) : Ensemble :=
+ | Union_introl : forall x:U, In B x -> In (Union B C) x
+ | 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.
+
+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.
+Hint Resolve Extensionality_Ensembles.
+
+End Ensembles.
+
+Hint Unfold In Included Same_set Strict_Included Add Setminus Subtract: sets
+ v62.
+
+Hint Resolve Union_introl Union_intror Intersection_intro In_singleton
+ Couple_l Couple_r Triple_l Triple_m Triple_r Disjoint_intro
+ Extensionality_Ensembles: sets v62. \ No newline at end of file
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
new file mode 100755
index 00000000..5a2e4397
--- /dev/null
+++ b/theories/Sets/Finite_sets.v
@@ -0,0 +1,81 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(****************************************************************************)
+(* *)
+(* Naive Set Theory in Coq *)
+(* *)
+(* INRIA INRIA *)
+(* Rocquencourt Sophia-Antipolis *)
+(* *)
+(* Coq V6.1 *)
+(* *)
+(* Gilles Kahn *)
+(* Gerard Huet *)
+(* *)
+(* *)
+(* *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
+(* to the Newton Institute for providing an exceptional work environment *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
+(****************************************************************************)
+
+(*i $Id: Finite_sets.v,v 1.6.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
+
+Require Import Ensembles.
+
+Section Ensembles_finis.
+Variable U : Type.
+
+Inductive Finite : Ensemble U -> Prop :=
+ | Empty_is_finite : Finite (Empty_set U)
+ | Union_is_finite :
+ forall A:Ensemble U,
+ Finite A -> forall x:U, ~ In U A x -> Finite (Add U A x).
+
+Inductive cardinal : Ensemble U -> nat -> Prop :=
+ | card_empty : cardinal (Empty_set U) 0
+ | card_add :
+ forall (A:Ensemble U) (n:nat),
+ cardinal A n -> forall x:U, ~ In U A x -> cardinal (Add U A x) (S n).
+
+End Ensembles_finis.
+
+Hint Resolve Empty_is_finite Union_is_finite: sets v62.
+Hint Resolve card_empty card_add: sets v62.
+
+Require Import Constructive_sets.
+
+Section Ensembles_finis_facts.
+Variable U : Type.
+
+Lemma cardinal_invert :
+ forall (X:Ensemble U) (p:nat),
+ cardinal U X p ->
+ match p with
+ | O => X = Empty_set U
+ | S n =>
+ exists A : _,
+ (exists x : _, X = Add U A x /\ ~ In U A x /\ cardinal U A n)
+ end.
+Proof.
+induction 1; simpl in |- *; auto.
+exists A; exists x; auto.
+Qed.
+
+Lemma cardinal_elim :
+ forall (X:Ensemble U) (p:nat),
+ cardinal U X p ->
+ match p with
+ | O => X = Empty_set U
+ | S n => Inhabited U X
+ end.
+Proof.
+intros X p C; elim C; simpl in |- *; trivial with sets.
+Qed.
+
+End Ensembles_finis_facts.
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
new file mode 100755
index 00000000..952965e8
--- /dev/null
+++ b/theories/Sets/Finite_sets_facts.v
@@ -0,0 +1,347 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(****************************************************************************)
+(* *)
+(* Naive Set Theory in Coq *)
+(* *)
+(* INRIA INRIA *)
+(* Rocquencourt Sophia-Antipolis *)
+(* *)
+(* Coq V6.1 *)
+(* *)
+(* Gilles Kahn *)
+(* Gerard Huet *)
+(* *)
+(* *)
+(* *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
+(* to the Newton Institute for providing an exceptional work environment *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
+(****************************************************************************)
+
+(*i $Id: Finite_sets_facts.v,v 1.7.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
+
+Require Export Finite_sets.
+Require Export Constructive_sets.
+Require Export Classical_Type.
+Require Export Classical_sets.
+Require Export Powerset.
+Require Export Powerset_facts.
+Require Export Powerset_Classical_facts.
+Require Export Gt.
+Require Export Lt.
+
+Section Finite_sets_facts.
+Variable U : Type.
+
+Lemma finite_cardinal :
+ forall X:Ensemble U, Finite U X -> exists n : nat, cardinal U X n.
+Proof.
+induction 1 as [| A _ [n H]].
+exists 0; auto with sets.
+exists (S n); auto with sets.
+Qed.
+
+Lemma cardinal_finite :
+ forall (X:Ensemble U) (n:nat), cardinal U X n -> Finite U X.
+Proof.
+induction 1; auto with sets.
+Qed.
+
+Theorem Add_preserves_Finite :
+ forall (X:Ensemble U) (x:U), Finite U X -> Finite U (Add U X x).
+Proof.
+intros X x H'.
+elim (classic (In U X x)); intro H'0; auto with sets.
+rewrite (Non_disjoint_union U X x); auto with sets.
+Qed.
+Hint Resolve Add_preserves_Finite.
+
+Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x).
+Proof.
+intro x; rewrite <- (Empty_set_zero U (Singleton U x)).
+change (Finite U (Add U (Empty_set U) x)) in |- *; auto with sets.
+Qed.
+Hint Resolve Singleton_is_finite.
+
+Theorem Union_preserves_Finite :
+ forall X Y:Ensemble U, Finite U X -> Finite U Y -> Finite U (Union U X Y).
+Proof.
+intros X Y H'; elim H'.
+rewrite (Empty_set_zero U Y); auto with sets.
+intros A H'0 H'1 x H'2 H'3.
+rewrite (Union_commutative U (Add U A x) Y).
+rewrite <- (Union_add U Y A x).
+rewrite (Union_commutative U Y A); auto with sets.
+Qed.
+
+Lemma Finite_downward_closed :
+ forall A:Ensemble U,
+ Finite U A -> forall X:Ensemble U, Included U X A -> Finite U X.
+Proof.
+intros A H'; elim H'; auto with sets.
+intros X H'0.
+rewrite (less_than_empty U X H'0); auto with sets.
+intros; elim Included_Add with U X A0 x; auto with sets.
+destruct 1 as [A' [H5 H6]].
+rewrite H5; auto with sets.
+Qed.
+
+Lemma Intersection_preserves_finite :
+ forall A:Ensemble U,
+ Finite U A -> forall X:Ensemble U, Finite U (Intersection U X A).
+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.
+intros X H; apply (cardinal_invert U X 0); trivial with sets.
+Qed.
+Hint Resolve cardinalO_empty.
+
+Lemma inh_card_gt_O :
+ forall X:Ensemble U, Inhabited U X -> forall n:nat, cardinal U X n -> n > 0.
+Proof.
+induction 1 as [x H'].
+intros n H'0.
+elim (gt_O_eq n); auto with sets.
+intro H'1; generalize H'; generalize H'0.
+rewrite <- H'1; intro H'2.
+rewrite (cardinalO_empty X); auto with sets.
+intro H'3; elim H'3.
+Qed.
+
+Lemma card_soustr_1 :
+ forall (X:Ensemble U) (n:nat),
+ cardinal U X n ->
+ forall x:U, In U X x -> cardinal U (Subtract U X x) (pred n).
+Proof.
+intros X n H'; elim H'.
+intros x H'0; elim H'0.
+clear H' n X.
+intros X n H' H'0 x H'1 x0 H'2.
+elim (classic (In U X x0)).
+intro H'4; rewrite (add_soustr_xy U X x x0).
+elim (classic (x = x0)).
+intro H'5.
+absurd (In U X x0); auto with sets.
+rewrite <- H'5; auto with sets.
+intro H'3; try assumption.
+cut (S (pred n) = pred (S n)).
+intro H'5; rewrite <- H'5.
+apply card_add; auto with sets.
+red in |- *; intro H'6; elim H'6.
+intros H'7 H'8; try assumption.
+elim H'1; auto with sets.
+unfold pred at 2 in |- *; symmetry in |- *.
+apply S_pred with (m := 0).
+change (n > 0) in |- *.
+apply inh_card_gt_O with (X := X); auto with sets.
+apply Inhabited_intro with (x := x0); auto with sets.
+red in |- *; intro H'3.
+apply H'1.
+elim H'3; auto with sets.
+rewrite H'3; auto with sets.
+elim (classic (x = x0)).
+intro H'3; rewrite <- H'3.
+cut (Subtract U (Add U X x) x = X); auto with sets.
+intro H'4; rewrite H'4; auto with sets.
+intros H'3 H'4; try assumption.
+absurd (In U (Add U X x) x0); auto with sets.
+red in |- *; intro H'5; try exact H'5.
+lapply (Add_inv U X x x0); tauto.
+Qed.
+
+Lemma cardinal_is_functional :
+ forall (X:Ensemble U) (c1:nat),
+ cardinal U X c1 ->
+ forall (Y:Ensemble U) (c2:nat), cardinal U Y c2 -> X = Y -> c1 = c2.
+Proof.
+intros X c1 H'; elim H'.
+intros Y c2 H'0; elim H'0; auto with sets.
+intros A n H'1 H'2 x H'3 H'5.
+elim (not_Empty_Add U A x); auto with sets.
+clear H' c1 X.
+intros X n H' H'0 x H'1 Y c2 H'2.
+elim H'2.
+intro H'3.
+elim (not_Empty_Add U X x); auto with sets.
+clear H'2 c2 Y.
+intros X0 c2 H'2 H'3 x0 H'4 H'5.
+elim (classic (In U X0 x)).
+intro H'6; apply f_equal with nat.
+apply H'0 with (Y := Subtract U (Add U X0 x0) x).
+elimtype (pred (S c2) = c2); auto with sets.
+apply card_soustr_1; auto with sets.
+rewrite <- H'5.
+apply Sub_Add_new; auto with sets.
+elim (classic (x = x0)).
+intros H'6 H'7; apply f_equal with nat.
+apply H'0 with (Y := X0); auto with sets.
+apply Simplify_add with (x := x); auto with sets.
+pattern x at 2 in |- *; rewrite H'6; auto with sets.
+intros H'6 H'7.
+absurd (Add U X x = Add U X0 x0); auto with sets.
+clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2.
+red in |- *; intro H'.
+lapply (Extension U (Add U X x) (Add U X0 x0)); auto with sets.
+clear H'.
+intro H'; red in H'.
+elim H'; intros H'0 H'1; red in H'0; clear H' H'1.
+absurd (In U (Add U X0 x0) x); auto with sets.
+lapply (Add_inv U X0 x0 x); [ intuition | apply (H'0 x); apply Add_intro2 ].
+Qed.
+
+Lemma cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m.
+Proof.
+intros m Cm; generalize (cardinal_invert U (Empty_set U) m Cm).
+elim m; auto with sets.
+intros; elim H0; intros; elim H1; intros; elim H2; intros.
+elim (not_Empty_Add U x x0 H3).
+Qed.
+
+Lemma cardinal_unicity :
+ forall (X:Ensemble U) (n:nat),
+ cardinal U X n -> forall m:nat, cardinal U X m -> n = m.
+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.
+Proof.
+intros A x n n' H'.
+elim (classic (In U A x)).
+intro H'0.
+rewrite (Non_disjoint_union U A x H'0).
+intro H'1; cut (n = n').
+intro E; rewrite E; auto with sets.
+apply cardinal_unicity with A; auto with sets.
+intros H'0 H'1.
+cut (n' = S n).
+intro E; rewrite E; auto with sets.
+apply cardinal_unicity with (Add U A x); auto with sets.
+Qed.
+
+Lemma incl_st_card_lt :
+ forall (X:Ensemble U) (c1:nat),
+ cardinal U X c1 ->
+ forall (Y:Ensemble U) (c2:nat),
+ cardinal U Y c2 -> Strict_Included U X Y -> c2 > c1.
+Proof.
+intros X c1 H'; elim H'.
+intros Y c2 H'0; elim H'0; auto with sets arith.
+intro H'1.
+elim (Strict_Included_strict U (Empty_set U)); auto with sets arith.
+clear H' c1 X.
+intros X n H' H'0 x H'1 Y c2 H'2.
+elim H'2.
+intro H'3; elim (not_SIncl_empty U (Add U X x)); auto with sets arith.
+clear H'2 c2 Y.
+intros X0 c2 H'2 H'3 x0 H'4 H'5; elim (classic (In U X0 x)).
+intro H'6; apply gt_n_S.
+apply H'0 with (Y := Subtract U (Add U X0 x0) x).
+elimtype (pred (S c2) = c2); auto with sets arith.
+apply card_soustr_1; auto with sets arith.
+apply incl_st_add_soustr; auto with sets arith.
+elim (classic (x = x0)).
+intros H'6 H'7; apply gt_n_S.
+apply H'0 with (Y := X0); auto with sets arith.
+apply sincl_add_x with (x := x0).
+rewrite <- H'6; auto with sets arith.
+pattern x0 at 1 in |- *; rewrite <- H'6; trivial with sets arith.
+intros H'6 H'7; red in H'5.
+elim H'5; intros H'8 H'9; try exact H'8; clear H'5.
+red in H'8.
+generalize (H'8 x).
+intro H'5; lapply H'5; auto with sets arith.
+intro H; elim Add_inv with U X0 x0 x; auto with sets arith.
+intro; absurd (In U X0 x); auto with sets arith.
+intro; absurd (x = x0); auto with sets arith.
+Qed.
+
+Lemma incl_card_le :
+ forall (X Y:Ensemble U) (n m:nat),
+ cardinal U X n -> cardinal U Y m -> Included U X Y -> n <= m.
+Proof.
+intros; elim Included_Strict_Included with U X Y; auto with sets arith; intro.
+cut (m > n); auto with sets arith.
+apply incl_st_card_lt with (X := X) (Y := Y); auto with sets arith.
+generalize H0; rewrite <- H2; intro.
+cut (n = m).
+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,
+ Finite U X ->
+ (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
+ P (Empty_set U).
+Proof.
+intros P H'; try assumption.
+apply H'; auto with sets.
+clear H'; auto with sets.
+intros Y H'; try assumption.
+red in H'.
+elim H'; intros H'0 H'1; try exact H'1; clear H'.
+lapply (less_than_empty U Y); [ intro H'3; try exact H'3 | assumption ].
+elim H'1; auto with sets.
+Qed.
+
+Hint Unfold not.
+
+Lemma Generalized_induction_on_finite_sets :
+ forall P:Ensemble U -> Prop,
+ (forall X:Ensemble U,
+ Finite U X ->
+ (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
+ forall X:Ensemble U, Finite U X -> P X.
+Proof.
+intros P H'0 X H'1.
+generalize P H'0; clear H'0 P.
+elim H'1.
+intros P H'0.
+apply G_aux; auto with sets.
+clear H'1 X.
+intros A H' H'0 x H'1 P H'3.
+cut (forall Y:Ensemble U, Included U Y (Add U A x) -> P Y); auto with sets.
+generalize H'1.
+apply H'0.
+intros X K H'5 L Y H'6; apply H'3; auto with sets.
+apply Finite_downward_closed with (A := Add U X x); auto with sets.
+intros Y0 H'7.
+elim (Strict_inclusion_is_transitive_with_inclusion U Y0 Y (Add U X x));
+ auto with sets.
+intros H'2 H'4.
+elim (Included_Add U Y0 X x);
+ [ intro H'14
+ | intro H'14; elim H'14; intros A' E; elim E; intros H'15 H'16; clear E H'14
+ | idtac ]; auto with sets.
+elim (Included_Strict_Included U Y0 X); auto with sets.
+intro H'9; apply H'5 with (Y := Y0); auto with sets.
+intro H'9; rewrite H'9.
+apply H'3; auto with sets.
+intros Y1 H'8; elim H'8.
+intros H'10 H'11; apply H'5 with (Y := Y1); auto with sets.
+elim (Included_Strict_Included U A' X); auto with sets.
+intro H'8; apply H'5 with (Y := A'); auto with sets.
+rewrite <- H'15; auto with sets.
+intro H'8.
+elim H'7.
+intros H'9 H'10; apply H'10 || elim H'10; try assumption.
+generalize H'6.
+rewrite <- H'8.
+rewrite <- H'15; auto with sets.
+Qed.
+
+End Finite_sets_facts. \ No newline at end of file
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
new file mode 100755
index 00000000..f58f2f81
--- /dev/null
+++ b/theories/Sets/Image.v
@@ -0,0 +1,205 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(****************************************************************************)
+(* *)
+(* Naive Set Theory in Coq *)
+(* *)
+(* INRIA INRIA *)
+(* Rocquencourt Sophia-Antipolis *)
+(* *)
+(* Coq V6.1 *)
+(* *)
+(* Gilles Kahn *)
+(* Gerard Huet *)
+(* *)
+(* *)
+(* *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
+(* to the Newton Institute for providing an exceptional work environment *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
+(****************************************************************************)
+
+(*i $Id: Image.v,v 1.6.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
+
+Require Export Finite_sets.
+Require Export Constructive_sets.
+Require Export Classical_Type.
+Require Export Classical_sets.
+Require Export Powerset.
+Require Export Powerset_facts.
+Require Export Powerset_Classical_facts.
+Require Export Gt.
+Require Export Lt.
+Require Export Le.
+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.
+intros X f x H'; try assumption.
+apply Im_intro with (x := x); auto with sets.
+Qed.
+Hint Resolve Im_def.
+
+Lemma Im_add :
+ forall (X:Ensemble U) (x:U) (f:U -> V),
+ Im (Add _ X x) f = Add _ (Im X f) (f x).
+Proof.
+intros X x f.
+apply Extensionality_Ensembles.
+split; red in |- *; intros x0 H'.
+elim H'; intros.
+rewrite H0.
+elim Add_inv with U X x x1; auto with sets.
+destruct 1; auto with sets.
+elim Add_inv with V (Im X f) (f x) x0; auto with sets.
+destruct 1 as [x0 H y H0].
+rewrite H0; auto with sets.
+destruct 1; auto with sets.
+Qed.
+
+Lemma image_empty : forall f:U -> V, Im (Empty_set U) f = Empty_set V.
+Proof.
+intro f; try assumption.
+apply Extensionality_Ensembles.
+split; auto with sets.
+red in |- *.
+intros x H'; elim H'.
+intros x0 H'0; elim H'0; auto with sets.
+Qed.
+Hint Resolve image_empty.
+
+Lemma finite_image :
+ forall (X:Ensemble U) (f:U -> V), Finite _ X -> Finite _ (Im X f).
+Proof.
+intros X f H'; elim H'.
+rewrite (image_empty f); auto with sets.
+intros A H'0 H'1 x H'2; clear H' X.
+rewrite (Im_add A x f); auto with sets.
+apply Add_preserves_Finite; auto with sets.
+Qed.
+Hint Resolve finite_image.
+
+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.
+Proof.
+intros X f y H'; elim H'.
+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).
+Proof.
+unfold injective in |- *; intros f H.
+cut (exists x : _, ~ (forall y:U, f x = f y -> x = y)).
+2: apply not_all_ex_not with (P := fun x:U => forall y:U, f x = f y -> x = y);
+ trivial with sets.
+destruct 1 as [x C]; exists x.
+cut (exists y : _, ~ (f x = f y -> x = y)).
+2: apply not_all_ex_not with (P := fun y:U => f x = f y -> x = y);
+ trivial with sets.
+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.
+Proof.
+intros.
+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.
+Proof.
+intros.
+elim Im_inv with A f (f x); trivial with sets.
+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 ->
+ cardinal _ A n -> forall n':nat, cardinal _ (Im A f) n' -> n' = n.
+Proof.
+induction 2 as [| A n H'0 H'1 x H'2]; auto with sets.
+rewrite (image_empty f).
+intros n' CE.
+apply cardinal_unicity with V (Empty_set V); auto with sets.
+intro n'.
+rewrite (Im_add A x f).
+intro H'3.
+elim cardinal_Im_intro with A f n; trivial with sets.
+intros i CI.
+lapply (H'1 i); trivial with sets.
+cut (~ In _ (Im A f) (f x)).
+intros H0 H1.
+apply cardinal_unicity with V (Add _ (Im A f) (f x)); trivial with sets.
+apply card_add; auto with sets.
+rewrite <- H1; trivial with sets.
+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.
+Proof.
+induction 1 as [| A n H'0 H'1 x H'2]; auto with sets.
+rewrite (image_empty f); intros.
+cut (n' = 0).
+intro E; rewrite E; trivial with sets.
+apply cardinal_unicity with V (Empty_set V); auto with sets.
+intro n'.
+rewrite (Im_add A x f).
+elim cardinal_Im_intro with A f n; trivial with sets.
+intros p C H'3.
+apply le_trans with (S p).
+apply card_Add_gen with V (Im A f) (f x); trivial with sets.
+apply le_n_S; auto with sets.
+Qed.
+
+Theorem Pigeonhole :
+ forall (A:Ensemble U) (f:U -> V) (n:nat),
+ cardinal U A n ->
+ forall n':nat, cardinal V (Im A f) n' -> n' < n -> ~ injective f.
+Proof.
+unfold not in |- *; intros A f n CAn n' CIfn' ltn'n I.
+cut (n' = n).
+intro E; generalize ltn'n; rewrite E; exact (lt_irrefl n).
+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 ->
+ forall n':nat,
+ cardinal _ (Im A f) n' ->
+ n' < n -> exists x : _, (exists y : _, f x = f y /\ x <> y).
+Proof.
+intros; apply not_injective_elim.
+apply Pigeonhole with A n n'; trivial with sets.
+Qed.
+End Image.
+Hint Resolve Im_def image_empty finite_image: sets v62. \ No newline at end of file
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
new file mode 100755
index 00000000..c357e26c
--- /dev/null
+++ b/theories/Sets/Infinite_sets.v
@@ -0,0 +1,244 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(****************************************************************************)
+(* *)
+(* Naive Set Theory in Coq *)
+(* *)
+(* INRIA INRIA *)
+(* Rocquencourt Sophia-Antipolis *)
+(* *)
+(* Coq V6.1 *)
+(* *)
+(* Gilles Kahn *)
+(* Gerard Huet *)
+(* *)
+(* *)
+(* *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
+(* to the Newton Institute for providing an exceptional work environment *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
+(****************************************************************************)
+
+(*i $Id: Infinite_sets.v,v 1.5.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
+
+Require Export Finite_sets.
+Require Export Constructive_sets.
+Require Export Classical_Type.
+Require Export Classical_sets.
+Require Export Powerset.
+Require Export Powerset_facts.
+Require Export Powerset_Classical_facts.
+Require Export Gt.
+Require Export Lt.
+Require Export Le.
+Require Export Finite_sets_facts.
+Require Export Image.
+
+Section Approx.
+Variable U : Type.
+
+Inductive Approximant (A X:Ensemble U) : Prop :=
+ Defn_of_Approximant : Finite U X -> Included U X A -> Approximant A X.
+End Approx.
+
+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).
+Proof.
+intros A X H' H'0.
+elim H'0; intros H'1 H'2.
+apply Strict_super_set_contains_new_element; auto with 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 ->
+ forall n:nat,
+ cardinal U X n ->
+ Included U X A -> exists Y : _, cardinal U Y (S n) /\ Included U Y A.
+Proof.
+intros A X H' n H'0; elim H'0; auto with sets.
+intro H'1.
+cut (Inhabited U (Setminus U A (Empty_set U))).
+intro H'2; elim H'2.
+intros x H'3.
+exists (Add U (Empty_set U) x); auto with sets.
+split.
+apply card_add; auto with sets.
+cut (In U A x).
+intro H'4; red in |- *; auto with sets.
+intros x0 H'5; elim H'5; auto with sets.
+intros x1 H'6; elim H'6; auto with sets.
+elim H'3; auto with sets.
+apply make_new_approximant; auto with sets.
+intros A0 n0 H'1 H'2 x H'3 H'5.
+lapply H'2; [ intro H'6; elim H'6; clear H'2 | clear H'2 ]; auto with sets.
+intros x0 H'2; try assumption.
+elim H'2; intros H'7 H'8; try exact H'8; clear H'2.
+elim (make_new_approximant A x0); auto with sets.
+intros x1 H'2; try assumption.
+exists (Add U x0 x1); auto with sets.
+split.
+apply card_add; auto with sets.
+elim H'2; auto with sets.
+red in |- *.
+intros x2 H'9; elim H'9; auto with sets.
+intros x3 H'10; elim H'10; auto with sets.
+elim H'2; auto with sets.
+auto with 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 ->
+ forall n:nat,
+ cardinal U X n ->
+ Approximant U A X ->
+ exists Y : _, cardinal U Y (S n) /\ Approximant U A Y.
+Proof.
+intros A X H' n H'0 H'1; try assumption.
+elim H'1.
+intros H'2 H'3.
+elimtype (exists Y : _, cardinal U Y (S n) /\ Included U Y A).
+intros x H'4; elim H'4; intros H'5 H'6; try exact H'5; clear H'4.
+exists x; auto with sets.
+split; [ auto with sets | idtac ].
+apply Defn_of_Approximant; auto with 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 ->
+ forall n:nat, exists Y : _, cardinal U Y n /\ Approximant U A Y.
+Proof.
+intros A H' H'0 n; elim n.
+exists (Empty_set U); auto with sets.
+intros n0 H'1; elim H'1.
+intros x H'2.
+apply approximants_grow' with (X := x); tauto.
+Qed.
+
+Variable V : Type.
+
+Theorem Image_set_continuous :
+ forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
+ Finite V X ->
+ Included V X (Im U V A f) ->
+ exists n : _,
+ (exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X).
+Proof.
+intros A f X H'; elim H'.
+intro H'0; exists 0.
+exists (Empty_set U); auto with sets.
+intros A0 H'0 H'1 x H'2 H'3; try assumption.
+lapply H'1;
+ [ intro H'4; elim H'4; intros n E; elim E; clear H'4 H'1 | clear H'1 ];
+ auto with sets.
+intros x0 H'1; try assumption.
+exists (S n); try assumption.
+elim H'1; intros H'4 H'5; elim H'4; intros H'6 H'7; try exact H'6;
+ clear H'4 H'1.
+clear E.
+generalize H'2.
+rewrite <- H'5.
+intro H'1; try assumption.
+red in H'3.
+generalize (H'3 x).
+intro H'4; lapply H'4; [ intro H'8; try exact H'8; clear H'4 | clear H'4 ];
+ auto with sets.
+specialize 5Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x);
+ intro H'11; lapply H'11; [ intro H'13; elim H'11; clear H'11 | clear H'11 ];
+ auto with sets.
+intros x1 H'4; try assumption.
+apply ex_intro with (x := Add U x0 x1).
+split; [ split; [ try assumption | idtac ] | idtac ].
+apply card_add; auto with sets.
+red in |- *; intro H'9; try exact H'9.
+apply H'1.
+elim H'4; intros H'10 H'11; rewrite <- H'11; clear H'4; auto with sets.
+elim H'4; intros H'9 H'10; try exact H'9; clear H'4; auto with sets.
+red in |- *; auto with sets.
+intros x2 H'4; elim H'4; auto with sets.
+intros x3 H'11; elim H'11; auto with sets.
+elim H'4; intros H'9 H'10; rewrite <- H'10; clear H'4; auto with sets.
+apply Im_add; auto with sets.
+Qed.
+
+Theorem Image_set_continuous' :
+ forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
+ Approximant V (Im U V A f) X ->
+ exists Y : _, Approximant U A Y /\ Im U V Y f = X.
+Proof.
+intros A f X H'; try assumption.
+cut
+ (exists n : _,
+ (exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X)).
+intro H'0; elim H'0; intros n E; elim E; clear H'0.
+intros x H'0; try assumption.
+elim H'0; intros H'1 H'2; elim H'1; intros H'3 H'4; try exact H'3;
+ clear H'1 H'0; auto with sets.
+exists x.
+split; [ idtac | try assumption ].
+apply Defn_of_Approximant; auto with sets.
+apply cardinal_finite with (n := n); auto with sets.
+apply Image_set_continuous; auto with sets.
+elim H'; auto with sets.
+elim H'; auto with sets.
+Qed.
+
+Theorem Pigeonhole_bis :
+ forall (A:Ensemble U) (f:U -> V),
+ ~ Finite U A -> Finite V (Im U V A f) -> ~ injective U V f.
+Proof.
+intros A f H'0 H'1; try assumption.
+elim (Image_set_continuous' A f (Im U V A f)); auto with sets.
+intros x H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.
+elim (make_new_approximant A x); auto with sets.
+intros x0 H'2; elim H'2.
+intros H'5 H'6.
+elim (finite_cardinal V (Im U V A f)); auto with sets.
+intros n E.
+elim (finite_cardinal U x); auto with sets.
+intros n0 E0.
+apply Pigeonhole with (A := Add U x x0) (n := S n0) (n' := n).
+apply card_add; auto with sets.
+rewrite (Im_add U V x x0 f); auto with sets.
+cut (In V (Im U V x f) (f x0)).
+intro H'8.
+rewrite (Non_disjoint_union V (Im U V x f) (f x0)); auto with sets.
+rewrite H'4; auto with sets.
+elim (Extension V (Im U V x f) (Im U V A f)); auto with sets.
+apply le_lt_n_Sm.
+apply cardinal_decreases with (U := U) (V := V) (A := x) (f := f);
+ auto with 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.
+Proof.
+intros A f H' H'0 H'1.
+apply NNPP.
+red in |- *; intro H'2.
+elim (Pigeonhole_bis A f); auto with sets.
+Qed.
+
+End Infinite_sets.
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
new file mode 100755
index 00000000..26f29c96
--- /dev/null
+++ b/theories/Sets/Integers.v
@@ -0,0 +1,167 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(****************************************************************************)
+(* *)
+(* Naive Set Theory in Coq *)
+(* *)
+(* INRIA INRIA *)
+(* Rocquencourt Sophia-Antipolis *)
+(* *)
+(* Coq V6.1 *)
+(* *)
+(* Gilles Kahn *)
+(* Gerard Huet *)
+(* *)
+(* *)
+(* *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
+(* to the Newton Institute for providing an exceptional work environment *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
+(****************************************************************************)
+
+(*i $Id: Integers.v,v 1.6.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
+
+Require Export Finite_sets.
+Require Export Constructive_sets.
+Require Export Classical_Type.
+Require Export Classical_sets.
+Require Export Powerset.
+Require Export Powerset_facts.
+Require Export Powerset_Classical_facts.
+Require Export Gt.
+Require Export Lt.
+Require Export Le.
+Require Export Finite_sets_facts.
+Require Export Image.
+Require Export Infinite_sets.
+Require Export Compare_dec.
+Require Export Relations_1.
+Require Export Partial_Order.
+Require Export Cpo.
+
+Section Integers_sect.
+
+Inductive Integers : Ensemble nat :=
+ Integers_defn : forall x:nat, In nat Integers x.
+Hint Resolve Integers_defn.
+
+Lemma le_reflexive : Reflexive nat le.
+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.
+Qed.
+
+Lemma le_trans : Transitive nat le.
+Proof.
+red in |- *; intros; apply le_trans with y; auto.
+Qed.
+Hint Resolve le_reflexive le_antisym le_trans.
+
+Lemma le_Order : Order nat le.
+Proof.
+auto with sets arith.
+Qed.
+Hint Resolve le_Order.
+
+Lemma triv_nat : forall n:nat, In nat Integers n.
+Proof.
+auto with sets arith.
+Qed.
+Hint Resolve triv_nat.
+
+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); auto with sets arith.
+Defined.
+Hint Unfold nat_po.
+
+Lemma le_total_order : Totally_ordered nat nat_po Integers.
+Proof.
+apply Totally_ordered_definition.
+simpl in |- *.
+intros H' x y H'0.
+specialize 2le_or_lt with (n := x) (m := y); intro H'2; elim H'2.
+intro H'1; left; auto with sets arith.
+intro H'1; right.
+cut (y <= x); auto with sets arith.
+Qed.
+Hint Resolve le_total_order.
+
+Lemma Finite_subset_has_lub :
+ forall X:Ensemble nat,
+ Finite nat X -> exists m : nat, Upper_Bound nat nat_po X m.
+Proof.
+intros X H'; elim H'.
+exists 0.
+apply Upper_Bound_definition; auto with sets arith.
+intros y H'0; elim H'0; auto with sets arith.
+intros A H'0 H'1 x H'2; try assumption.
+elim H'1; intros x0 H'3; clear H'1.
+elim le_total_order.
+simpl in |- *.
+intro H'1; try assumption.
+lapply H'1; [ intro H'4; idtac | try assumption ]; auto with sets arith.
+generalize (H'4 x0 x).
+clear H'4.
+clear H'1.
+intro H'1; lapply H'1;
+ [ intro H'4; elim H'4;
+ [ intro H'5; try exact H'5; clear H'4 H'1 | intro H'5; clear H'4 H'1 ]
+ | clear H'1 ].
+exists x.
+apply Upper_Bound_definition; auto with sets arith; simpl in |- *.
+intros y H'1; elim H'1.
+generalize le_trans.
+intro H'4; red in H'4.
+intros x1 H'6; try assumption.
+apply H'4 with (y := x0); auto with sets arith.
+elim H'3; simpl in |- *; auto with sets arith.
+intros x1 H'4; elim H'4; auto with sets arith.
+exists x0.
+apply Upper_Bound_definition; auto with sets arith; simpl in |- *.
+intros y H'1; elim H'1.
+intros x1 H'4; try assumption.
+elim H'3; simpl in |- *; auto with sets arith.
+intros x1 H'4; elim H'4; auto with sets arith.
+red in |- *.
+intros x1 H'1; elim H'1; auto with sets arith.
+Qed.
+
+Lemma Integers_has_no_ub :
+ ~ (exists m : nat, Upper_Bound nat nat_po Integers m).
+Proof.
+red in |- *; intro H'; elim H'.
+intros x H'0.
+elim H'0; intros H'1 H'2.
+cut (In nat Integers (S x)).
+intro H'3.
+specialize 1H'2 with (y := S x); intro H'4; lapply H'4;
+ [ intro H'5; clear H'4 | try assumption; clear H'4 ].
+simpl in H'5.
+absurd (S x <= x); auto with arith.
+auto with sets arith.
+Qed.
+
+Lemma Integers_infinite : ~ Finite nat Integers.
+Proof.
+generalize Integers_has_no_ub.
+intro H'; red in |- *; intro H'0; try exact H'0.
+apply H'.
+apply Finite_subset_has_lub; auto with sets arith.
+Qed.
+
+End Integers_sect.
+
+
+
+
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
new file mode 100755
index 00000000..a308282b
--- /dev/null
+++ b/theories/Sets/Multiset.v
@@ -0,0 +1,191 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: Multiset.v,v 1.9.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
+
+(* G. Huet 1-9-95 *)
+
+Require Import Permut.
+
+Set Implicit Arguments.
+
+Section multiset_defs.
+
+Variable A : Set.
+Variable eqA : A -> A -> Prop.
+Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+
+Inductive multiset : Set :=
+ 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
+ | left _ => 1
+ | right _ => 0
+ 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.
+
+Hint Unfold meq multiplicity.
+
+Lemma meq_refl : forall x:multiset, meq x x.
+Proof.
+destruct x; auto.
+Qed.
+Hint Resolve meq_refl.
+
+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 |- *.
+destruct x; destruct y; auto.
+Qed.
+Hint Immediate meq_sym.
+
+(** multiset union *)
+Definition munion (m1 m2:multiset) :=
+ Bag (fun a:A => multiplicity m1 a + multiplicity m2 a).
+
+Lemma munion_empty_left : forall x:multiset, meq x (munion EmptyBag x).
+Proof.
+unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.
+Qed.
+Hint Resolve munion_empty_left.
+
+Lemma munion_empty_right : forall x:multiset, meq x (munion x EmptyBag).
+Proof.
+unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.
+Qed.
+
+
+Require Import 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 |- *.
+destruct x; destruct y; auto with arith.
+Qed.
+Hint Resolve munion_comm.
+
+Lemma munion_ass :
+ forall x y z:multiset, meq (munion (munion x y) z) (munion x (munion y z)).
+Proof.
+unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
+destruct x; destruct y; destruct z; auto with arith.
+Qed.
+Hint Resolve munion_ass.
+
+Lemma meq_left :
+ forall x y z:multiset, meq x y -> meq (munion x z) (munion y z).
+Proof.
+unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
+destruct x; destruct y; destruct z.
+intros; elim H; auto with arith.
+Qed.
+Hint Resolve meq_left.
+
+Lemma meq_right :
+ forall x y z:multiset, meq x y -> meq (munion z x) (munion z y).
+Proof.
+unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
+destruct x; destruct y; destruct z.
+intros; elim H; auto.
+Qed.
+Hint Resolve meq_right.
+
+
+(** Here we should make multiset an abstract datatype, by hiding [Bag],
+ [munion], [multiplicity]; all further properties are proved abstractly *)
+
+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); auto.
+exact meq_trans.
+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.
+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.
+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).
+Proof.
+intros; apply (twist multiset munion meq); auto.
+exact meq_trans.
+Qed.
+
+Lemma multiset_twist2 :
+ forall x y z t:multiset,
+ meq (munion x (munion (munion y z) t)) (munion (munion y (munion x z)) t).
+Proof.
+intros; apply meq_trans with (munion (munion x (munion y z)) t).
+apply meq_sym; apply munion_ass.
+apply meq_left; apply munion_perm_left.
+Qed.
+
+(** specific for treesort *)
+
+Lemma treesort_twist1 :
+ forall x y z t u:multiset,
+ meq u (munion y z) ->
+ meq (munion x (munion u t)) (munion (munion y (munion x t)) z).
+Proof.
+intros; apply meq_trans with (munion x (munion (munion y z) t)).
+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) ->
+ meq (munion x (munion u t)) (munion (munion y (munion x z)) t).
+Proof.
+intros; apply meq_trans with (munion x (munion (munion y z) t)).
+apply meq_right; apply meq_left; trivial.
+apply multiset_twist2.
+Qed.
+
+
+(*i theory of minter to do similarly
+Require Min.
+(* multiset intersection *)
+Definition minter := [m1,m2:multiset]
+ (Bag [a:A](min (multiplicity m1 a)(multiplicity m2 a))).
+i*)
+
+End multiset_defs.
+
+Unset Implicit Arguments.
+
+Hint Unfold meq multiplicity: v62 datatypes.
+Hint Resolve munion_empty_right munion_comm munion_ass meq_left meq_right
+ munion_empty_left: v62 datatypes.
+Hint Immediate meq_sym: v62 datatypes. \ No newline at end of file
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
new file mode 100755
index 00000000..b3e59886
--- /dev/null
+++ b/theories/Sets/Partial_Order.v
@@ -0,0 +1,100 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(****************************************************************************)
+(* *)
+(* Naive Set Theory in Coq *)
+(* *)
+(* INRIA INRIA *)
+(* Rocquencourt Sophia-Antipolis *)
+(* *)
+(* Coq V6.1 *)
+(* *)
+(* Gilles Kahn *)
+(* Gerard Huet *)
+(* *)
+(* *)
+(* *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
+(* to the Newton Institute for providing an exceptional work environment *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
+(****************************************************************************)
+
+(*i $Id: Partial_Order.v,v 1.6.2.1 2004/07/16 19:31:18 herbelin Exp $ 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 ->
+ ~ (exists z : _, Strict_Rel_of x z /\ Strict_Rel_of z y) ->
+ covers y x.
+
+End Partial_orders.
+
+Hint Unfold Carrier_of Rel_of Strict_Rel_of: sets v62.
+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.
+unfold Strict_Rel_of at 1 in |- *.
+red in |- *.
+elim D; simpl in |- *.
+intros C R H' H'0; elim H'0.
+intros H'1 H'2 H'3 x y z H'4 H'5; split.
+apply H'2 with (y := y); tauto.
+red in |- *; intro H'6.
+elim H'4; intros H'7 H'8; apply H'8; clear H'4.
+apply H'3; auto.
+rewrite H'6; tauto.
+Qed.
+
+Lemma Strict_Rel_Transitive_with_Rel_left :
+ forall x y z:U,
+ Rel_of U D x y -> Strict_Rel_of U D y z -> Strict_Rel_of U D x z.
+unfold Strict_Rel_of at 1 in |- *.
+red in |- *.
+elim D; simpl in |- *.
+intros C R H' H'0; elim H'0.
+intros H'1 H'2 H'3 x y z H'4 H'5; split.
+apply H'2 with (y := y); tauto.
+red in |- *; intro H'6.
+elim H'5; intros H'7 H'8; apply H'8; clear H'5.
+apply H'3; auto.
+rewrite <- H'6; auto.
+Qed.
+
+Lemma Strict_Rel_Transitive : Transitive U (Strict_Rel_of U D).
+red in |- *.
+intros x y z H' H'0.
+apply Strict_Rel_Transitive_with_Rel with (y := y);
+ [ intuition | unfold Strict_Rel_of in H', H'0; intuition ].
+Qed.
+End Partial_order_facts. \ No newline at end of file
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v
new file mode 100755
index 00000000..af6151bf
--- /dev/null
+++ b/theories/Sets/Permut.v
@@ -0,0 +1,91 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: Permut.v,v 1.6.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+
+(* G. Huet 1-9-95 *)
+
+(** We consider a Set [U], given with a commutative-associative operator [op],
+ and a congruence [cong]; we show permutation lemmas *)
+
+Section Axiomatisation.
+
+Variable U : Set.
+
+Variable op : U -> U -> U.
+
+Variable cong : U -> U -> Prop.
+
+Hypothesis op_comm : forall x y:U, cong (op x y) (op y x).
+Hypothesis op_ass : forall x y z:U, cong (op (op x y) z) (op x (op y z)).
+
+Hypothesis cong_left : forall x y z:U, cong x y -> cong (op x z) (op y z).
+Hypothesis cong_right : forall x y z:U, cong x y -> cong (op z x) (op z y).
+Hypothesis cong_trans : forall x y z:U, cong x y -> cong y z -> cong x z.
+Hypothesis cong_sym : forall x y:U, cong x y -> cong y x.
+
+(** Remark. we do not need: [Hypothesis cong_refl : (x:U)(cong x x)]. *)
+
+Lemma cong_congr :
+ forall x y z t:U, cong x y -> cong z t -> cong (op x z) (op y t).
+Proof.
+intros; apply cong_trans with (op y z).
+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_right; apply op_comm.
+apply cong_sym; apply op_ass.
+Qed.
+
+Lemma perm_left : forall x y z:U, cong (op x (op y z)) (op y (op x z)).
+Proof.
+intros.
+apply cong_trans with (op (op x y) z).
+apply cong_sym; apply op_ass.
+apply cong_trans with (op (op y x) z).
+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).
+apply cong_sym; apply op_ass.
+apply op_comm.
+Qed.
+
+(* Needed for treesort ... *)
+Lemma twist :
+ forall x y z t:U, cong (op x (op (op y z) t)) (op (op y (op x t)) z).
+Proof.
+intros.
+apply cong_trans with (op x (op (op y t) z)).
+apply cong_right; apply perm_right.
+apply cong_trans with (op (op x (op y t)) z).
+apply cong_sym; apply op_ass.
+apply cong_left; apply perm_left.
+Qed.
+
+End Axiomatisation. \ No newline at end of file
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
new file mode 100755
index 00000000..a7f5e9f4
--- /dev/null
+++ b/theories/Sets/Powerset.v
@@ -0,0 +1,190 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(****************************************************************************)
+(* *)
+(* Naive Set Theory in Coq *)
+(* *)
+(* INRIA INRIA *)
+(* Rocquencourt Sophia-Antipolis *)
+(* *)
+(* Coq V6.1 *)
+(* *)
+(* Gilles Kahn *)
+(* Gerard Huet *)
+(* *)
+(* *)
+(* *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
+(* to the Newton Institute for providing an exceptional work environment *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
+(****************************************************************************)
+
+(*i $Id: Powerset.v,v 1.5.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+
+Require Export Ensembles.
+Require Export Relations_1.
+Require Export Relations_1_facts.
+Require Export Partial_Order.
+Require Export Cpo.
+
+Section The_power_set_partial_order.
+Variable U : Type.
+
+Inductive Power_set (A:Ensemble U) : Ensemble (Ensemble U) :=
+ Definition_of_Power_set :
+ forall X:Ensemble U, Included U X A -> In (Ensemble U) (Power_set A) X.
+Hint Resolve Definition_of_Power_set.
+
+Theorem Empty_set_minimal : forall X:Ensemble U, Included U (Empty_set U) X.
+intro X; red in |- *.
+intros x H'; elim H'.
+Qed.
+Hint Resolve Empty_set_minimal.
+
+Theorem Power_set_Inhabited :
+ forall X:Ensemble U, Inhabited (Ensemble U) (Power_set X).
+intro X.
+apply Inhabited_intro with (Empty_set U); auto with sets.
+Qed.
+Hint Resolve Power_set_Inhabited.
+
+Theorem Inclusion_is_an_order : Order (Ensemble U) (Included U).
+auto 6 with sets.
+Qed.
+Hint Resolve Inclusion_is_an_order.
+
+Theorem Inclusion_is_transitive : Transitive (Ensemble U) (Included U).
+elim Inclusion_is_an_order; auto with sets.
+Qed.
+Hint Resolve Inclusion_is_transitive.
+
+Definition Power_set_PO : Ensemble U -> PO (Ensemble U).
+intro A; try assumption.
+apply Definition_of_PO with (Power_set A) (Included U); auto with sets.
+Defined.
+Hint Unfold Power_set_PO.
+
+Theorem Strict_Rel_is_Strict_Included :
+ same_relation (Ensemble U) (Strict_Included U)
+ (Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))).
+auto with sets.
+Qed.
+Hint Resolve Strict_Rel_Transitive Strict_Rel_is_Strict_Included.
+
+Lemma Strict_inclusion_is_transitive_with_inclusion :
+ forall x y z:Ensemble U,
+ Strict_Included U x y -> Included U y z -> Strict_Included U x z.
+intros x y z H' H'0; try assumption.
+elim Strict_Rel_is_Strict_Included.
+unfold contains in |- *.
+intros H'1 H'2; try assumption.
+apply H'1.
+apply Strict_Rel_Transitive_with_Rel with (y := y); auto with sets.
+Qed.
+
+Lemma Strict_inclusion_is_transitive_with_inclusion_left :
+ forall x y z:Ensemble U,
+ Included U x y -> Strict_Included U y z -> Strict_Included U x z.
+intros x y z H' H'0; try assumption.
+elim Strict_Rel_is_Strict_Included.
+unfold contains in |- *.
+intros H'1 H'2; try assumption.
+apply H'1.
+apply Strict_Rel_Transitive_with_Rel_left with (y := y); auto with sets.
+Qed.
+
+Lemma Strict_inclusion_is_transitive :
+ Transitive (Ensemble U) (Strict_Included U).
+apply cong_transitive_same_relation with
+ (R := Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U)));
+ auto with sets.
+Qed.
+
+Theorem Empty_set_is_Bottom :
+ forall A:Ensemble U, Bottom (Ensemble U) (Power_set_PO A) (Empty_set U).
+intro A; apply Bottom_definition; simpl in |- *; auto with sets.
+Qed.
+Hint Resolve Empty_set_is_Bottom.
+
+Theorem Union_minimal :
+ forall a b X:Ensemble U,
+ Included U a X -> Included U b X -> Included U (Union U a b) X.
+intros a b X H' H'0; red in |- *.
+intros x H'1; elim H'1; auto with sets.
+Qed.
+Hint Resolve Union_minimal.
+
+Theorem Intersection_maximal :
+ forall a b X:Ensemble U,
+ Included U X a -> Included U X b -> Included U X (Intersection U a b).
+auto with sets.
+Qed.
+
+Theorem Union_increases_l : forall a b:Ensemble U, Included U a (Union U a b).
+auto with sets.
+Qed.
+
+Theorem Union_increases_r : forall a b:Ensemble U, Included U b (Union U a b).
+auto with sets.
+Qed.
+
+Theorem Intersection_decreases_l :
+ forall a b:Ensemble U, Included U (Intersection U a b) a.
+intros a b; red in |- *.
+intros x H'; elim H'; auto with sets.
+Qed.
+
+Theorem Intersection_decreases_r :
+ forall a b:Ensemble U, Included U (Intersection U a b) b.
+intros a b; red in |- *.
+intros x H'; elim H'; auto with sets.
+Qed.
+Hint Resolve Union_increases_l Union_increases_r Intersection_decreases_l
+ Intersection_decreases_r.
+
+Theorem Union_is_Lub :
+ forall A a b:Ensemble U,
+ Included U a A ->
+ Included U b A ->
+ Lub (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b) (Union U a b).
+intros A a b H' H'0.
+apply Lub_definition; simpl in |- *.
+apply Upper_Bound_definition; simpl in |- *; auto with sets.
+intros y H'1; elim H'1; auto with sets.
+intros y H'1; elim H'1; simpl in |- *; auto with sets.
+Qed.
+
+Theorem Intersection_is_Glb :
+ forall A a b:Ensemble U,
+ Included U a A ->
+ Included U b A ->
+ Glb (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b)
+ (Intersection U a b).
+intros A a b H' H'0.
+apply Glb_definition; simpl in |- *.
+apply Lower_Bound_definition; simpl in |- *; auto with sets.
+apply Definition_of_Power_set.
+generalize Inclusion_is_transitive; intro IT; red in IT; apply IT with a;
+ auto with sets.
+intros y H'1; elim H'1; auto with sets.
+intros y H'1; elim H'1; simpl in |- *; auto with sets.
+Qed.
+
+End The_power_set_partial_order.
+
+Hint Resolve Empty_set_minimal: sets v62.
+Hint Resolve Power_set_Inhabited: sets v62.
+Hint Resolve Inclusion_is_an_order: sets v62.
+Hint Resolve Inclusion_is_transitive: sets v62.
+Hint Resolve Union_minimal: sets v62.
+Hint Resolve Union_increases_l: sets v62.
+Hint Resolve Union_increases_r: sets v62.
+Hint Resolve Intersection_decreases_l: sets v62.
+Hint Resolve Intersection_decreases_r: sets v62.
+Hint Resolve Empty_set_is_Bottom: sets v62.
+Hint Resolve Strict_inclusion_is_transitive: sets v62. \ No newline at end of file
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
new file mode 100755
index 00000000..05c60def
--- /dev/null
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -0,0 +1,342 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(****************************************************************************)
+(* *)
+(* Naive Set Theory in Coq *)
+(* *)
+(* INRIA INRIA *)
+(* Rocquencourt Sophia-Antipolis *)
+(* *)
+(* Coq V6.1 *)
+(* *)
+(* Gilles Kahn *)
+(* Gerard Huet *)
+(* *)
+(* *)
+(* *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
+(* to the Newton Institute for providing an exceptional work environment *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
+(****************************************************************************)
+
+(*i $Id: Powerset_Classical_facts.v,v 1.5.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+
+Require Export Ensembles.
+Require Export Constructive_sets.
+Require Export Relations_1.
+Require Export Relations_1_facts.
+Require Export Partial_Order.
+Require Export Cpo.
+Require Export Powerset.
+Require Export Powerset_facts.
+Require Export Classical_Type.
+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 ->
+ Strict_Included U (Add U A x) (Add U B x) -> Strict_Included U A B.
+Proof.
+intros A B x H' H'0; red in |- *.
+lapply (Strict_Included_inv U (Add U A x) (Add U B x)); auto with sets.
+clear H'0; intro H'0; split.
+apply incl_add_x with (x := x); tauto.
+elim H'0; intros H'1 H'2; elim H'2; clear H'0 H'2.
+intros x0 H'0.
+red in |- *; intro H'2.
+elim H'0; clear H'0.
+rewrite <- H'2; auto with sets.
+Qed.
+
+Lemma incl_soustr_in :
+ forall (X:Ensemble U) (x:U), In U X x -> Included U (Subtract U X x) X.
+Proof.
+intros X x H'; red in |- *.
+intros x0 H'0; elim H'0; auto with sets.
+Qed.
+Hint Resolve incl_soustr_in: sets v62.
+
+Lemma incl_soustr :
+ forall (X Y:Ensemble U) (x:U),
+ Included U X Y -> Included U (Subtract U X x) (Subtract U Y x).
+Proof.
+intros X Y x H'; red in |- *.
+intros x0 H'0; elim H'0.
+intros H'1 H'2.
+apply Subtract_intro; auto with sets.
+Qed.
+Hint Resolve incl_soustr: sets v62.
+
+
+Lemma incl_soustr_add_l :
+ forall (X:Ensemble U) (x:U), Included U (Subtract U (Add U X x) x) X.
+Proof.
+intros X x; red in |- *.
+intros x0 H'; elim H'; auto with sets.
+intro H'0; elim H'0; auto with sets.
+intros t H'1 H'2; elim H'2; auto with sets.
+Qed.
+Hint Resolve incl_soustr_add_l: sets v62.
+
+Lemma incl_soustr_add_r :
+ forall (X:Ensemble U) (x:U),
+ ~ In U X x -> Included U X (Subtract U (Add U X x) x).
+Proof.
+intros X x H'; red in |- *.
+intros x0 H'0; try assumption.
+apply Subtract_intro; auto with sets.
+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).
+Proof.
+intros X x H'; red in |- *.
+intros x0 H'0; try assumption.
+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.
+Proof.
+intros X x H'; red in |- *.
+intros x0 H'0; elim H'0; auto with sets.
+intros y H'1; elim H'1; auto with sets.
+intros t H'1; try assumption.
+rewrite <- (Singleton_inv U x t); auto with sets.
+Qed.
+Hint Resolve add_soustr_1 add_soustr_2: sets v62.
+
+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.
+Proof.
+intros X x y H'; apply Extensionality_Ensembles.
+split; red in |- *.
+intros x0 H'0; elim H'0; auto with sets.
+intro H'1; elim H'1.
+intros u H'2 H'3; try assumption.
+apply Add_intro1.
+apply Subtract_intro; auto with sets.
+intros t H'2 H'3; try assumption.
+elim (Singleton_inv U x t); auto with sets.
+intros u H'2; try assumption.
+elim (Add_inv U (Subtract U X y) x u); auto with sets.
+intro H'0; elim H'0; auto with sets.
+intro H'0; rewrite <- H'0; auto with sets.
+Qed.
+Hint Resolve add_soustr_xy: sets v62.
+
+Lemma incl_st_add_soustr :
+ forall (X Y:Ensemble U) (x:U),
+ ~ In U X x ->
+ Strict_Included U (Add U X x) Y -> Strict_Included U X (Subtract U Y x).
+Proof.
+intros X Y x H' H'0; apply sincl_add_x with (x := x); auto with sets.
+split.
+elim H'0.
+intros H'1 H'2.
+generalize (Inclusion_is_transitive U).
+intro H'4; red in H'4.
+apply H'4 with (y := Y); auto with sets.
+red in H'0.
+elim H'0; intros H'1 H'2; try exact H'1; clear H'0. (* PB *)
+red in |- *; intro H'0; apply H'2.
+rewrite H'0; auto 8 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 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.
+Proof.
+intros X X0 x H' H'0 H'1; try assumption.
+rewrite (Sub_Add_new X x); auto with sets.
+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) ->
+ Included U X A \/ (exists A' : _, X = Add U A' x /\ Included U A' A).
+Proof.
+intros X A x H'0; try assumption.
+elim (classic (In U X x)).
+intro H'1; right; try assumption.
+exists (Subtract U X x).
+split; auto with sets.
+red in H'0.
+red in |- *.
+intros x0 H'2; try assumption.
+lapply (Subtract_inv U X x x0); auto with sets.
+intro H'3; elim H'3; intros K K'; clear H'3.
+lapply (H'0 x0); auto with sets.
+intro H'3; try assumption.
+lapply (Add_inv U A x x0); auto with sets.
+intro H'4; elim H'4;
+ [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ].
+elim K'; auto with sets.
+intro H'1; left; try assumption.
+red in H'0.
+red in |- *.
+intros x0 H'2; try assumption.
+lapply (H'0 x0); auto with sets.
+intro H'3; try assumption.
+lapply (Add_inv U A x x0); auto with sets.
+intro H'4; elim H'4;
+ [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ].
+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 ->
+ Strict_Included U x y /\
+ (forall z:Ensemble U, Included U x z -> Included U z y -> x = z \/ z = y).
+Proof.
+intros A x y H'; elim H'.
+unfold Strict_Rel_of in |- *; simpl in |- *.
+intros H'0 H'1; split; [ auto with sets | idtac ].
+intros z H'2 H'3; try assumption.
+elim (classic (x = z)); auto with sets.
+intro H'4; right; try assumption.
+elim (classic (z = y)); auto with sets.
+intro H'5; try assumption.
+elim H'1.
+exists z; auto with sets.
+Qed.
+
+Theorem Add_covers :
+ forall A a:Ensemble U,
+ Included U a A ->
+ forall x:U,
+ In U A x ->
+ ~ In U a x -> covers (Ensemble U) (Power_set_PO U A) (Add U a x) a.
+Proof.
+intros A a H' x H'0 H'1; try assumption.
+apply setcover_intro; auto with sets.
+red in |- *.
+split; [ idtac | red in |- *; intro H'2; try exact H'2 ]; auto with sets.
+apply H'1.
+rewrite H'2; auto with sets.
+red in |- *; intro H'2; elim H'2; clear H'2.
+intros z H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.
+lapply (Strict_Included_inv U a z); auto with sets; clear H'3.
+intro H'2; elim H'2; intros H'3 H'5; elim H'5; clear H'2 H'5.
+intros x0 H'2; elim H'2.
+intros H'5 H'6; try assumption.
+generalize H'4; intro K.
+red in H'4.
+elim H'4; intros H'8 H'9; red in H'8; clear H'4.
+lapply (H'8 x0); auto with sets.
+intro H'7; try assumption.
+elim (Add_inv U a x x0); auto with sets.
+intro H'15.
+cut (Included U (Add U a x) z).
+intro H'10; try assumption.
+red in K.
+elim K; intros H'11 H'12; apply H'12; clear K; auto with sets.
+rewrite H'15.
+red in |- *.
+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 ->
+ Included U a' A ->
+ covers (Ensemble U) (Power_set_PO U A) a' a ->
+ exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x.
+Proof.
+intros A a a' H' H'0 H'1; try assumption.
+elim (setcover_inv A a a'); auto with sets.
+intros H'6 H'7.
+clear H'1.
+elim (Strict_Included_inv U a a'); auto with sets.
+intros H'5 H'8; elim H'8.
+intros x H'1; elim H'1.
+intros H'2 H'3; try assumption.
+exists x.
+split; [ try assumption | idtac ].
+clear H'8 H'1.
+elim (H'7 (Add U a x)); auto with sets.
+intro H'1.
+absurd (a = Add U a x); auto with sets.
+red in |- *; intro H'8; try exact H'8.
+apply H'3.
+rewrite H'8; auto with sets.
+auto with sets.
+red in |- *.
+intros x0 H'1; elim H'1; auto with sets.
+intros x1 H'8; elim H'8; auto with sets.
+split; [ idtac | try assumption ].
+red in H'0; auto with sets.
+Qed.
+
+Theorem covers_is_Add :
+ forall A a a':Ensemble U,
+ Included U a A ->
+ Included U a' A ->
+ (covers (Ensemble U) (Power_set_PO U A) a' a <->
+ (exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x)).
+Proof.
+intros A a a' H' H'0; split; intro K.
+apply covers_Add with (A := A); auto with sets.
+elim K.
+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 ->
+ covers (Ensemble U) (Power_set_PO U A) (Singleton U x) (Empty_set U).
+intros x A H'.
+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.
+intros X x H'; try assumption.
+red in H'.
+lapply (Singleton_atomic x (Full_set U));
+ [ intro H'2; try exact H'2 | apply Full_intro ].
+elim H'; intros H'0 H'1; try exact H'1; clear H'.
+elim (setcover_inv (Full_set U) (Empty_set U) (Singleton U x));
+ [ intros H'6 H'7; try exact H'7 | idtac ]; auto with sets.
+elim (H'7 X); [ intro H'5; try exact H'5 | intro H'5 | idtac | idtac ];
+ auto with sets.
+elim H'1; auto with sets.
+Qed.
+
+End Sets_as_an_algebra.
+
+Hint Resolve incl_soustr_in: sets v62.
+Hint Resolve incl_soustr: sets v62.
+Hint Resolve incl_soustr_add_l: sets v62.
+Hint Resolve incl_soustr_add_r: sets v62.
+Hint Resolve add_soustr_1 add_soustr_2: sets v62.
+Hint Resolve add_soustr_xy: sets v62. \ No newline at end of file
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
new file mode 100755
index 00000000..2c71f529
--- /dev/null
+++ b/theories/Sets/Powerset_facts.v
@@ -0,0 +1,268 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(****************************************************************************)
+(* *)
+(* Naive Set Theory in Coq *)
+(* *)
+(* INRIA INRIA *)
+(* Rocquencourt Sophia-Antipolis *)
+(* *)
+(* Coq V6.1 *)
+(* *)
+(* Gilles Kahn *)
+(* Gerard Huet *)
+(* *)
+(* *)
+(* *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
+(* to the Newton Institute for providing an exceptional work environment *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
+(****************************************************************************)
+
+(*i $Id: Powerset_facts.v,v 1.8.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+
+Require Export Ensembles.
+Require Export Constructive_sets.
+Require Export Relations_1.
+Require Export Relations_1_facts.
+Require Export Partial_Order.
+Require Export Cpo.
+Require Export Powerset.
+
+Section Sets_as_an_algebra.
+Variable U : Type.
+Hint Unfold not.
+
+Theorem Empty_set_zero : forall X:Ensemble U, Union U (Empty_set U) X = X.
+Proof.
+auto 6 with sets.
+Qed.
+Hint Resolve Empty_set_zero.
+
+Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x.
+Proof.
+unfold Add at 1 in |- *; auto with sets.
+Qed.
+Hint Resolve Empty_set_zero'.
+
+Lemma less_than_empty :
+ forall X:Ensemble U, Included U X (Empty_set U) -> X = Empty_set U.
+Proof.
+auto with sets.
+Qed.
+Hint Resolve less_than_empty.
+
+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.
+Hint Resolve Union_associative.
+
+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.
+auto 7 with sets.
+Qed.
+
+Theorem Couple_as_union :
+ forall x y:U, Union U (Singleton U x) (Singleton U y) = Couple U x y.
+Proof.
+intros x y; apply Extensionality_Ensembles; split; red in |- *.
+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) =
+ Triple U x y z.
+Proof.
+intros x y z; apply Extensionality_Ensembles; split; red in |- *.
+intros x0 H'; elim H'.
+intros x1 H'0; elim H'0; (intros x2 H'1; elim H'1; auto with sets).
+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.
+rewrite <- (Couple_as_union x y).
+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.
+intros x y z.
+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.
+intros A B.
+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) =
+ Union U (Intersection U A B) (Intersection U A C).
+Proof.
+intros A B C.
+apply Extensionality_Ensembles.
+split; red in |- *; intros x H'.
+elim H'.
+intros x0 H'0 H'1; generalize H'0.
+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) =
+ Intersection U (Union U A B) (Union U A C).
+Proof.
+intros A B C.
+apply Extensionality_Ensembles.
+split; red in |- *; intros x H'.
+elim H'; auto with sets.
+intros x0 H'0; elim H'0; auto with sets.
+elim H'.
+intros x0 H'0; elim H'0; auto with sets.
+intros x1 H'1 H'2; try exact H'2.
+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 with sets.
+Qed.
+Hint Resolve Union_add.
+
+Theorem Non_disjoint_union :
+ forall (X:Ensemble U) (x:U), In U X x -> Add U X x = X.
+intros X x H'; unfold Add in |- *.
+apply Extensionality_Ensembles; red in |- *.
+split; red in |- *; auto with sets.
+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.
+intros X x H'; unfold Subtract in |- *.
+apply Extensionality_Ensembles.
+split; red in |- *; auto with sets.
+intros x0 H'0; elim H'0; auto with sets.
+intros x0 H'0; apply Setminus_intro; auto with sets.
+red in |- *; intro H'1; elim H'1.
+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.
+Hint Resolve singlx.
+
+Lemma incl_add :
+ forall (A B:Ensemble U) (x:U),
+ Included U A B -> Included U (Add U A x) (Add U B x).
+Proof.
+intros A B x H'; red in |- *; auto with sets.
+intros x0 H'0.
+lapply (Add_inv U A x x0); auto with sets.
+intro H'1; elim H'1;
+ [ intro H'2; clear H'1 | intro H'2; rewrite <- H'2; clear H'1 ];
+ auto with sets.
+Qed.
+Hint Resolve incl_add.
+
+Lemma incl_add_x :
+ forall (A B:Ensemble U) (x:U),
+ ~ In U A x -> Included U (Add U A x) (Add U B x) -> Included U A B.
+Proof.
+unfold Included in |- *.
+intros A B x H' H'0 x0 H'1.
+lapply (H'0 x0); auto with sets.
+intro H'2; lapply (Add_inv U B x x0); auto with sets.
+intro H'3; elim H'3;
+ [ intro H'4; try exact H'4; clear H'3 | intro H'4; clear H'3 ].
+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.
+intros A x y.
+unfold Add in |- *.
+rewrite (Union_associative A (Singleton U x) (Singleton U y)).
+rewrite (Union_commutative (Singleton U x) (Singleton U y)).
+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.
+Proof.
+intros A x y z.
+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).
+Proof.
+intros A B x y H'; try assumption.
+rewrite <- (Union_add (Add U A x) B y).
+unfold Add at 4 in |- *.
+rewrite (Union_commutative A (Singleton U x)).
+rewrite Union_associative.
+rewrite (Union_absorbs A B H').
+rewrite (Union_commutative (Singleton U x) A).
+auto with sets.
+Qed.
+
+Lemma setcover_intro :
+ forall (U:Type) (A x y:Ensemble U),
+ Strict_Included U x y ->
+ ~ (exists z : _, Strict_Included U x z /\ Strict_Included U z y) ->
+ covers (Ensemble U) (Power_set_PO U A) y x.
+Proof.
+intros; apply Definition_of_covers; auto with sets.
+Qed.
+Hint Resolve setcover_intro.
+
+End Sets_as_an_algebra.
+
+Hint Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add
+ singlx incl_add: sets v62.
+
diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v
new file mode 100755
index 00000000..e33746a9
--- /dev/null
+++ b/theories/Sets/Relations_1.v
@@ -0,0 +1,67 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(****************************************************************************)
+(* *)
+(* Naive Set Theory in Coq *)
+(* *)
+(* INRIA INRIA *)
+(* Rocquencourt Sophia-Antipolis *)
+(* *)
+(* Coq V6.1 *)
+(* *)
+(* Gilles Kahn *)
+(* Gerard Huet *)
+(* *)
+(* *)
+(* *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
+(* to the Newton Institute for providing an exceptional work environment *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
+(****************************************************************************)
+
+(*i $Id: Relations_1.v,v 1.4.2.1 2004/07/16 19:31:18 herbelin Exp $ 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.
+Hint Resolve Definition_of_preorder Definition_of_order
+ Definition_of_equivalence Definition_of_PER: sets v62. \ No newline at end of file
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
new file mode 100755
index 00000000..62688895
--- /dev/null
+++ b/theories/Sets/Relations_1_facts.v
@@ -0,0 +1,112 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(****************************************************************************)
+(* *)
+(* Naive Set Theory in Coq *)
+(* *)
+(* INRIA INRIA *)
+(* Rocquencourt Sophia-Antipolis *)
+(* *)
+(* Coq V6.1 *)
+(* *)
+(* Gilles Kahn *)
+(* Gerard Huet *)
+(* *)
+(* *)
+(* *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
+(* to the Newton Institute for providing an exceptional work environment *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
+(****************************************************************************)
+
+(*i $Id: Relations_1_facts.v,v 1.7.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+
+Require Export Relations_1.
+
+Definition Complement (U:Type) (R:Relation U) : Relation U :=
+ fun x y:U => ~ R x y.
+
+Theorem Rsym_imp_notRsym :
+ forall (U:Type) (R:Relation U),
+ Symmetric U R -> Symmetric U (Complement U R).
+Proof.
+unfold Symmetric, Complement in |- *.
+intros U R H' x y H'0; red in |- *; intro H'1; apply H'0; auto with sets.
+Qed.
+
+Theorem Equiv_from_preorder :
+ forall (U:Type) (R:Relation U),
+ Preorder U R -> Equivalence U (fun x y:U => R x y /\ R y x).
+Proof.
+intros U R H'; elim H'; intros H'0 H'1.
+apply Definition_of_equivalence.
+red in H'0; auto 10 with sets.
+2: red in |- *; intros x y h; elim h; intros H'3 H'4; auto 10 with sets.
+red in H'1; red in |- *; auto 10 with sets.
+intros x y z h; elim h; intros H'3 H'4; clear h.
+intro h; elim h; intros H'5 H'6; clear h.
+split; apply H'1 with y; auto 10 with sets.
+Qed.
+Hint Resolve Equiv_from_preorder.
+
+Theorem Equiv_from_order :
+ forall (U:Type) (R:Relation U),
+ Order U R -> Equivalence U (fun x y:U => R x y /\ R y x).
+Proof.
+intros U R H'; elim H'; auto 10 with sets.
+Qed.
+Hint Resolve Equiv_from_order.
+
+Theorem contains_is_preorder :
+ forall U:Type, Preorder (Relation U) (contains U).
+Proof.
+auto 10 with sets.
+Qed.
+Hint Resolve contains_is_preorder.
+
+Theorem same_relation_is_equivalence :
+ forall U:Type, Equivalence (Relation U) (same_relation U).
+Proof.
+unfold same_relation at 1 in |- *; auto 10 with sets.
+Qed.
+Hint Resolve same_relation_is_equivalence.
+
+Theorem cong_reflexive_same_relation :
+ forall (U:Type) (R R':Relation U),
+ same_relation U R R' -> Reflexive U R -> Reflexive U R'.
+Proof.
+unfold same_relation in |- *; intuition.
+Qed.
+
+Theorem cong_symmetric_same_relation :
+ forall (U:Type) (R R':Relation U),
+ same_relation U R R' -> Symmetric U R -> Symmetric U R'.
+Proof.
+ compute in |- *; intros; elim H; intros; clear H;
+ apply (H3 y x (H0 x y (H2 x y H1))).
+(*Intuition.*)
+Qed.
+
+Theorem cong_antisymmetric_same_relation :
+ forall (U:Type) (R R':Relation U),
+ same_relation U R R' -> Antisymmetric U R -> Antisymmetric U R'.
+Proof.
+ compute in |- *; intros; elim H; intros; clear H;
+ apply (H0 x y (H3 x y H1) (H3 y x H2)).
+(*Intuition.*)
+Qed.
+
+Theorem cong_transitive_same_relation :
+ forall (U:Type) (R R':Relation U),
+ same_relation U R R' -> Transitive U R -> Transitive U R'.
+Proof.
+intros U R R' H' H'0; red in |- *.
+elim H'.
+intros H'1 H'2 x y z H'3 H'4; apply H'2.
+apply H'0 with y; auto with sets.
+Qed. \ No newline at end of file
diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v
new file mode 100755
index 00000000..15d3ee2d
--- /dev/null
+++ b/theories/Sets/Relations_2.v
@@ -0,0 +1,56 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(****************************************************************************)
+(* *)
+(* Naive Set Theory in Coq *)
+(* *)
+(* INRIA INRIA *)
+(* Rocquencourt Sophia-Antipolis *)
+(* *)
+(* Coq V6.1 *)
+(* *)
+(* Gilles Kahn *)
+(* Gerard Huet *)
+(* *)
+(* *)
+(* *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
+(* to the Newton Institute for providing an exceptional work environment *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
+(****************************************************************************)
+
+(*i $Id: Relations_2.v,v 1.4.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+
+Require Export Relations_1.
+
+Section Relations_2.
+Variable U : Type.
+Variable R : Relation U.
+
+Inductive Rstar : Relation U :=
+ | Rstar_0 : forall x:U, Rstar x x
+ | Rstar_n : forall x y z:U, R x y -> Rstar y z -> Rstar x z.
+
+Inductive Rstar1 : Relation U :=
+ | Rstar1_0 : forall x:U, Rstar1 x x
+ | Rstar1_1 : forall x y:U, R x y -> Rstar1 x y
+ | Rstar1_n : forall x y z:U, Rstar1 x y -> Rstar1 y z -> Rstar1 x z.
+
+Inductive Rplus : Relation U :=
+ | Rplus_0 : forall x y:U, R x y -> Rplus x y
+ | Rplus_n : forall x y z:U, R x y -> Rplus y z -> Rplus x z.
+
+Definition Strongly_confluent : Prop :=
+ forall x a b:U, R x a -> R x b -> ex (fun z:U => R a z /\ R b z).
+
+End Relations_2.
+
+Hint Resolve Rstar_0: sets v62.
+Hint Resolve Rstar1_0: sets v62.
+Hint Resolve Rstar1_1: sets v62.
+Hint Resolve Rplus_0: sets v62. \ No newline at end of file
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
new file mode 100755
index 00000000..4c729fe7
--- /dev/null
+++ b/theories/Sets/Relations_2_facts.v
@@ -0,0 +1,153 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(****************************************************************************)
+(* *)
+(* Naive Set Theory in Coq *)
+(* *)
+(* INRIA INRIA *)
+(* Rocquencourt Sophia-Antipolis *)
+(* *)
+(* Coq V6.1 *)
+(* *)
+(* Gilles Kahn *)
+(* Gerard Huet *)
+(* *)
+(* *)
+(* *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
+(* to the Newton Institute for providing an exceptional work environment *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
+(****************************************************************************)
+
+(*i $Id: Relations_2_facts.v,v 1.6.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+
+Require Export Relations_1.
+Require Export Relations_1_facts.
+Require Export Relations_2.
+
+Theorem Rstar_reflexive :
+ forall (U:Type) (R:Relation U), Reflexive U (Rstar U R).
+Proof.
+auto with sets.
+Qed.
+
+Theorem Rplus_contains_R :
+ forall (U:Type) (R:Relation U), contains U (Rplus U R) R.
+Proof.
+auto with sets.
+Qed.
+
+Theorem Rstar_contains_R :
+ forall (U:Type) (R:Relation U), contains U (Rstar U R) R.
+Proof.
+intros U R; red in |- *; intros x y H'; apply Rstar_n with y; auto with sets.
+Qed.
+
+Theorem Rstar_contains_Rplus :
+ forall (U:Type) (R:Relation U), contains U (Rstar U R) (Rplus U R).
+Proof.
+intros U R; red in |- *.
+intros x y H'; elim H'.
+generalize Rstar_contains_R; intro T; red in T; auto with sets.
+intros x0 y0 z H'0 H'1 H'2; apply Rstar_n with y0; auto with sets.
+Qed.
+
+Theorem Rstar_transitive :
+ forall (U:Type) (R:Relation U), Transitive U (Rstar U R).
+Proof.
+intros U R; red in |- *.
+intros x y z H'; elim H'; auto with sets.
+intros x0 y0 z0 H'0 H'1 H'2 H'3; apply Rstar_n with y0; auto with sets.
+Qed.
+
+Theorem Rstar_cases :
+ forall (U:Type) (R:Relation U) (x y:U),
+ Rstar U R x y -> x = y \/ (exists u : _, R x u /\ Rstar U R u y).
+Proof.
+intros U R x y H'; elim H'; auto with sets.
+intros x0 y0 z H'0 H'1 H'2; right; exists y0; auto with sets.
+Qed.
+
+Theorem Rstar_equiv_Rstar1 :
+ forall (U:Type) (R:Relation U), same_relation U (Rstar U R) (Rstar1 U R).
+Proof.
+generalize Rstar_contains_R; intro T; red in T.
+intros U R; unfold same_relation, contains in |- *.
+split; intros x y H'; elim H'; auto with sets.
+generalize Rstar_transitive; intro T1; red in T1.
+intros x0 y0 z H'0 H'1 H'2 H'3; apply T1 with y0; auto with sets.
+intros x0 y0 z H'0 H'1 H'2; apply Rstar1_n with y0; auto with sets.
+Qed.
+
+Theorem Rsym_imp_Rstarsym :
+ forall (U:Type) (R:Relation U), Symmetric U R -> Symmetric U (Rstar U R).
+Proof.
+intros U R H'; red in |- *.
+intros x y H'0; elim H'0; auto with sets.
+intros x0 y0 z H'1 H'2 H'3.
+generalize Rstar_transitive; intro T1; red in T1.
+apply T1 with y0; auto with sets.
+apply Rstar_n with x0; auto with sets.
+Qed.
+
+Theorem Sstar_contains_Rstar :
+ forall (U:Type) (R S:Relation U),
+ contains U (Rstar U S) R -> contains U (Rstar U S) (Rstar U R).
+Proof.
+unfold contains in |- *.
+intros U R S H' x y H'0; elim H'0; auto with sets.
+generalize Rstar_transitive; intro T1; red in T1.
+intros x0 y0 z H'1 H'2 H'3; apply T1 with y0; auto with sets.
+Qed.
+
+Theorem star_monotone :
+ forall (U:Type) (R S:Relation U),
+ contains U S R -> contains U (Rstar U S) (Rstar U R).
+Proof.
+intros U R S H'.
+apply Sstar_contains_Rstar; auto with sets.
+generalize (Rstar_contains_R U S); auto with sets.
+Qed.
+
+Theorem RstarRplus_RRstar :
+ forall (U:Type) (R:Relation U) (x y z:U),
+ Rstar U R x y -> Rplus U R y z -> exists u : _, R x u /\ Rstar U R u z.
+Proof.
+generalize Rstar_contains_Rplus; intro T; red in T.
+generalize Rstar_transitive; intro T1; red in T1.
+intros U R x y z H'; elim H'.
+intros x0 H'0; elim H'0.
+intros x1 y0 H'1; exists y0; auto with sets.
+intros x1 y0 z0 H'1 H'2 H'3; exists y0; auto with sets.
+intros x0 y0 z0 H'0 H'1 H'2 H'3; exists y0.
+split; [ try assumption | idtac ].
+apply T1 with z0; auto with sets.
+Qed.
+
+Theorem Lemma1 :
+ forall (U:Type) (R:Relation U),
+ Strongly_confluent U R ->
+ forall x b:U,
+ Rstar U R x b ->
+ forall a:U, R x a -> exists z : _, Rstar U R a z /\ R b z.
+Proof.
+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 3H' with (x := x0) (a := a) (b := y); intro H'7; lapply H'7;
+ [ intro H'8; lapply H'8;
+ [ intro H'9; try exact H'9; clear H'8 H'7 | clear H'8 H'7 ]
+ | clear H'7 ]; auto with sets.
+elim H'9.
+intros t H'5; elim H'5; intros H'6 H'7; try exact H'6; clear H'5.
+elim (H'3 t); auto with sets.
+intros z1 H'5; elim H'5; intros H'8 H'10; try exact H'8; clear H'5.
+exists z1; split; [ idtac | assumption ].
+apply Rstar_n with t; auto with sets.
+Qed. \ No newline at end of file
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
new file mode 100755
index 00000000..6a254819
--- /dev/null
+++ b/theories/Sets/Relations_3.v
@@ -0,0 +1,62 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(****************************************************************************)
+(* *)
+(* Naive Set Theory in Coq *)
+(* *)
+(* INRIA INRIA *)
+(* Rocquencourt Sophia-Antipolis *)
+(* *)
+(* Coq V6.1 *)
+(* *)
+(* Gilles Kahn *)
+(* Gerard Huet *)
+(* *)
+(* *)
+(* *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
+(* to the Newton Institute for providing an exceptional work environment *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
+(****************************************************************************)
+
+(*i $Id: Relations_3.v,v 1.7.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+
+Require Export Relations_1.
+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 : U -> Prop :=
+ definition_of_noetherian :
+ forall x:U, (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.
+Hint Unfold confluent: sets v62.
+Hint Unfold Confluent: sets v62.
+Hint Resolve definition_of_noetherian: sets v62.
+Hint Unfold Noetherian: sets v62.
+
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v
new file mode 100755
index 00000000..34322dc7
--- /dev/null
+++ b/theories/Sets/Relations_3_facts.v
@@ -0,0 +1,171 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(****************************************************************************)
+(* *)
+(* Naive Set Theory in Coq *)
+(* *)
+(* INRIA INRIA *)
+(* Rocquencourt Sophia-Antipolis *)
+(* *)
+(* Coq V6.1 *)
+(* *)
+(* Gilles Kahn *)
+(* Gerard Huet *)
+(* *)
+(* *)
+(* *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
+(* to the Newton Institute for providing an exceptional work environment *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
+(****************************************************************************)
+
+(*i $Id: Relations_3_facts.v,v 1.6.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+
+Require Export Relations_1.
+Require Export Relations_1_facts.
+Require Export Relations_2.
+Require Export Relations_2_facts.
+Require Export Relations_3.
+
+Theorem Rstar_imp_coherent :
+ forall (U:Type) (R:Relation U) (x y:U), Rstar U R x y -> coherent U R x y.
+Proof.
+intros U R x y H'; red in |- *.
+exists y; auto with sets.
+Qed.
+Hint Resolve Rstar_imp_coherent.
+
+Theorem coherent_symmetric :
+ forall (U:Type) (R:Relation U), Symmetric U (coherent U R).
+Proof.
+unfold coherent at 1 in |- *.
+intros U R; red in |- *.
+intros x y H'; elim H'.
+intros z H'0; exists z; tauto.
+Qed.
+
+Theorem Strong_confluence :
+ forall (U:Type) (R:Relation U), Strongly_confluent U R -> Confluent U R.
+Proof.
+intros U R H'; red in |- *.
+intro x; red in |- *; intros a b H'0.
+unfold coherent at 1 in |- *.
+generalize b; clear b.
+elim H'0; clear H'0.
+intros x0 b H'1; exists b; auto with sets.
+intros x0 y z H'1 H'2 H'3 b H'4.
+generalize (Lemma1 U R); intro h; lapply h;
+ [ intro H'0; generalize (H'0 x0 b); intro h0; lapply h0;
+ [ intro H'5; generalize (H'5 y); intro h1; lapply h1;
+ [ intro h2; elim h2; intros z0 h3; elim h3; intros H'6 H'7;
+ clear h h0 h1 h2 h3
+ | clear h h0 h1 ]
+ | clear h h0 ]
+ | clear h ]; auto with sets.
+generalize (H'3 z0); intro h; lapply h;
+ [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9; clear h h0 h1
+ | clear h ]; auto with sets.
+exists z1; split; auto with sets.
+apply Rstar_n with z0; auto with sets.
+Qed.
+
+Theorem Strong_confluence_direct :
+ forall (U:Type) (R:Relation U), Strongly_confluent U R -> Confluent U R.
+Proof.
+intros U R H'; red in |- *.
+intro x; red in |- *; intros a b H'0.
+unfold coherent at 1 in |- *.
+generalize b; clear b.
+elim H'0; clear H'0.
+intros x0 b H'1; exists b; auto with sets.
+intros x0 y z H'1 H'2 H'3 b H'4.
+cut (ex (fun t:U => Rstar U R y t /\ R b t)).
+intro h; elim h; intros t h0; elim h0; intros H'0 H'5; clear h h0.
+generalize (H'3 t); intro h; lapply h;
+ [ intro h0; elim h0; intros z0 h1; elim h1; intros H'6 H'7; clear h h0 h1
+ | clear h ]; auto with sets.
+exists z0; split; [ assumption | idtac ].
+apply Rstar_n with t; auto with sets.
+generalize H'1; generalize y; clear H'1.
+elim H'4.
+intros x1 y0 H'0; exists y0; auto with sets.
+intros x1 y0 z0 H'0 H'1 H'5 y1 H'6.
+red in H'.
+generalize (H' x1 y0 y1); intro h; lapply h;
+ [ intro H'7; lapply H'7;
+ [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9;
+ clear h H'7 h0 h1
+ | clear h ]
+ | clear h ]; auto with sets.
+generalize (H'5 z1); intro h; lapply h;
+ [ intro h0; elim h0; intros t h1; elim h1; intros H'7 H'10; clear h h0 h1
+ | clear h ]; auto with sets.
+exists t; split; auto with sets.
+apply Rstar_n with z1; auto with sets.
+Qed.
+
+Theorem Noetherian_contains_Noetherian :
+ forall (U:Type) (R R':Relation U),
+ Noetherian U R -> contains U R R' -> Noetherian U R'.
+Proof.
+unfold Noetherian at 2 in |- *.
+intros U R R' H' H'0 x.
+elim (H' x); auto with sets.
+Qed.
+
+Theorem Newman :
+ forall (U:Type) (R:Relation U),
+ Noetherian U R -> Locally_confluent U R -> Confluent U R.
+Proof.
+intros U R H' H'0; red in |- *; intro x.
+elim (H' x); unfold confluent in |- *.
+intros x0 H'1 H'2 y z H'3 H'4.
+generalize (Rstar_cases U R x0 y); intro h; lapply h;
+ [ intro h0; elim h0;
+ [ clear h h0; intro h1
+ | intro h1; elim h1; intros u h2; elim h2; intros H'5 H'6;
+ clear h h0 h1 h2 ]
+ | clear h ]; auto with sets.
+elim h1; auto with sets.
+generalize (Rstar_cases U R x0 z); intro h; lapply h;
+ [ intro h0; elim h0;
+ [ clear h h0; intro h1
+ | intro h1; elim h1; intros v h2; elim h2; intros H'7 H'8;
+ clear h h0 h1 h2 ]
+ | clear h ]; auto with sets.
+elim h1; generalize coherent_symmetric; intro t; red in t; auto with sets.
+unfold Locally_confluent, locally_confluent, coherent in H'0.
+generalize (H'0 x0 u v); intro h; lapply h;
+ [ intro H'9; lapply H'9;
+ [ intro h0; elim h0; intros t h1; elim h1; intros H'10 H'11;
+ clear h H'9 h0 h1
+ | clear h ]
+ | clear h ]; auto with sets.
+clear H'0.
+unfold coherent at 1 in H'2.
+generalize (H'2 u); intro h; lapply h;
+ [ intro H'0; generalize (H'0 y t); intro h0; lapply h0;
+ [ intro H'9; lapply H'9;
+ [ intro h1; elim h1; intros y1 h2; elim h2; intros H'12 H'13;
+ clear h h0 H'9 h1 h2
+ | clear h h0 ]
+ | clear h h0 ]
+ | clear h ]; auto with sets.
+generalize Rstar_transitive; intro T; red in T.
+generalize (H'2 v); intro h; lapply h;
+ [ intro H'9; generalize (H'9 y1 z); intro h0; lapply h0;
+ [ intro H'14; lapply H'14;
+ [ intro h1; elim h1; intros z1 h2; elim h2; intros H'15 H'16;
+ clear h h0 H'14 h1 h2
+ | clear h h0 ]
+ | clear h h0 ]
+ | clear h ]; auto with sets.
+red in |- *; (exists z1; split); auto with sets.
+apply T with y1; auto with sets.
+apply T with t; auto with sets.
+Qed. \ No newline at end of file
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
new file mode 100644
index 00000000..10d26f22
--- /dev/null
+++ b/theories/Sets/Uniset.v
@@ -0,0 +1,215 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: Uniset.v,v 1.9.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+
+(** Sets as characteristic functions *)
+
+(* G. Huet 1-9-95 *)
+(* Updated Papageno 12/98 *)
+
+Require Import Bool.
+
+Set Implicit Arguments.
+
+Section defs.
+
+Variable A : Set.
+Variable eqA : A -> A -> Prop.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+
+Inductive uniset : Set :=
+ Charac : (A -> bool) -> uniset.
+
+Definition charac (s:uniset) (a:A) : bool := let (f) := s in f a.
+
+Definition Emptyset := Charac (fun a:A => false).
+
+Definition Fullset := Charac (fun a:A => true).
+
+Definition Singleton (a:A) :=
+ Charac
+ (fun a':A =>
+ match eqA_dec a a' with
+ | left h => true
+ | right h => false
+ end).
+
+Definition In (s:uniset) (a:A) : Prop := charac s a = true.
+Hint Unfold In.
+
+(** uniset inclusion *)
+Definition incl (s1 s2:uniset) := forall a:A, leb (charac s1 a) (charac s2 a).
+Hint Unfold incl.
+
+(** uniset equality *)
+Definition seq (s1 s2:uniset) := forall a:A, charac s1 a = charac s2 a.
+Hint Unfold seq.
+
+Lemma leb_refl : forall b:bool, leb b b.
+Proof.
+destruct b; simpl in |- *; auto.
+Qed.
+Hint Resolve leb_refl.
+
+Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2.
+Proof.
+unfold incl in |- *; intros s1 s2 E a; elim (E a); auto.
+Qed.
+
+Lemma incl_right : forall s1 s2:uniset, seq s1 s2 -> incl s2 s1.
+Proof.
+unfold incl in |- *; intros s1 s2 E a; elim (E a); auto.
+Qed.
+
+Lemma seq_refl : forall x:uniset, seq x x.
+Proof.
+destruct x; unfold seq in |- *; auto.
+Qed.
+Hint Resolve seq_refl.
+
+Lemma seq_trans : forall x y z:uniset, seq x y -> seq y z -> seq x z.
+Proof.
+unfold seq in |- *.
+destruct x; destruct y; destruct z; simpl in |- *; intros.
+rewrite H; auto.
+Qed.
+
+Lemma seq_sym : forall x y:uniset, seq x y -> seq y x.
+Proof.
+unfold seq in |- *.
+destruct x; destruct y; simpl in |- *; auto.
+Qed.
+
+(** uniset union *)
+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.
+Hint Resolve union_empty_left.
+
+Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset).
+Proof.
+unfold seq in |- *; unfold union in |- *; simpl in |- *.
+intros x a; rewrite (orb_b_false (charac x a)); auto.
+Qed.
+Hint Resolve union_empty_right.
+
+Lemma union_comm : forall x y:uniset, seq (union x y) (union y x).
+Proof.
+unfold seq in |- *; unfold charac in |- *; unfold union in |- *.
+destruct x; destruct y; auto with bool.
+Qed.
+Hint Resolve union_comm.
+
+Lemma union_ass :
+ forall x y z:uniset, seq (union (union x y) z) (union x (union y z)).
+Proof.
+unfold seq in |- *; unfold union in |- *; unfold charac in |- *.
+destruct x; destruct y; destruct z; auto with bool.
+Qed.
+Hint Resolve union_ass.
+
+Lemma seq_left : forall x y z:uniset, seq x y -> seq (union x z) (union y z).
+Proof.
+unfold seq in |- *; unfold union in |- *; unfold charac in |- *.
+destruct x; destruct y; destruct z.
+intros; elim H; auto.
+Qed.
+Hint Resolve seq_left.
+
+Lemma seq_right : forall x y z:uniset, seq x y -> seq (union z x) (union z y).
+Proof.
+unfold seq in |- *; unfold union in |- *; unfold charac in |- *.
+destruct x; destruct y; destruct z.
+intros; elim H; auto.
+Qed.
+Hint Resolve seq_right.
+
+
+(** All the proofs that follow duplicate [Multiset_of_A] *)
+
+(** 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.
+intros; apply (op_rotate uniset union seq); auto.
+exact seq_trans.
+Qed.
+
+Lemma seq_congr :
+ forall x y z t:uniset, seq x y -> seq z t -> seq (union x z) (union y t).
+Proof.
+intros; apply (cong_congr uniset union seq); auto.
+exact seq_trans.
+Qed.
+
+Lemma union_perm_left :
+ forall x y z:uniset, seq (union x (union y z)) (union y (union x z)).
+Proof.
+intros; apply (perm_left uniset union seq); auto.
+exact seq_trans.
+Qed.
+
+Lemma uniset_twist1 :
+ forall x y z t:uniset,
+ seq (union x (union (union y z) t)) (union (union y (union x t)) z).
+Proof.
+intros; apply (twist uniset union seq); auto.
+exact seq_trans.
+Qed.
+
+Lemma uniset_twist2 :
+ forall x y z t:uniset,
+ seq (union x (union (union y z) t)) (union (union y (union x z)) t).
+Proof.
+intros; apply seq_trans with (union (union x (union y z)) t).
+apply seq_sym; apply union_ass.
+apply seq_left; apply union_perm_left.
+Qed.
+
+(** specific for treesort *)
+
+Lemma treesort_twist1 :
+ forall x y z t u:uniset,
+ seq u (union y z) ->
+ seq (union x (union u t)) (union (union y (union x t)) z).
+Proof.
+intros; apply seq_trans with (union x (union (union y z) t)).
+apply seq_right; apply seq_left; trivial.
+apply uniset_twist1.
+Qed.
+
+Lemma treesort_twist2 :
+ forall x y z t u:uniset,
+ seq u (union y z) ->
+ seq (union x (union u t)) (union (union y (union x z)) t).
+Proof.
+intros; apply seq_trans with (union x (union (union y z) t)).
+apply seq_right; apply seq_left; trivial.
+apply uniset_twist2.
+Qed.
+
+
+(*i theory of minter to do similarly
+Require Min.
+(* uniset intersection *)
+Definition minter := [m1,m2:uniset]
+ (Charac [a:A](andb (charac m1 a)(charac m2 a))).
+i*)
+
+End defs.
+
+Unset Implicit Arguments. \ No newline at end of file
diff --git a/theories/Sets/intro.tex b/theories/Sets/intro.tex
new file mode 100755
index 00000000..83c2177f
--- /dev/null
+++ b/theories/Sets/intro.tex
@@ -0,0 +1,24 @@
+\section{Sets}\label{Sets}
+
+This is a library on sets defined by their characteristic predicate.
+It contains the following modules:
+
+\begin{itemize}
+\item {\tt Ensembles.v}
+\item {\tt Constructive\_sets.v}, {\tt Classical\_sets.v}
+\item {\tt Relations\_1.v}, {\tt Relations\_2.v},
+ {\tt Relations\_3.v}, {\tt Relations\_1\_facts.v}, \\
+ {\tt Relations\_2\_facts.v}, {\tt Relations\_3\_facts.v}
+\item {\tt Partial\_Order.v}, {\tt Cpo.v}
+\item {\tt Powerset.v}, {\tt Powerset\_facts.v},
+ {\tt Powerset\_Classical\_facts.v}
+\item {\tt Finite\_sets.v}, {\tt Finite\_sets\_facts.v}
+\item {\tt Image.v}
+\item {\tt Infinite\_sets.v}
+\item {\tt Integers.v}
+\end{itemize}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End: