diff options
Diffstat (limited to 'theories7/Sets/Partial_Order.v')
| -rwxr-xr-x | theories7/Sets/Partial_Order.v | 100 |
1 files changed, 0 insertions, 100 deletions
diff --git a/theories7/Sets/Partial_Order.v b/theories7/Sets/Partial_Order.v deleted file mode 100755 index 759cf4e2..00000000 --- a/theories7/Sets/Partial_Order.v +++ /dev/null @@ -1,100 +0,0 @@ -(************************************************************************) -(* 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. |