Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 109 insertions, 0 deletions

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