1 files changed, 100 insertions, 0 deletions
diff --git a/theories7/Sets/Partial_Order.v b/theories7/Sets/Partial_Order.v
new file mode 100755
index 00000000..759cf4e2
--- /dev/null
+++ b/theories7/Sets/Partial_Order.v
@@ -0,0 +1,100 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(****************************************************************************)
+(*                                                                          *)
+(*                         Naive Set Theory in Coq                          *)
+(*                                                                          *)
+(*                     INRIA                        INRIA                   *)
+(*              Rocquencourt                        Sophia-Antipolis        *)
+(*                                                                          *)
+(*                                 Coq V6.1                                 *)
+(*									    *)
+(*			         Gilles Kahn 				    *)
+(*				 Gerard Huet				    *)
+(*									    *)
+(*									    *)
+(*                                                                          *)
+(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks  *)
+(* to the Newton Institute for providing an exceptional work environment    *)
+(* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
+(****************************************************************************)
+
+(*i $Id: Partial_Order.v,v 1.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*)
+
+Require Export Ensembles.
+Require Export Relations_1.
+
+Section Partial_orders.
+Variable U: Type.
+
+Definition Carrier :=  (Ensemble U).
+
+Definition Rel :=  (Relation U).
+
+Record PO : Type := Definition_of_PO {
+   Carrier_of: (Ensemble U);
+   Rel_of: (Relation U);
+   PO_cond1: (Inhabited U Carrier_of);
+   PO_cond2: (Order U Rel_of) }.
+Variable p: PO.
+
+Definition Strict_Rel_of : Rel :=  [x, y: U] (Rel_of p x y) /\ ~ x == y.
+
+Inductive covers [y, x:U]: Prop :=
+      Definition_of_covers:
+      (Strict_Rel_of x y) -> 
+          ~ (EXT z | (Strict_Rel_of x z) /\ (Strict_Rel_of z y)) -> 
+          (covers y x).
+
+End Partial_orders.
+
+Hints Unfold Carrier_of Rel_of  Strict_Rel_of : sets v62.
+Hints Resolve Definition_of_covers : sets v62.
+
+
+Section Partial_order_facts.
+Variable U:Type.
+Variable D:(PO U).
+
+Lemma Strict_Rel_Transitive_with_Rel:
+  (x:U) (y:U) (z:U) (Strict_Rel_of U D x y) -> (Rel_of U D y z) ->
+  (Strict_Rel_of U D x z).
+Unfold 1 Strict_Rel_of.
+Red.
+Elim D; Simpl.
+Intros C R H' H'0; Elim H'0.
+Intros H'1 H'2 H'3 x y z H'4 H'5; Split.
+Apply H'2 with y := y; Tauto.
+Red; Intro H'6.
+Elim H'4; Intros H'7 H'8; Apply H'8; Clear H'4.
+Apply H'3; Auto.
+Rewrite H'6; Tauto.
+Qed.
+
+Lemma Strict_Rel_Transitive_with_Rel_left:
+  (x:U) (y:U) (z:U) (Rel_of U D x y) -> (Strict_Rel_of U D y z) ->
+  (Strict_Rel_of U D x z).
+Unfold 1 Strict_Rel_of.
+Red.
+Elim D; Simpl.
+Intros C R H' H'0; Elim H'0.
+Intros H'1 H'2 H'3 x y z H'4 H'5; Split.
+Apply H'2 with y := y; Tauto.
+Red; Intro H'6.
+Elim H'5; Intros H'7 H'8; Apply H'8; Clear H'5.
+Apply H'3; Auto.
+Rewrite <- H'6; Auto.
+Qed.
+
+Lemma Strict_Rel_Transitive: (Transitive U (Strict_Rel_of U D)).
+Red.
+Intros x y z H' H'0.
+Apply Strict_Rel_Transitive_with_Rel with y := y; 
+  [ Intuition | Unfold Strict_Rel_of in H' H'0; Intuition ].
+Qed.
+End Partial_order_facts.