diff options
Diffstat (limited to 'theories/Sets/Partial_Order.v')
| -rw-r--r-- | theories/Sets/Partial_Order.v | 116 |
1 files changed, 59 insertions, 57 deletions
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index 9924ba66..6210913c 100644 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -24,32 +24,32 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id: Partial_Order.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Partial_Order.v 9245 2006-10-17 12:53:34Z notin $ 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 := fun x y:U => Rel_of p x y /\ x <> y. - -Inductive covers (y x:U) : Prop := + 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 := fun x y:U => Rel_of p x y /\ x <> y. + + Inductive covers (y x:U) : Prop := Definition_of_covers : - Strict_Rel_of x y -> - ~ (exists z : _, Strict_Rel_of x z /\ Strict_Rel_of z y) -> - covers y x. + Strict_Rel_of x y -> + ~ (exists z : _, Strict_Rel_of x z /\ Strict_Rel_of z y) -> + covers y x. End Partial_orders. @@ -58,43 +58,45 @@ Hint Resolve Definition_of_covers: sets v62. Section Partial_order_facts. -Variable U : Type. -Variable D : PO U. - -Lemma Strict_Rel_Transitive_with_Rel : - forall x y z:U, - Strict_Rel_of U D x y -> Rel_of U D y z -> Strict_Rel_of U D x z. -unfold Strict_Rel_of at 1 in |- *. -red in |- *. -elim D; simpl in |- *. -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 in |- *; 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. + Variable U : Type. + Variable D : PO U. + + Lemma Strict_Rel_Transitive_with_Rel : + forall x y z:U, + Strict_Rel_of U D x y -> Rel_of U D y z -> Strict_Rel_of U D x z. + Proof. + unfold Strict_Rel_of at 1 in |- *. + red in |- *. + elim D; simpl in |- *. + 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 in |- *; 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 : - forall x y z:U, - Rel_of U D x y -> Strict_Rel_of U D y z -> Strict_Rel_of U D x z. -unfold Strict_Rel_of at 1 in |- *. -red in |- *. -elim D; simpl in |- *. -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 in |- *; 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_with_Rel_left : + forall x y z:U, + Rel_of U D x y -> Strict_Rel_of U D y z -> Strict_Rel_of U D x z. + Proof. + unfold Strict_Rel_of at 1 in |- *. + red in |- *. + elim D; simpl in |- *. + 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 in |- *; 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 in |- *. -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. + Lemma Strict_Rel_Transitive : Transitive U (Strict_Rel_of U D). + red in |- *. + 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.
\ No newline at end of file |