Library Coq.Sets.Cpo
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.
#[global]
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 : core.
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 _ PO_of_chain)}.
End Specific_orders.