diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-21 01:12:06 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-21 01:12:06 +0000 |
commit | 71f380cb047a98d95b743edf98fe03bd041ea7bc (patch) | |
tree | cc8702b5f493b2bf0011eca7229e294417a03456 /theories/Sets/Partial_Order.v | |
parent | 0940e93d753c2df977e44d40f5b9d9652e881def (diff) |
theories/Sets
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@509 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Sets/Partial_Order.v')
-rwxr-xr-x | theories/Sets/Partial_Order.v | 92 |
1 files changed, 92 insertions, 0 deletions
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v new file mode 100755 index 000000000..7b0f432ba --- /dev/null +++ b/theories/Sets/Partial_Order.v @@ -0,0 +1,92 @@ +(****************************************************************************) +(* *) +(* 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. *) +(****************************************************************************) + +(* $Id$ *) + +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. +Qed. +End Partial_order_facts. |