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.

Arguments Sup {c} M.
Arguments le {c} x y.
Arguments join {c} M.
Arguments le_refl {c} x.
Arguments le_tsym {c x y} le_x_y le_y_x.
Arguments le_trans {c x} y {z} le_x_y le_y_z.
Arguments le_joinP {c} M y cm.

Hint Resolve le_refl.

Instance Transitivity_le {T : CompletePartialOrder} : Transitive (@le T).
Proof. intros x y z. apply le_trans. Qed.

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.
Proof. apply le_joinP. Qed.

Lemma join_ub M x : Sup M -> M x -> x <= join M.
Proof. intros cm. now apply <- (le_joinP M). Qed.

Lemma le_join M x : Sup M -> (exists2 y, M y & x <= y) -> x <= join M.
Proof. intros cm [y my le_x_y]. transitivity y; [|apply join_ub]; trivial. Qed.

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

Lemma botP x : Sup (fun _ : T => False) -> bot <= x.
Proof. intros ce. now apply join_le. Qed.

Lemma join_mono (M N : T -> Prop) :
  Sup M -> Sup N -> (forall x , M x -> N x) -> join M <= join N.
Proof with auto.
  intros cm cn sub. apply join_le... intros x px. apply join_ub...
Qed.

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).
Proof with auto.
  intros cm cmn D. apply le_tsym; [|apply join_mono; tauto].
  apply join_le... intros x px. destruct (D _ px) as [y [y1 [y2 y3]]].
  apply le_join... exists y; tauto.
Qed.

End Facts.

Arguments bot {T}.