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

(****************************************************************************)
(* This contribution was updated for Coq V5.10 by the COQ workgroup.        *)
(* January 1995                                                             *)
(****************************************************************************)
(*                                                                          *)
(*      Initial Version: Frederic Prost, July 1993                          *)
(*      Revised Version: Gilles Kahn, September 1993                        *)
(*                               INRIA Sophia-Antipolis, FRANCE             *)
(*      Revised Version: Jean-Christophe Filliatre, January 1995            *)
(*                               ENS-Lyon, FRANCE                           *)
(*                                                                          *)
(****************************************************************************)
(*                          Partial_order_facts.v                           *)
(****************************************************************************)

Require Import Ensembles.
Require Import Relations_1.
Require Import podefs.
Require Import podefs_1.
Require Import ps.

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.
(* Goal: Transitive U (Rel_of U D) *)
   elim D; simpl in |- *; auto.
(* Goal: forall (C : Carrier U) (R : Rel U) (_ : Non_empty U C) (_ : Order U R), Transitive U R *)
   intros C R H' H'0; elim H'0; auto 10.
   Qed.
   Hint Resolve Rel_of_reflexive.
   
   Theorem Rel_of_antisymmetric : Antisymmetric U (Rel_of U D).
(* Goal: Transitive U (Rel_of U D) *)
   elim D; simpl in |- *; auto.
(* Goal: forall (C : Carrier U) (R : Rel U) (_ : Non_empty U C) (_ : Order U R), Transitive U R *)
   intros C R H' H'0; elim H'0; auto 10.
   Qed.
   Hint Resolve Rel_of_antisymmetric.
   
   Theorem Rel_of_transitive : Transitive U (Rel_of U D).
(* Goal: Transitive U (Rel_of U D) *)
   elim D; simpl in |- *; auto.
(* Goal: forall (C : Carrier U) (R : Rel U) (_ : Non_empty U C) (_ : Order U R), Transitive U R *)
   intros C R H' H'0; elim H'0; auto 10.
   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).
(* 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 |- *; auto 20.
(* 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 20.
   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.
(* 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; auto 20.
(* 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 20.
   Qed.
   
   Theorem Singleton_has_lub :
    forall x : U, In U (Carrier_of U D) x -> Lub U D (Singleton U x) x.
(* Goal: forall (x : U) (_ : In U (Carrier_of U D) x), Lub U D (Singleton U x) x *)
   intros x H'; auto 20.
(* Goal: Lub U D (Singleton U x) x *)
   apply Lub_definition; auto 10.
(* Goal: Upper_Bound U D (Empty_set U) y *)
   apply Upper_Bound_definition; auto 10.
(* Goal: forall (y : U) (_ : Upper_Bound U D (Singleton U x) y), Rel_of U D x y *)
   intros y H'0; elim H'0; auto 10.
(* Goal: forall (y : U) (_ : Upper_Bound U D (Singleton U x) y), Rel_of U D x y *)
   intros y H'0; elim H'0; auto 10.
   Qed.
   Hint Resolve Singleton_has_lub.
   
   Theorem Empty_set_has_Upper_Bound :
    exists maj : U, Upper_Bound U D (Empty_set U) maj.
(* Goal: @ex U (fun maj : U => Upper_Bound U D (Empty_set U) maj) *)
   elim D.
(* Goal: forall (C : Carrier U) (R : Rel U) (n : Non_empty U C) (o : Order U R), @ex U (fun maj : U => Upper_Bound U (Definition_of_PO U C R n o) (Empty_set U) maj) *)
   intros C R n o.
(* Goal: @ex U (fun maj : U => Upper_Bound U (Definition_of_PO U C R n o) (Empty_set U) maj) *)
   elim n.
(* Goal: forall (x : U) (_ : In U C x), @ex U (fun maj : U => Upper_Bound U (Definition_of_PO U C R n o) (Empty_set U) maj) *)
   intros x H'; exists x.
(* Goal: Upper_Bound U (Definition_of_PO U C R n o) (Empty_set U) x *)
   apply Upper_Bound_definition; auto.
(* Goal: forall (y : U) (_ : In U (Empty_set U) y), Rel_of U (Definition_of_PO U C R n o) y x *)
   intros y H'0; elim H'0; auto.
   Qed.
   Hint Resolve Empty_set_has_Upper_Bound.
   
   Theorem Empty_set_has_lub :
    Cpo U D -> exists bsup : U, Lub U D (Empty_set U) bsup.
(* Goal: forall _ : Cpo U D, @ex U (fun bsup : U => Lub U D (Empty_set U) bsup) *)
   intro H'; elim H'.
(* Goal: forall (_ : @ex U (fun bot : U => Bottom U D bot)) (_ : forall (X : Ensemble U) (_ : Directed U D X), @ex U (fun bsup : U => Lub U D X bsup)), @ex U (fun bsup : U => Lub U D (Empty_set U) bsup) *)
   intro h; elim h; intros bot E; clear h.
(* Goal: forall _ : forall (X : Ensemble U) (_ : Directed U D X), @ex U (fun bsup : U => Lub U D X bsup), @ex U (fun bsup : U => Lub U D (Empty_set U) bsup) *)
   intro H'0; exists bot.
(* Goal: Lub U D (Empty_set U) bot *)
   apply Lub_definition.
(* Goal: Upper_Bound U D (Empty_set U) bot *)
(* Goal: forall (y : U) (_ : Upper_Bound U D (Empty_set U) y), Rel_of U D bot y *)
   apply Upper_Bound_definition.
(* Goal: forall (_ : In U (Carrier_of U D) y) (_ : forall (y0 : U) (_ : In U (Empty_set U) y0), Rel_of U D y0 y), Rel_of U D bot y *)
   elim E; auto.
(* Goal: forall (y : U) (_ : In U (Couple U x x) y), Rel_of U D y x *)
   intros y H'1; elim H'1; auto.
(* Goal: forall (y : U) (_ : In U (Couple U x x) y), Rel_of U D y x *)
   intros y H'1; elim H'1; auto.
(* Goal: forall (_ : In U (Carrier_of U D) y) (_ : forall (y0 : U) (_ : In U (Empty_set U) y0), Rel_of U D y0 y), Rel_of U D bot y *)
   elim E; auto.
   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.
(* 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 *)
   clear B.
(* 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 BB maj H' H'0 H'1 H'2; elim H'2; auto.
   Qed.
   
   Theorem Conditionally_complete_has_a_bottom :
    Conditionally_complete U D -> exists bot : U, Bottom U D bot.
(* Goal: forall _ : Conditionally_complete U D, @ex U (fun bot : U => Bottom U D bot) *)
   intro H'; elim H'; auto 10.
   intro H'0; generalize (H'0 (Empty_set U)); intro h; lapply h;
    [ intro H'1; lapply H'1;
       [ intro h0; elim h0; intros bsup E; clear h H'1 h0; elim E | clear h ]
    | clear h ]; auto 10.
(* 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; apply Bottom_definition; auto 10.
(* Goal: In U (Carrier_of U D) bsup *)
(* Goal: forall (y : U) (_ : In U (Carrier_of U D) y), Rel_of U D bsup y *)
   elim H'1; auto 10.
(* Goal: forall (y : U) (_ : In U (Carrier_of U D) y), Rel_of U D bsup y *)
   intros y H'3; try assumption; auto 10.
(* Goal: Rel_of U D bsup y *)
   apply H'2; auto 10.
(* Goal: Upper_Bound U D (Empty_set U) y *)
   apply Upper_Bound_definition; auto 10.
(* Goal: forall (y0 : U) (_ : In U (Empty_set U) y0), Rel_of U D y0 y *)
   intros y0 H'4; elim H'4; auto 10.
   Qed.
   Hint Resolve Conditionally_complete_has_a_bottom.

   Theorem Compatible_is_reflexive : Reflexive U (Compatible U D).
(* Goal: Reflexive U (Compatible U D) *)
   red in |- *; intro x; red in |- *.
   exists x; intros H' H'0; split; [ idtac | apply Upper_Bound_definition ];
    auto.
(* Goal: forall (y : U) (_ : In U (Couple U x x) y), Rel_of U D y x *)
   intros y H'1; elim H'1; auto.
   Qed.
   
   Theorem Couple_is_symmetric :
    forall x y : U, Couple U x y = Couple U y x :>Ensemble U.
   intros x y; apply Extensionality_Ensembles; apply Same_set_intro;
    red in |- *; (intros x0 H'; elim H'); auto 10.
   Qed.
   
   Theorem Compatible_is_symmetric : Symmetric U (Compatible U D).
(* Goal: Symmetric U (Compatible U D) *)
   red in |- *; unfold Compatible in |- *.
(* Goal: forall (x y : U) (_ : @ex U (fun z : U => forall (_ : In U (Carrier_of U D) x) (_ : In U (Carrier_of U D) y), and (In U (Carrier_of U D) z) (Upper_Bound U D (Couple U x y) z))), @ex U (fun z : U => forall (_ : In U (Carrier_of U D) y) (_ : In U (Carrier_of U D) x), and (In U (Carrier_of U D) z) (Upper_Bound U D (Couple U y x) z)) *)
   intros x y h; elim h; intros z E; clear h.
(* Goal: @ex U (fun z : U => forall (_ : In U (Carrier_of U D) y) (_ : In U (Carrier_of U D) x), and (In U (Carrier_of U D) z) (Upper_Bound U D (Couple U y x) z)) *)
   elim Couple_is_symmetric; exists z; auto.
   Qed.
   
End Lemmas_on_partial_orders.
Hint Resolve Couple_included_in_carrier.
Hint Resolve Singleton_has_lub.
Hint Resolve Empty_set_has_Upper_Bound.
Hint Resolve Empty_set_has_lub.
Hint Resolve Conditionally_complete_has_a_bottom.

