diff options
author | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-17 12:53:34 +0000 |
---|---|---|
committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-17 12:53:34 +0000 |
commit | 28dc7a05cc1d3e03ed1435b3db4340db954a59e2 (patch) | |
tree | 63cdf18cd47260eb90550f62f7b22e2e2e208f6c /theories/Sets/Cpo.v | |
parent | 744e7f6a319f4d459a3cc2309f575d43041d75aa (diff) |
Mise en forme des theories
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Sets/Cpo.v')
-rw-r--r-- | theories/Sets/Cpo.v | 103 |
1 files changed, 52 insertions, 51 deletions
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index efd83c106..c1e64babc 100644 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -31,79 +31,80 @@ 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 |