diff options
Diffstat (limited to 'theories/Sets/Cpo.v')
| -rwxr-xr-x | theories/Sets/Cpo.v | 110 |
1 files changed, 56 insertions, 54 deletions
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index c234bd1c7..0d77c0617 100755 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -31,77 +31,79 @@ Require Export Relations_1. Require Export Partial_Order. Section Bounds. -Variable U: Type. -Variable D: (PO U). +Variable U : Type. +Variable D : PO U. -Local C := (Carrier_of U D). +Let C := Carrier_of U D. -Local R := (Rel_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) -> ((y: U) (In U B y) -> (R y x)) -> (Upper_Bound B x). +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) -> ((y: U) (In U B y) -> (R x y)) -> (Lower_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) -> ((y: U) (Upper_Bound B y) -> (R x y)) -> (Lub 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) -> ((y: U) (Lower_Bound B y) -> (R y x)) -> (Glb 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) -> ((y: U) (In U C y) -> (R bot y)) -> (Bottom bot). +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) -> - (x: U) (y: U) (Included U (Couple U x y) B) -> (R x y) \/ (R y x)) -> - (Totally_ordered B). +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) := - [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)). +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) -> - ((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 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: - ((EXT bot | (Bottom bot))) -> - ((X: (Ensemble U)) (Directed X) -> (EXT bsup | (Lub X bsup))) -> - Complete. + 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: - ((X: (Ensemble U)) - (Included U X C) -> (EXT maj | (Upper_Bound X maj)) -> - (EXT bsup | (Lub X bsup))) -> Conditionally_complete. + 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. -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. +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. +Variable U : Type. -Record Cpo : Type := Definition_of_cpo { - PO_of_cpo: (PO U); - Cpo_cond: (Complete U PO_of_cpo) }. +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)) }. +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. +End Specific_orders.
\ No newline at end of file |