(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

Require Import Ensembles.
Require Import Relations_1.
Require Import Partial_Order.
Require Import Cpo.
Require Import algpodefs.
Require Import Powerset.
Section Lemmas_on_partial_orders.
Variable U : Type.
Variable B : Ensemble U.
Variable D : PO U.

Theorem Rel_of_reflexive : forall x : U, Rel_of U D x x.
Proof.
(* Goal: @ex U (fun maj : U => Upper_Bound U D (Empty_set U) maj) *)
elim D.
(* Goal: forall (Carrier_of : Ensemble U) (Rel_of0 : Relation U) (PO_cond1 : Inhabited U Carrier_of) (PO_cond2 : Order U Rel_of0), Transitive U (Rel_of U (Definition_of_PO U Carrier_of Rel_of0 PO_cond1 PO_cond2)) *)
intros Carrier_of Rel_of PO_cond1 PO_cond2; elim PO_cond2; auto with sets.
Qed.
Hint Resolve Rel_of_reflexive.

Theorem Rel_of_antisymmetric : Antisymmetric U (Rel_of U D).
Proof.
(* Goal: @ex U (fun maj : U => Upper_Bound U D (Empty_set U) maj) *)
elim D.
(* Goal: forall (Carrier_of : Ensemble U) (Rel_of0 : Relation U) (PO_cond1 : Inhabited U Carrier_of) (PO_cond2 : Order U Rel_of0), Transitive U (Rel_of U (Definition_of_PO U Carrier_of Rel_of0 PO_cond1 PO_cond2)) *)
intros Carrier_of Rel_of PO_cond1 PO_cond2; elim PO_cond2; auto with sets.
Qed.
Hint Resolve Rel_of_antisymmetric.

Theorem Rel_of_transitive : Transitive U (Rel_of U D).
Proof.
(* Goal: @ex U (fun maj : U => Upper_Bound U D (Empty_set U) maj) *)
elim D.
(* Goal: forall (Carrier_of : Ensemble U) (Rel_of0 : Relation U) (PO_cond1 : Inhabited U Carrier_of) (PO_cond2 : Order U Rel_of0), Transitive U (Rel_of U (Definition_of_PO U Carrier_of Rel_of0 PO_cond1 PO_cond2)) *)
intros Carrier_of Rel_of PO_cond1 PO_cond2; elim PO_cond2; auto with sets.
Qed.
Hint Resolve Rel_of_transitive.

Theorem Couple_included_in_carrier :
 forall x y : U,
 In U (Carrier_of U D) x ->
 In U (Carrier_of U D) y -> Included U (Couple U x y) (Carrier_of U D).
Proof.
(* Goal: forall (x y : U) (_ : In U (Carrier_of U D) x) (_ : In U (Carrier_of U D) y), Included U (Couple U x y) (Carrier_of U D) *)
intros x y H' H'0; red in |- *.
(* Goal: forall (x0 : U) (_ : In U (Couple U x y) x0), In U (Carrier_of U D) x0 *)
intros x0 H'1; elim H'1; auto with sets.
Qed.
Hint Resolve Couple_included_in_carrier.

Theorem Lub_is_in_Carrier :
 forall (bsup : U) (X : Ensemble U),
 Included U X (Carrier_of U D) ->
 Lub U D X bsup -> In U (Carrier_of U D) bsup.
Proof.
(* Goal: forall (bsup : U) (X : Ensemble U) (_ : Included U X (Carrier_of U D)) (_ : Lub U D X bsup), In U (Carrier_of U D) bsup *)
intros bsup X H' H'0; elim H'0.
(* Goal: forall (_ : Upper_Bound U D X bsup) (_ : forall (y : U) (_ : Upper_Bound U D X y), Rel_of U D bsup y), In U (Carrier_of U D) bsup *)
intro H'1; elim H'1; auto with sets.
Qed.

Theorem Singleton_has_lub :
 forall x : U, In U (Carrier_of U D) x -> Lub U D (Singleton U x) x.
Proof.
(* Goal: forall (x : U) (_ : In U (Carrier_of U D) x), Lub U D (Singleton U x) x *)
intros x H'.
(* Goal: Lub U PO_of_cpo (Empty_set U) bot *)
apply Lub_definition.
(* Goal: Upper_Bound U PO_of_cpo (Empty_set U) bot *)
(* Goal: forall (y : U) (_ : Upper_Bound U PO_of_cpo (Empty_set U) y), Rel_of U PO_of_cpo bot y *)
apply Upper_Bound_definition; auto with sets.
(* Goal: forall (y : U) (_ : In U (Empty_set U) y), Rel_of U D y x *)
intros y H'0; elim H'0; auto with sets.
(* Goal: forall (y : U) (_ : In U (Empty_set U) y), Rel_of U D y x *)
intros y H'0; elim H'0; auto with sets.
Qed.
Hint Resolve Singleton_has_lub.

Theorem Empty_set_has_Upper_Bound :
 exists maj : U, Upper_Bound U D (Empty_set U) maj.
Proof.
(* Goal: @ex U (fun maj : U => Upper_Bound U D (Empty_set U) maj) *)
elim D.
(* Goal: forall (Carrier_of : Ensemble U) (Rel_of : Relation U) (PO_cond1 : Inhabited U Carrier_of) (PO_cond2 : Order U Rel_of), @ex U (fun maj : U => Upper_Bound U (Definition_of_PO U Carrier_of Rel_of PO_cond1 PO_cond2) (Empty_set U) maj) *)
intros C R cond1 cond2.
(* Goal: @ex U (fun maj : U => Upper_Bound U (Definition_of_PO U C R cond1 cond2) (Empty_set U) maj) *)
elim cond1.
(* Goal: forall (x : U) (_ : In U C x), @ex U (fun maj : U => Upper_Bound U (Definition_of_PO U C R cond1 cond2) (Empty_set U) maj) *)
intros x H'; exists x.
(* Goal: Upper_Bound U PO_of_cpo (Empty_set U) bot *)
(* Goal: forall (y : U) (_ : Upper_Bound U PO_of_cpo (Empty_set U) y), Rel_of U PO_of_cpo bot y *)
apply Upper_Bound_definition; auto with sets.
(* Goal: forall (y : U) (_ : In U (Empty_set U) y), Rel_of U D y x *)
intros y H'0; elim H'0; auto with sets.
Qed.
Hint Resolve Empty_set_has_Upper_Bound.

Theorem Anyone_is_Upper_Bound_of_Empty_set :
 forall x : U, In U (Carrier_of U D) x -> Upper_Bound U D (Empty_set U) x.
(* Goal: Upper_Bound U PO_of_cpo (Empty_set U) bot *)
(* Goal: forall (y : U) (_ : Upper_Bound U PO_of_cpo (Empty_set U) y), Rel_of U PO_of_cpo bot y *)
intros x H'; apply Upper_Bound_definition; auto with sets.
(* Goal: forall (y : U) (_ : In U (Empty_set U) y), Rel_of U D y x *)
intros y H'0; elim H'0; auto with sets.
Qed.
Hint Resolve Anyone_is_Upper_Bound_of_Empty_set.

Theorem Empty_set_has_lub :
 forall C : Cpo U, exists bsup : U, Lub U (PO_of_cpo U C) (Empty_set U) bsup.
Proof.
(* Goal: forall C : Cpo U, @ex U (fun bsup : U => Lub U (PO_of_cpo U C) (Empty_set U) bsup) *)
intro C; elim C; simpl in |- *.
(* Goal: forall (PO_of_cpo : PO U) (_ : Complete U PO_of_cpo), @ex U (fun bsup : U => Lub U PO_of_cpo (Empty_set U) bsup) *)
intros PO_of_cpo Cpo_cond; elim Cpo_cond; clear Cpo_cond.
(* Goal: forall (_ : @ex U (fun bot : U => Bottom U PO_of_cpo bot)) (_ : forall (X : Ensemble U) (_ : Directed U PO_of_cpo X), @ex U (fun bsup : U => Lub U PO_of_cpo X bsup)), @ex U (fun bsup : U => Lub U PO_of_cpo (Empty_set U) bsup) *)
intro H'; elim H'; clear H'.
(* Goal: forall (x : U) (_ : Bottom U PO_of_cpo x) (_ : forall (X : Ensemble U) (_ : Directed U PO_of_cpo X), @ex U (fun bsup : U => Lub U PO_of_cpo X bsup)), @ex U (fun bsup : U => Lub U PO_of_cpo (Empty_set U) bsup) *)
intros bot is_bot H'0; exists bot; simpl in |- *.
(* Goal: Lub U PO_of_cpo (Empty_set U) bot *)
elim is_bot; intros H' H'1.
(* Goal: Lub U PO_of_cpo (Empty_set U) bot *)
apply Lub_definition.
(* Goal: Upper_Bound U PO_of_cpo (Empty_set U) bot *)
(* Goal: forall (y : U) (_ : Upper_Bound U PO_of_cpo (Empty_set U) y), Rel_of U PO_of_cpo bot y *)
apply Upper_Bound_definition; auto with sets.
(* Goal: forall (y : U) (_ : Upper_Bound U PO_of_cpo (Empty_set U) y), Rel_of U PO_of_cpo bot y *)
intros y H'2; elim H'2; auto with sets.
(* Goal: forall (y : U) (_ : Upper_Bound U PO_of_cpo (Empty_set U) y), Rel_of U PO_of_cpo bot y *)
intros y H'2; elim H'2; auto with sets.
Qed.
Hint Resolve Empty_set_has_lub.

Theorem Upper_downward_stable :
 forall (A B : Ensemble U) (maj : U),
 Included U A (Carrier_of U D) ->
 Included U B (Carrier_of U D) ->
 Included U A B -> Upper_Bound U D B maj -> Upper_Bound U D A maj.
Proof.
(* Goal: forall (A B : Ensemble U) (maj : U) (_ : Included U A (Carrier_of U D)) (_ : Included U B (Carrier_of U D)) (_ : Included U A B) (_ : Upper_Bound U D B maj), Upper_Bound U D A maj *)
intros A B0 maj H' H'0 H'1 H'2; elim H'2; auto with sets.
Qed.

Theorem Conditionally_complete_has_a_bottom :
 Conditionally_complete U D -> exists bot : U, Bottom U D bot.
Proof.
(* Goal: forall _ : Conditionally_complete U D, @ex U (fun bot : U => Bottom U D bot) *)
intro H'; elim H'.
intro H'0; elim (H'0 (Empty_set U));
(* Goal: forall _ : Coherent U D, @ex U (fun bot : U => Bottom U D bot) *)
 [ intros bsup E; elim E | idtac | idtac ]; auto with sets.
(* Goal: forall (_ : Upper_Bound U D (Empty_set U) bsup) (_ : forall (y : U) (_ : Upper_Bound U D (Empty_set U) y), Rel_of U D bsup y), @ex U (fun bot : U => Bottom U D bot) *)
intros H'1 H'2; exists bsup.
(* Goal: Bottom U D bsup *)
elim H'1; auto with sets.
Qed.
Hint Resolve Conditionally_complete_has_a_bottom.

Theorem Bottom_is_compact :
 Conditionally_complete U D ->
 exists bot : U, Bottom U D bot /\ Compact U D bot.
Proof.
intro H'; lapply Conditionally_complete_has_a_bottom;
 [ intro H'0 | try assumption ].
(* Goal: @ex U (fun bot : U => and (Bottom U D bot) (Compact U D bot)) *)
elim H'0; intros bot E; clear H'0.
(* Goal: @ex U (fun bot : U => and (Bottom U D bot) (Compact U D bot)) *)
exists bot; split; auto with sets.
(* Goal: Compact U D bot *)
apply Definition_of_compact; auto with sets.
(* Goal: and (In U X x) (Rel_of U D bot x) *)
elim E; auto with sets.
(* Goal: forall (X : Ensemble U) (_ : Directed U D X) (_ : @ex U (fun bsup : U => and (Lub U D X bsup) (Rel_of U D bot bsup))), @ex U (fun y : U => and (In U X y) (Rel_of U D bot y)) *)
intros X H'0; elim H'0.
(* Goal: forall (_ : Included U X (Carrier_of U D)) (_ : Inhabited U X) (_ : forall (x1 x2 : U) (_ : Included U (Couple U x1 x2) X), @ex U (fun x3 : U => and (In U X x3) (Upper_Bound U D (Couple U x1 x2) x3))) (_ : @ex U (fun bsup : U => and (Lub U D X bsup) (Rel_of U D bot bsup))), @ex U (fun y : U => and (In U X y) (Rel_of U D bot y)) *)
intros H'1 H'2; elim H'2.
(* Goal: forall (x : U) (_ : In U X x) (_ : forall (x1 x2 : U) (_ : Included U (Couple U x1 x2) X), @ex U (fun x3 : U => and (In U X x3) (Upper_Bound U D (Couple U x1 x2) x3))) (_ : @ex U (fun bsup : U => and (Lub U D X bsup) (Rel_of U D bot bsup))), @ex U (fun y : U => and (In U X y) (Rel_of U D bot y)) *)
intros x H'3 H'4 H'5; try assumption.
(* Goal: @ex U (fun y : U => and (In U X y) (Rel_of U D bot y)) *)
exists x; auto with sets.
(* Goal: and (In U X x) (Rel_of U D bot x) *)
elim E; auto with sets.
Qed.
Hint Resolve Bottom_is_compact.

Theorem Compact_is_in_Carrier :
 forall x : U, Compact U D x -> In U (Carrier_of U D) x.
Proof.
(* Goal: forall (x : U) (_ : Compact U D x), In U (Carrier_of U D) x *)
intros x H'; elim H'; auto with sets.
Qed.
Hint Resolve Compact_is_in_Carrier.

Theorem Compatible_is_reflexive : forall x : U, Compatible U D x x.
Proof.
(* Goal: forall x : U, Compatible U D x x *)
intro x; red in |- *; simpl in |- *.
(* Goal: forall (_ : In U (Carrier_of U D) x) (_ : In U (Carrier_of U D) x), @ex U (fun z : U => and (In U (Carrier_of U D) z) (Upper_Bound U D (Couple U x x) z)) *)
intros H'2 H'3; exists x.
(* Goal: and (In U (Carrier_of U D) x) (Upper_Bound U D (Couple U x x) x) *)
split; [ assumption | apply Upper_Bound_definition ]; auto with sets.
(* Goal: forall (y : U) (_ : In U (Couple U x x) y), Rel_of U D y x *)
intros y H'; elim H'; auto with sets.
Qed.
Hint Resolve Compatible_is_reflexive.

Theorem Couple_is_symmetric :
 forall x y : U, Couple U x y = Couple U y x :>Ensemble U.
Proof.
(* Goal: forall x y : U, @eq (Ensemble U) (Couple U x y) (Couple U y x) *)
intros x y; apply Extensionality_Ensembles; red in |- *.
(* Goal: and (Included U (Couple U x y) (Couple U y x)) (Included U (Couple U y x) (Couple U x y)) *)
split; red in |- *; (intros x0 H'; elim H'); auto with sets.
Qed.

Theorem Compatible_is_symmetric :
 forall x y : U, Compatible U D x y -> Compatible U D y x.
Proof.
(* Goal: forall (x y : U) (_ : Compatible U D x y), Compatible U D y x *)
unfold Compatible in |- *.
(* Goal: forall (x y : U) (_ : forall (_ : In U (Carrier_of U D) x) (_ : In U (Carrier_of U D) y), @ex U (fun z : U => and (In U (Carrier_of U D) z) (Upper_Bound U D (Couple U x y) z))) (_ : In U (Carrier_of U D) y) (_ : In U (Carrier_of U D) x), @ex U (fun z : U => and (In U (Carrier_of U D) z) (Upper_Bound U D (Couple U y x) z)) *)
intros x y H' H'0 H'1.
(* Goal: @ex U (fun z : U => and (In U (Carrier_of U D) z) (Upper_Bound U D (Couple U y x) z)) *)
rewrite <- (Couple_is_symmetric x y); auto with sets.
Qed.
Hint Immediate Compatible_is_symmetric.

Theorem Compatible_imp_consistent :
 forall x y : U, Compatible U D x y -> Consistent U D (Couple U x y).
(* Goal: forall (x y : U) (_ : Compatible U D x y), Consistent U D (Couple U x y) *)
intros x y H'; red in |- *; simpl in |- *.
(* Goal: forall (_ : Included U (Couple U x y) (Carrier_of U D)) (x0 y0 : U) (_ : Included U (Couple U x0 y0) (Couple U x y)), Compatible U D x0 y0 *)
intros H'0 x0 y0 H'1; try assumption.
(* Goal: Compatible U D x0 y0 *)
red in H'1.
(* Goal: Compatible U D x0 y0 *)
lapply (H'1 x0); [ intro H'3 | auto with sets ].
(* Goal: Compatible U D x0 y0 *)
lapply (H'1 y0); [ intro H'4 | auto with sets ].
(* Goal: Compatible U D x0 y0 *)
elim H'4.
(* Goal: Compatible U D x0 y *)
elim H'3; auto with sets.
(* Goal: Compatible U D x0 y *)
elim H'3; auto with sets.
Qed.

Theorem Consistent_imp_compatible :
 forall x y : U,
 In U (Carrier_of U D) x ->
 In U (Carrier_of U D) y ->
 Consistent U D (Couple U x y) -> Compatible U D x y.
Proof.
(* Goal: forall (x y : U) (_ : In U (Carrier_of U D) x) (_ : In U (Carrier_of U D) y) (_ : Consistent U D (Couple U x y)), Compatible U D x y *)
intros x y H' H'0 H'1; red in H'1; simpl in H'1; auto with sets.
Qed.

Theorem Coherent_implies_Conditionally_Complete :
 Coherent U D -> Conditionally_complete U D.
Proof.
(* Goal: forall _ : Coherent U D, Conditionally_complete U D *)
intro H'; red in H'.
(* Goal: Conditionally_complete U D *)
apply Definition_of_Conditionally_complete.
(* Goal: forall (X : Ensemble U) (_ : Included U X (Carrier_of U D)) (_ : @ex U (fun maj : U => Upper_Bound U D X maj)), @ex U (fun bsup : U => Lub U D X bsup) *)
intros X H'0 H'1.
(* Goal: @ex U (fun bsup : U => Lub U D X bsup) *)
apply H'; auto with sets.
(* Goal: Consistent U D X *)
red in |- *; simpl in |- *.
(* Goal: Consistent U D X *)
intros H'2 x y H'3; red in |- *; simpl in |- *.
(* Goal: forall (_ : In U (Carrier_of U D) x) (_ : In U (Carrier_of U D) y), @ex U (fun z : U => and (In U (Carrier_of U D) z) (Upper_Bound U D (Couple U x y) z)) *)
intros H'4 H'5.
(* Goal: @ex U (fun z : U => and (In U (Carrier_of U D) z) (Upper_Bound U D (Couple U x y) z)) *)
elim H'1; intros maj E; try exact E; clear H'1.
(* Goal: and (In U X x) (Rel_of U D bot x) *)
exists maj; elim E; auto with sets.
Qed.
Hint Resolve Coherent_implies_Conditionally_Complete.

Theorem Coherent_has_a_bottom :
 Coherent U D -> exists bot : U, Bottom U D bot.
Proof.
(* Goal: forall _ : Coherent U D, @ex U (fun bot : U => Bottom U D bot) *)
auto with sets.
Qed.
Hint Resolve Coherent_has_a_bottom.

Theorem Coherent_implies_Complete : Coherent U D -> Complete U D.
Proof.
(* Goal: forall _ : Coherent U D, Complete U D *)
intro H'.
(* Goal: forall _ : Coherent U D, @ex U (fun bot : U => Bottom U D bot) *)
apply Definition_of_Complete; auto with sets.
(* Goal: forall (X : Ensemble U) (_ : Directed U D X), @ex U (fun bsup : U => Lub U D X bsup) *)
intros X H'0; apply H'.
(* Goal: forall _ : Coherent U D, @ex U (fun bot : U => Bottom U D bot) *)
elim H'0; auto with sets.
(* Goal: Consistent U D X *)
red in |- *; simpl in |- *.
(* Goal: forall (_ : Included U X (Carrier_of U D)) (x y : U) (_ : Included U (Couple U x y) X), Compatible U D x y *)
intros H'1 x y H'2; elim H'0.
(* Goal: forall (_ : Included U X (Carrier_of U D)) (_ : Inhabited U X) (_ : forall (x1 x2 : U) (_ : Included U (Couple U x1 x2) X), @ex U (fun x3 : U => and (In U X x3) (Upper_Bound U D (Couple U x1 x2) x3))), Compatible U D x y *)
intros H'3 H'4 H'5; lapply (H'5 x y); [ intro H'8; elim H'8 | auto with sets ].
(* Goal: Consistent U D X *)
intros x0 H'6; red in |- *; simpl in |- *.
(* Goal: forall (_ : In U (Carrier_of U D) x) (_ : In U (Carrier_of U D) y), @ex U (fun z : U => and (In U (Carrier_of U D) z) (Upper_Bound U D (Couple U x y) z)) *)
intros H'7 H'9; exists x0.
(* Goal: and (In U (Carrier_of U D) x0) (Upper_Bound U D (Couple U x y) x0) *)
intuition.
Qed.
End Lemmas_on_partial_orders.
Hint Resolve Rel_of_reflexive.
Hint Resolve Rel_of_antisymmetric.
Hint Resolve Rel_of_transitive.
Hint Resolve Couple_included_in_carrier.
Hint Resolve Singleton_has_lub.
Hint Resolve Empty_set_has_Upper_Bound.
Hint Resolve Anyone_is_Upper_Bound_of_Empty_set.
Hint Resolve Empty_set_has_lub.
Hint Resolve Conditionally_complete_has_a_bottom.
Hint Resolve Bottom_is_compact.
Hint Resolve Compact_is_in_Carrier.
Hint Resolve Compatible_is_reflexive.
Hint Immediate Compatible_is_symmetric.
Hint Resolve Coherent_implies_Conditionally_Complete.
Hint Resolve Coherent_has_a_bottom.

