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.