diff options
Diffstat (limited to 'theories/Sets/Cpo.v')
| -rwxr-xr-x | theories/Sets/Cpo.v | 109 |
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 |