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