diff options
Diffstat (limited to 'theories/Sets/Partial_Order.v')
-rwxr-xr-x | theories/Sets/Partial_Order.v | 102 |
1 files changed, 51 insertions, 51 deletions
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index f3d692b85..5ef6bc9b0 100755 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -30,71 +30,71 @@ Require Export Ensembles. Require Export Relations_1. Section Partial_orders. -Variable U: Type. +Variable U : Type. -Definition Carrier := (Ensemble U). +Definition Carrier := Ensemble U. -Definition Rel := (Relation 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. +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. +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) -> - ~ (EXT z | (Strict_Rel_of x z) /\ (Strict_Rel_of z y)) -> - (covers y x). +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. End Partial_orders. -Hints Unfold Carrier_of Rel_of Strict_Rel_of : sets v62. -Hints Resolve Definition_of_covers : sets v62. +Hint Unfold Carrier_of Rel_of Strict_Rel_of: sets v62. +Hint Resolve Definition_of_covers: sets v62. Section Partial_order_facts. -Variable U:Type. -Variable D:(PO U). +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. +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. -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. +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: (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 ]. +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. +End Partial_order_facts.
\ No newline at end of file |