diff options
Diffstat (limited to 'theories7/Sets/Cpo.v')
| -rwxr-xr-x | theories7/Sets/Cpo.v | 107 |
1 files changed, 0 insertions, 107 deletions
diff --git a/theories7/Sets/Cpo.v b/theories7/Sets/Cpo.v deleted file mode 100755 index 2fe46be6..00000000 --- a/theories7/Sets/Cpo.v +++ /dev/null @@ -1,107 +0,0 @@ -(************************************************************************) -(* 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.1.2.1 2004/07/16 19:31:38 herbelin Exp $ i*) - -Require Export Ensembles. -Require Export Relations_1. -Require Export Partial_Order. - -Section Bounds. -Variable U: Type. -Variable D: (PO U). - -Local C := (Carrier_of U D). - -Local R := (Rel_of U D). - -Inductive Upper_Bound [B:(Ensemble U); x:U]: Prop := - Upper_Bound_definition: - (In U C x) -> ((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) -> ((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) -> ((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) -> ((y: U) (Lower_Bound B y) -> (R y x)) -> (Glb B x). - -Inductive Bottom [bot:U]: Prop := - Bottom_definition: - (In U C bot) -> ((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) -> - (x: U) (y: U) (Included U (Couple U x y) B) -> (R x y) \/ (R y x)) -> - (Totally_ordered B). - -Definition Compatible : (Relation U) := - [x: U] [y: U] (In U C x) -> (In U C y) -> - (EXT 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) -> - ((x1: U) (x2: U) (Included U (Couple U x1 x2) X) -> - (EXT x3 | (In U X x3) /\ (Upper_Bound (Couple U x1 x2) x3))) -> - (Directed X). - -Inductive Complete : Prop := - Definition_of_Complete: - ((EXT bot | (Bottom bot))) -> - ((X: (Ensemble U)) (Directed X) -> (EXT bsup | (Lub X bsup))) -> - Complete. - -Inductive Conditionally_complete : Prop := - Definition_of_Conditionally_complete: - ((X: (Ensemble U)) - (Included U X C) -> (EXT maj | (Upper_Bound X maj)) -> - (EXT bsup | (Lub X bsup))) -> Conditionally_complete. -End Bounds. -Hints 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. |