diff options
Diffstat (limited to 'theories/Sets/Relations_1_facts.v')
| -rw-r--r-- | theories/Sets/Relations_1_facts.v | 24 |
1 files changed, 11 insertions, 13 deletions
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v index f002e926..c4ede814 100644 --- a/theories/Sets/Relations_1_facts.v +++ b/theories/Sets/Relations_1_facts.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id: Relations_1_facts.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export Relations_1. Definition Complement (U:Type) (R:Relation U) : Relation U := @@ -35,8 +33,8 @@ Theorem Rsym_imp_notRsym : forall (U:Type) (R:Relation U), Symmetric U R -> Symmetric U (Complement U R). Proof. -unfold Symmetric, Complement in |- *. -intros U R H' x y H'0; red in |- *; intro H'1; apply H'0; auto with sets. +unfold Symmetric, Complement. +intros U R H' x y H'0; red; intro H'1; apply H'0; auto with sets. Qed. Theorem Equiv_from_preorder : @@ -46,8 +44,8 @@ Proof. intros U R H'; elim H'; intros H'0 H'1. apply Definition_of_equivalence. red in H'0; auto 10 with sets. -2: red in |- *; intros x y h; elim h; intros H'3 H'4; auto 10 with sets. -red in H'1; red in |- *; auto 10 with sets. +2: red; intros x y h; elim h; intros H'3 H'4; auto 10 with sets. +red in H'1; red; auto 10 with sets. intros x y z h; elim h; intros H'3 H'4; clear h. intro h; elim h; intros H'5 H'6; clear h. split; apply H'1 with y; auto 10 with sets. @@ -72,7 +70,7 @@ Hint Resolve contains_is_preorder. Theorem same_relation_is_equivalence : forall U:Type, Equivalence (Relation U) (same_relation U). Proof. -unfold same_relation at 1 in |- *; auto 10 with sets. +unfold same_relation at 1; auto 10 with sets. Qed. Hint Resolve same_relation_is_equivalence. @@ -80,14 +78,14 @@ Theorem cong_reflexive_same_relation : forall (U:Type) (R R':Relation U), same_relation U R R' -> Reflexive U R -> Reflexive U R'. Proof. -unfold same_relation in |- *; intuition. +unfold same_relation; intuition. Qed. Theorem cong_symmetric_same_relation : forall (U:Type) (R R':Relation U), same_relation U R R' -> Symmetric U R -> Symmetric U R'. Proof. - compute in |- *; intros; elim H; intros; clear H; + compute; intros; elim H; intros; clear H; apply (H3 y x (H0 x y (H2 x y H1))). (*Intuition.*) Qed. @@ -96,7 +94,7 @@ Theorem cong_antisymmetric_same_relation : forall (U:Type) (R R':Relation U), same_relation U R R' -> Antisymmetric U R -> Antisymmetric U R'. Proof. - compute in |- *; intros; elim H; intros; clear H; + compute; intros; elim H; intros; clear H; apply (H0 x y (H3 x y H1) (H3 y x H2)). (*Intuition.*) Qed. @@ -105,8 +103,8 @@ Theorem cong_transitive_same_relation : forall (U:Type) (R R':Relation U), same_relation U R R' -> Transitive U R -> Transitive U R'. Proof. -intros U R R' H' H'0; red in |- *. +intros U R R' H' H'0; red. elim H'. intros H'1 H'2 x y z H'3 H'4; apply H'2. apply H'0 with y; auto with sets. -Qed.
\ No newline at end of file +Qed. |