diff options
Diffstat (limited to 'theories/Sets/Cpo.v')
| -rw-r--r-- | theories/Sets/Cpo.v | 105 |
1 files changed, 53 insertions, 52 deletions
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index 0b2cf3e3..1e1b70d5 100644 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -24,86 +24,87 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id: Cpo.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Cpo.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Export Ensembles. Require Export Relations_1. Require Export Partial_Order. Section Bounds. -Variable U : Type. -Variable D : PO U. + Variable U : Type. + Variable D : PO U. -Let C := Carrier_of U D. + Let C := Carrier_of U D. + + Let R := Rel_of U D. -Let R := Rel_of U D. - -Inductive Upper_Bound (B:Ensemble U) (x:U) : Prop := + 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. + 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 := + 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 := + 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. + 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 := + 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. + Lower_Bound B x -> (forall y:U, Lower_Bound B y -> R y x) -> Glb B x. -Inductive Bottom (bot:U) : Prop := + 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 := + 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. + (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. + 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 Complete : Prop := + 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. + (exists bot : _, Bottom bot) -> + (forall X:Ensemble U, Directed X -> exists bsup : _, Lub X bsup) -> + Complete. -Inductive Conditionally_complete : Prop := + 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. + (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)}. + 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 |