Require Export Setoid.
Structure CompletePartialOrder := {
    ltype :> Type;
    Sup : (ltype -> Prop) -> Prop;
    le : ltype -> ltype -> Prop;
    join : (ltype -> Prop) -> ltype;
    le_refl : forall x, le x x;
    le_tsym : forall x y, le x y -> le y x -> x = y;
    le_trans : forall x y z, le x y -> le y z -> le x z;
    le_joinP : forall (M : ltype -> Prop) (y : ltype),
                 Sup M -> ((forall x, M x -> le x y) <-> le (join M) y)
}.

Notation "x <= y" := (@le _ x y) : poset_scope.
Open Scope poset_scope.


Hint Resolve le_refl.

Instance Transitivity_le {T : CompletePartialOrder} : Transitive (@le T).

Section Facts.

Variable T : CompletePartialOrder.
Implicit Types (x y z : T) (M : T -> Prop).

Lemma join_le M y : Sup M -> (forall x, M x -> x <= y) -> join M <= y.

Lemma join_ub M x : Sup M -> M x -> x <= join M.

Lemma le_join M x : Sup M -> (exists2 y, M y & x <= y) -> x <= join M.

Definition bot : T := join (fun _ => False).

Lemma botP x : Sup (fun _ : T => False) -> bot <= x.

Lemma join_mono (M N : T -> Prop) :
  Sup M -> Sup N -> (forall x , M x -> N x) -> join M <= join N.

Lemma join_eqI (M N : T -> Prop) :
  Sup M -> Sup (fun x => M x /\ N x) ->
  (forall x, M x -> exists y, x <= y /\ M y /\ N y) ->
  join M = join (fun x => M x /\ N x).

End Facts.