diff options
Diffstat (limited to 'theories7/Sets/Partial_Order.v')
| -rwxr-xr-x | theories7/Sets/Partial_Order.v | 100 |
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. |