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.




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)}.




End Specific_orders.