diff options
Diffstat (limited to 'theories/Sets')
-rw-r--r-- | theories/Sets/Classical_sets.v | 18 | ||||
-rw-r--r-- | theories/Sets/Constructive_sets.v | 18 | ||||
-rw-r--r-- | theories/Sets/Cpo.v | 2 | ||||
-rw-r--r-- | theories/Sets/Ensembles.v | 2 | ||||
-rw-r--r-- | theories/Sets/Finite_sets.v | 6 | ||||
-rw-r--r-- | theories/Sets/Finite_sets_facts.v | 20 | ||||
-rw-r--r-- | theories/Sets/Image.v | 12 | ||||
-rw-r--r-- | theories/Sets/Infinite_sets.v | 14 | ||||
-rw-r--r-- | theories/Sets/Integers.v | 24 | ||||
-rw-r--r-- | theories/Sets/Multiset.v | 18 | ||||
-rw-r--r-- | theories/Sets/Partial_Order.v | 20 | ||||
-rw-r--r-- | theories/Sets/Permut.v | 2 | ||||
-rw-r--r-- | theories/Sets/Powerset.v | 28 | ||||
-rw-r--r-- | theories/Sets/Powerset_Classical_facts.v | 42 | ||||
-rw-r--r-- | theories/Sets/Powerset_facts.v | 36 | ||||
-rw-r--r-- | theories/Sets/Relations_1.v | 2 | ||||
-rw-r--r-- | theories/Sets/Relations_1_facts.v | 20 | ||||
-rw-r--r-- | theories/Sets/Relations_2.v | 2 | ||||
-rw-r--r-- | theories/Sets/Relations_2_facts.v | 14 | ||||
-rw-r--r-- | theories/Sets/Relations_3.v | 2 | ||||
-rw-r--r-- | theories/Sets/Relations_3_facts.v | 28 | ||||
-rw-r--r-- | theories/Sets/Uniset.v | 30 |
22 files changed, 180 insertions, 180 deletions
diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v index f93631c7..3129dbb1 100644 --- a/theories/Sets/Classical_sets.v +++ b/theories/Sets/Classical_sets.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -38,8 +38,8 @@ Section Ensembles_classical. elim (not_all_ex_not U (fun x:U => ~ In U A x)). intros x H; apply Inhabited_intro with x. apply NNPP; auto with sets. - red in |- *; intro. - apply NI; red in |- *. + red; intro. + apply NI; red. intros x H'; elim (H x); trivial with sets. Qed. @@ -47,7 +47,7 @@ Section Ensembles_classical. forall A:Ensemble U, A <> Empty_set U -> Inhabited U A. Proof. intros; apply not_included_empty_Inhabited. - red in |- *; auto with sets. + red; auto with sets. Qed. Lemma Inhabited_Setminus : @@ -73,7 +73,7 @@ Section Ensembles_classical. Lemma Subtract_intro : forall (A:Ensemble U) (x y:U), In U A y -> x <> y -> In U (Subtract U A x) y. Proof. - unfold Subtract at 1 in |- *; auto with sets. + unfold Subtract at 1; auto with sets. Qed. Hint Resolve Subtract_intro : sets. @@ -103,7 +103,7 @@ Section Ensembles_classical. Lemma not_SIncl_empty : forall X:Ensemble U, ~ Strict_Included U X (Empty_set U). Proof. - intro X; red in |- *; intro H'; try exact H'. + intro X; red; intro H'; try exact H'. lapply (Strict_Included_inv X (Empty_set U)); auto with sets. intro H'0; elim H'0; intros H'1 H'2; elim H'2; clear H'0. intros x H'0; elim H'0. @@ -113,10 +113,10 @@ Section Ensembles_classical. Lemma Complement_Complement : forall A:Ensemble U, Complement U (Complement U A) = A. Proof. - unfold Complement in |- *; intros; apply Extensionality_Ensembles; + unfold Complement; intros; apply Extensionality_Ensembles; auto with sets. - red in |- *; split; auto with sets. - red in |- *; intros; apply NNPP; auto with sets. + red; split; auto with sets. + red; intros; apply NNPP; auto with sets. Qed. End Ensembles_classical. diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v index e6dd8381..f559533a 100644 --- a/theories/Sets/Constructive_sets.v +++ b/theories/Sets/Constructive_sets.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -36,24 +36,24 @@ Section Ensembles_facts. Lemma Noone_in_empty : forall x:U, ~ In U (Empty_set U) x. Proof. - red in |- *; destruct 1. + red; destruct 1. Qed. Lemma Included_Empty : forall A:Ensemble U, Included U (Empty_set U) A. Proof. - intro; red in |- *. + intro; red. intros x H; elim (Noone_in_empty x); auto with sets. Qed. Lemma Add_intro1 : forall (A:Ensemble U) (x y:U), In U A y -> In U (Add U A x) y. Proof. - unfold Add at 1 in |- *; auto with sets. + unfold Add at 1; auto with sets. Qed. Lemma Add_intro2 : forall (A:Ensemble U) (x:U), In U (Add U A x) x. Proof. - unfold Add at 1 in |- *; auto with sets. + unfold Add at 1; auto with sets. Qed. Lemma Inhabited_add : forall (A:Ensemble U) (x:U), Inhabited U (Add U A x). @@ -66,7 +66,7 @@ Section Ensembles_facts. forall X:Ensemble U, Inhabited U X -> X <> Empty_set U. Proof. intros X H'; elim H'. - intros x H'0; red in |- *; intro H'1. + intros x H'0; red; intro H'1. absurd (In U X x); auto with sets. rewrite H'1; auto using Noone_in_empty with sets. Qed. @@ -78,7 +78,7 @@ Section Ensembles_facts. Lemma not_Empty_Add : forall (A:Ensemble U) (x:U), Empty_set U <> Add U A x. Proof. - intros; red in |- *; intro H; generalize (Add_not_Empty A x); auto with sets. + intros; red; intro H; generalize (Add_not_Empty A x); auto with sets. Qed. Lemma Singleton_inv : forall x y:U, In U (Singleton U x) y -> x = y. @@ -121,7 +121,7 @@ Section Ensembles_facts. forall (A B:Ensemble U) (x:U), In U A x -> ~ In U B x -> In U (Setminus U A B) x. Proof. - unfold Setminus at 1 in |- *; red in |- *; auto with sets. + unfold Setminus at 1; red; auto with sets. Qed. Lemma Strict_Included_intro : @@ -132,7 +132,7 @@ Section Ensembles_facts. Lemma Strict_Included_strict : forall X:Ensemble U, ~ Strict_Included U X X. Proof. - intro X; red in |- *; intro H'; elim H'. + intro X; red; intro H'; elim H'. intros H'0 H'1; elim H'1; auto with sets. Qed. diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index d612e71e..058eec3d 100644 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v index 58b979dd..181069d5 100644 --- a/theories/Sets/Ensembles.v +++ b/theories/Sets/Ensembles.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v index f0843675..fc940e48 100644 --- a/theories/Sets/Finite_sets.v +++ b/theories/Sets/Finite_sets.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -61,7 +61,7 @@ Section Ensembles_finis_facts. (exists x : _, X = Add U A x /\ ~ In U A x /\ cardinal U A n) end. Proof. - induction 1; simpl in |- *; auto. + induction 1; simpl; auto. exists A; exists x; auto. Qed. @@ -73,7 +73,7 @@ Section Ensembles_finis_facts. | S n => Inhabited U X end. Proof. - intros X p C; elim C; simpl in |- *; trivial with sets. + intros X p C; elim C; simpl; trivial with sets. Qed. End Ensembles_finis_facts. diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v index 350cd783..c0613637 100644 --- a/theories/Sets/Finite_sets_facts.v +++ b/theories/Sets/Finite_sets_facts.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -62,7 +62,7 @@ Section Finite_sets_facts. Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x). Proof. intro x; rewrite <- (Empty_set_zero U (Singleton U x)). - change (Finite U (Add U (Empty_set U) x)) in |- *; auto with sets. + change (Finite U (Add U (Empty_set U) x)); auto with sets. Qed. Theorem Union_preserves_Finite : @@ -134,15 +134,15 @@ Section Finite_sets_facts. cut (S (pred n) = pred (S n)). intro H'5; rewrite <- H'5. apply card_add; auto with sets. - red in |- *; intro H'6; elim H'6. + red; intro H'6; elim H'6. intros H'7 H'8; try assumption. elim H'1; auto with sets. - unfold pred at 2 in |- *; symmetry in |- *. + unfold pred at 2; symmetry . apply S_pred with (m := 0). - change (n > 0) in |- *. + change (n > 0). apply inh_card_gt_O with (X := X); auto with sets. apply Inhabited_intro with (x := x0); auto with sets. - red in |- *; intro H'3. + red; intro H'3. apply H'1. elim H'3; auto with sets. rewrite H'3; auto with sets. @@ -152,7 +152,7 @@ Section Finite_sets_facts. intro H'4; rewrite H'4; auto with sets. intros H'3 H'4; try assumption. absurd (In U (Add U X x) x0); auto with sets. - red in |- *; intro H'5; try exact H'5. + red; intro H'5; try exact H'5. lapply (Add_inv U X x x0); tauto. Qed. @@ -183,11 +183,11 @@ Section Finite_sets_facts. intros H'6 H'7; apply f_equal. apply H'0 with (Y := X0); auto with sets. apply Simplify_add with (x := x); auto with sets. - pattern x at 2 in |- *; rewrite H'6; auto with sets. + pattern x at 2; rewrite H'6; auto with sets. intros H'6 H'7. absurd (Add U X x = Add U X0 x0); auto with sets. clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2. - red in |- *; intro H'. + red; intro H'. lapply (Extension U (Add U X x) (Add U X0 x0)); auto with sets. clear H'. intro H'; red in H'. @@ -254,7 +254,7 @@ Section Finite_sets_facts. apply H'0 with (Y := X0); auto with sets arith. apply sincl_add_x with (x := x0). rewrite <- H'6; auto with sets arith. - pattern x0 at 1 in |- *; rewrite <- H'6; trivial with sets arith. + pattern x0 at 1; rewrite <- H'6; trivial with sets arith. intros H'6 H'7; red in H'5. elim H'5; intros H'8 H'9; try exact H'8; clear H'5. red in H'8. diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v index 24facb6f..bdb7c077 100644 --- a/theories/Sets/Image.v +++ b/theories/Sets/Image.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -55,7 +55,7 @@ Section Image. Proof. intros X x f. apply Extensionality_Ensembles. - split; red in |- *; intros x0 H'. + split; red; intros x0 H'. elim H'; intros. rewrite H0. elim Add_inv with U X x x1; auto using Im_def with sets. @@ -72,7 +72,7 @@ Section Image. intro f; try assumption. apply Extensionality_Ensembles. split; auto with sets. - red in |- *. + red. intros x H'; elim H'. intros x0 H'0; elim H'0; auto with sets. Qed. @@ -102,7 +102,7 @@ Section Image. forall f:U -> V, ~ injective f -> exists x : _, (exists y : _, f x = f y /\ x <> y). Proof. - unfold injective in |- *; intros f H. + unfold injective; intros f H. cut (exists x : _, ~ (forall y:U, f x = f y -> x = y)). 2: apply not_all_ex_not with (P := fun x:U => forall y:U, f x = f y -> x = y); trivial with sets. @@ -153,7 +153,7 @@ Section Image. apply cardinal_unicity with V (Add _ (Im A f) (f x)); trivial with sets. apply card_add; auto with sets. rewrite <- H1; trivial with sets. - red in |- *; intro; apply H'2. + red; intro; apply H'2. apply In_Image_elim with f; trivial with sets. Qed. @@ -180,7 +180,7 @@ Section Image. cardinal U A n -> forall n':nat, cardinal V (Im A f) n' -> n' < n -> ~ injective f. Proof. - unfold not in |- *; intros A f n CAn n' CIfn' ltn'n I. + unfold not; intros A f n CAn n' CIfn' ltn'n I. cut (n' = n). intro E; generalize ltn'n; rewrite E; exact (lt_irrefl n). apply injective_preserves_cardinal with (A := A) (f := f) (n := n); diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v index a21fe880..897046ab 100644 --- a/theories/Sets/Infinite_sets.v +++ b/theories/Sets/Infinite_sets.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -56,7 +56,7 @@ Section Infinite_sets. intros A X H' H'0. elim H'0; intros H'1 H'2. apply Strict_super_set_contains_new_element; auto with sets. - red in |- *; intro H'3; apply H'. + red; intro H'3; apply H'. rewrite <- H'3; auto with sets. Qed. @@ -76,7 +76,7 @@ Section Infinite_sets. split. apply card_add; auto with sets. cut (In U A x). - intro H'4; red in |- *; auto with sets. + intro H'4; red; auto with sets. intros x0 H'5; elim H'5; auto with sets. intros x1 H'6; elim H'6; auto with sets. elim H'3; auto with sets. @@ -91,7 +91,7 @@ Section Infinite_sets. split. apply card_add; auto with sets. elim H'2; auto with sets. - red in |- *. + red. intros x2 H'9; elim H'9; auto with sets. intros x3 H'10; elim H'10; auto with sets. elim H'2; auto with sets. @@ -167,11 +167,11 @@ Section Infinite_sets. apply ex_intro with (x := Add U x0 x1). split; [ split; [ try assumption | idtac ] | idtac ]. apply card_add; auto with sets. - red in |- *; intro H'9; try exact H'9. + red; intro H'9; try exact H'9. apply H'1. elim H'4; intros H'10 H'11; rewrite <- H'11; clear H'4; auto with sets. elim H'4; intros H'9 H'10; try exact H'9; clear H'4; auto with sets. - red in |- *; auto with sets. + red; auto with sets. intros x2 H'4; elim H'4; auto with sets. intros x3 H'11; elim H'11; auto with sets. elim H'4; intros H'9 H'10; rewrite <- H'10; clear H'4; auto with sets. @@ -235,7 +235,7 @@ Section Infinite_sets. Proof. intros A f H' H'0 H'1. apply NNPP. - red in |- *; intro H'2. + red; intro H'2. elim (Pigeonhole_bis A f); auto with sets. Qed. diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v index 2c94a2e1..4ee7496e 100644 --- a/theories/Sets/Integers.v +++ b/theories/Sets/Integers.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -49,17 +49,17 @@ Section Integers_sect. Lemma le_reflexive : Reflexive nat le. Proof. - red in |- *; auto with arith. + red; auto with arith. Qed. Lemma le_antisym : Antisymmetric nat le. Proof. - red in |- *; intros x y H H'; rewrite (le_antisym x y); auto. + red; intros x y H H'; rewrite (le_antisym x y); auto. Qed. Lemma le_trans : Transitive nat le. Proof. - red in |- *; intros; apply le_trans with y; auto. + red; intros; apply le_trans with y; auto. Qed. Lemma le_Order : Order nat le. @@ -83,7 +83,7 @@ Section Integers_sect. Lemma le_total_order : Totally_ordered nat nat_po Integers. Proof. apply Totally_ordered_definition. - simpl in |- *. + simpl. intros H' x y H'0. elim le_or_lt with (n := x) (m := y). intro H'1; left; auto with sets arith. @@ -103,7 +103,7 @@ Section Integers_sect. intros A H'0 H'1 x H'2; try assumption. elim H'1; intros x0 H'3; clear H'1. elim le_total_order. - simpl in |- *. + simpl. intro H'1; try assumption. lapply H'1; [ intro H'4; idtac | try assumption ]; auto with sets arith. generalize (H'4 x0 x). @@ -114,28 +114,28 @@ Section Integers_sect. [ intro H'5; try exact H'5; clear H'4 H'1 | intro H'5; clear H'4 H'1 ] | clear H'1 ]. exists x. - apply Upper_Bound_definition. simpl in |- *. apply triv_nat. + apply Upper_Bound_definition. simpl. apply triv_nat. intros y H'1; elim H'1. generalize le_trans. intro H'4; red in H'4. intros x1 H'6; try assumption. - apply H'4 with (y := x0). elim H'3; simpl in |- *; auto with sets arith. trivial. + apply H'4 with (y := x0). elim H'3; simpl; auto with sets arith. trivial. intros x1 H'4; elim H'4. unfold nat_po; simpl; trivial. exists x0. apply Upper_Bound_definition. unfold nat_po. simpl. apply triv_nat. intros y H'1; elim H'1. intros x1 H'4; try assumption. - elim H'3; simpl in |- *; auto with sets arith. + elim H'3; simpl; auto with sets arith. intros x1 H'4; elim H'4; auto with sets arith. - red in |- *. + red. intros x1 H'1; elim H'1; apply triv_nat. Qed. Lemma Integers_has_no_ub : ~ (exists m : nat, Upper_Bound nat nat_po Integers m). Proof. - red in |- *; intro H'; elim H'. + red; intro H'; elim H'. intros x H'0. elim H'0; intros H'1 H'2. cut (In nat Integers (S x)). @@ -150,7 +150,7 @@ Section Integers_sect. Lemma Integers_infinite : ~ Finite nat Integers. Proof. generalize Integers_has_no_ub. - intro H'; red in |- *; intro H'0; try exact H'0. + intro H'; red; intro H'0; try exact H'0. apply H'. apply Finite_subset_has_lub; auto with sets arith. Qed. diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index 5f21335f..1d0abab8 100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -42,14 +42,14 @@ Section multiset_defs. Lemma meq_trans : forall x y z:multiset, meq x y -> meq y z -> meq x z. Proof. - unfold meq in |- *. + unfold meq. destruct x; destruct y; destruct z. intros; rewrite H; auto. Qed. Lemma meq_sym : forall x y:multiset, meq x y -> meq y x. Proof. - unfold meq in |- *. + unfold meq. destruct x; destruct y; auto. Qed. @@ -59,12 +59,12 @@ Section multiset_defs. Lemma munion_empty_left : forall x:multiset, meq x (munion EmptyBag x). Proof. - unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto. + unfold meq; unfold munion; simpl; auto. Qed. Lemma munion_empty_right : forall x:multiset, meq x (munion x EmptyBag). Proof. - unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto. + unfold meq; unfold munion; simpl; auto. Qed. @@ -72,21 +72,21 @@ Section multiset_defs. Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x). Proof. - unfold meq in |- *; unfold multiplicity in |- *; unfold munion in |- *. + unfold meq; unfold multiplicity; unfold munion. destruct x; destruct y; auto with arith. Qed. Lemma munion_ass : forall x y z:multiset, meq (munion (munion x y) z) (munion x (munion y z)). Proof. - unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *. + unfold meq; unfold munion; unfold multiplicity. destruct x; destruct y; destruct z; auto with arith. Qed. Lemma meq_left : forall x y z:multiset, meq x y -> meq (munion x z) (munion y z). Proof. - unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *. + unfold meq; unfold munion; unfold multiplicity. destruct x; destruct y; destruct z. intros; elim H; auto with arith. Qed. @@ -94,7 +94,7 @@ Section multiset_defs. Lemma meq_right : forall x y z:multiset, meq x y -> meq (munion z x) (munion z y). Proof. - unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *. + unfold meq; unfold munion; unfold multiplicity. destruct x; destruct y; destruct z. intros; elim H; auto. Qed. diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index a319b983..054164da 100644 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -63,13 +63,13 @@ Section Partial_order_facts. 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 |- *. + unfold Strict_Rel_of at 1. + 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 in |- *; intro H'6. + 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. @@ -79,20 +79,20 @@ Section Partial_order_facts. 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 |- *. + unfold Strict_Rel_of at 1. + 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 in |- *; intro H'6. + 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 in |- *. + 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 ]. diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v index e28a1264..5523f64c 100644 --- a/theories/Sets/Permut.v +++ b/theories/Sets/Permut.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v index f8b24e74..cdbeaf7b 100644 --- a/theories/Sets/Powerset.v +++ b/theories/Sets/Powerset.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -39,7 +39,7 @@ Inductive Power_set (A:Ensemble U) : Ensemble (Ensemble U) := Hint Resolve Definition_of_Power_set. Theorem Empty_set_minimal : forall X:Ensemble U, Included U (Empty_set U) X. -intro X; red in |- *. +intro X; red. intros x H'; elim H'. Qed. Hint Resolve Empty_set_minimal. @@ -79,7 +79,7 @@ Lemma Strict_inclusion_is_transitive_with_inclusion : Strict_Included U x y -> Included U y z -> Strict_Included U x z. intros x y z H' H'0; try assumption. elim Strict_Rel_is_Strict_Included. -unfold contains in |- *. +unfold contains. intros H'1 H'2; try assumption. apply H'1. apply Strict_Rel_Transitive_with_Rel with (y := y); auto with sets. @@ -90,7 +90,7 @@ Lemma Strict_inclusion_is_transitive_with_inclusion_left : Included U x y -> Strict_Included U y z -> Strict_Included U x z. intros x y z H' H'0; try assumption. elim Strict_Rel_is_Strict_Included. -unfold contains in |- *. +unfold contains. intros H'1 H'2; try assumption. apply H'1. apply Strict_Rel_Transitive_with_Rel_left with (y := y); auto with sets. @@ -105,14 +105,14 @@ Qed. Theorem Empty_set_is_Bottom : forall A:Ensemble U, Bottom (Ensemble U) (Power_set_PO A) (Empty_set U). -intro A; apply Bottom_definition; simpl in |- *; auto with sets. +intro A; apply Bottom_definition; simpl; auto with sets. Qed. Hint Resolve Empty_set_is_Bottom. Theorem Union_minimal : forall a b X:Ensemble U, Included U a X -> Included U b X -> Included U (Union U a b) X. -intros a b X H' H'0; red in |- *. +intros a b X H' H'0; red. intros x H'1; elim H'1; auto with sets. Qed. Hint Resolve Union_minimal. @@ -133,13 +133,13 @@ Qed. Theorem Intersection_decreases_l : forall a b:Ensemble U, Included U (Intersection U a b) a. -intros a b; red in |- *. +intros a b; red. intros x H'; elim H'; auto with sets. Qed. Theorem Intersection_decreases_r : forall a b:Ensemble U, Included U (Intersection U a b) b. -intros a b; red in |- *. +intros a b; red. intros x H'; elim H'; auto with sets. Qed. Hint Resolve Union_increases_l Union_increases_r Intersection_decreases_l @@ -151,10 +151,10 @@ Theorem Union_is_Lub : Included U b A -> Lub (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b) (Union U a b). intros A a b H' H'0. -apply Lub_definition; simpl in |- *. -apply Upper_Bound_definition; simpl in |- *; auto with sets. +apply Lub_definition; simpl. +apply Upper_Bound_definition; simpl; auto with sets. intros y H'1; elim H'1; auto with sets. -intros y H'1; elim H'1; simpl in |- *; auto with sets. +intros y H'1; elim H'1; simpl; auto with sets. Qed. Theorem Intersection_is_Glb : @@ -164,13 +164,13 @@ Theorem Intersection_is_Glb : Glb (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b) (Intersection U a b). intros A a b H' H'0. -apply Glb_definition; simpl in |- *. -apply Lower_Bound_definition; simpl in |- *; auto with sets. +apply Glb_definition; simpl. +apply Lower_Bound_definition; simpl; auto with sets. apply Definition_of_Power_set. generalize Inclusion_is_transitive; intro IT; red in IT; apply IT with a; auto with sets. intros y H'1; elim H'1; auto with sets. -intros y H'1; elim H'1; simpl in |- *; auto with sets. +intros y H'1; elim H'1; simpl; auto with sets. Qed. End The_power_set_partial_order. diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v index 09fc2094..d24e931d 100644 --- a/theories/Sets/Powerset_Classical_facts.v +++ b/theories/Sets/Powerset_Classical_facts.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -44,13 +44,13 @@ Section Sets_as_an_algebra. ~ In U A x -> Strict_Included U (Add U A x) (Add U B x) -> Strict_Included U A B. Proof. - intros A B x H' H'0; red in |- *. + intros A B x H' H'0; red. lapply (Strict_Included_inv U (Add U A x) (Add U B x)); auto with sets. clear H'0; intro H'0; split. apply incl_add_x with (x := x); tauto. elim H'0; intros H'1 H'2; elim H'2; clear H'0 H'2. intros x0 H'0. - red in |- *; intro H'2. + red; intro H'2. elim H'0; clear H'0. rewrite <- H'2; auto with sets. Qed. @@ -58,7 +58,7 @@ Section Sets_as_an_algebra. Lemma incl_soustr_in : forall (X:Ensemble U) (x:U), In U X x -> Included U (Subtract U X x) X. Proof. - intros X x H'; red in |- *. + intros X x H'; red. intros x0 H'0; elim H'0; auto with sets. Qed. @@ -66,7 +66,7 @@ Section Sets_as_an_algebra. forall (X Y:Ensemble U) (x:U), Included U X Y -> Included U (Subtract U X x) (Subtract U Y x). Proof. - intros X Y x H'; red in |- *. + intros X Y x H'; red. intros x0 H'0; elim H'0. intros H'1 H'2. apply Subtract_intro; auto with sets. @@ -75,7 +75,7 @@ Section Sets_as_an_algebra. Lemma incl_soustr_add_l : forall (X:Ensemble U) (x:U), Included U (Subtract U (Add U X x) x) X. Proof. - intros X x; red in |- *. + intros X x; red. intros x0 H'; elim H'; auto with sets. intro H'0; elim H'0; auto with sets. intros t H'1 H'2; elim H'2; auto with sets. @@ -85,10 +85,10 @@ Section Sets_as_an_algebra. forall (X:Ensemble U) (x:U), ~ In U X x -> Included U X (Subtract U (Add U X x) x). Proof. - intros X x H'; red in |- *. + intros X x H'; red. intros x0 H'0; try assumption. apply Subtract_intro; auto with sets. - red in |- *; intro H'1; apply H'; rewrite H'1; auto with sets. + red; intro H'1; apply H'; rewrite H'1; auto with sets. Qed. Hint Resolve incl_soustr_add_r: sets v62. @@ -96,7 +96,7 @@ Section Sets_as_an_algebra. forall (X:Ensemble U) (x:U), In U X x -> Included U X (Add U (Subtract U X x) x). Proof. - intros X x H'; red in |- *. + intros X x H'; red. intros x0 H'0; try assumption. elim (classic (x = x0)); intro K; auto with sets. elim K; auto with sets. @@ -106,7 +106,7 @@ Section Sets_as_an_algebra. forall (X:Ensemble U) (x:U), In U X x -> Included U (Add U (Subtract U X x) x) X. Proof. - intros X x H'; red in |- *. + intros X x H'; red. intros x0 H'0; elim H'0; auto with sets. intros y H'1; elim H'1; auto with sets. intros t H'1; try assumption. @@ -118,7 +118,7 @@ Section Sets_as_an_algebra. x <> y -> Subtract U (Add U X x) y = Add U (Subtract U X y) x. Proof. intros X x y H'; apply Extensionality_Ensembles. - split; red in |- *. + split; red. intros x0 H'0; elim H'0; auto with sets. intro H'1; elim H'1. intros u H'2 H'3; try assumption. @@ -146,7 +146,7 @@ Section Sets_as_an_algebra. apply H'4 with (y := Y); auto using add_soustr_2 with sets. red in H'0. elim H'0; intros H'1 H'2; try exact H'1; clear H'0. (* PB *) - red in |- *; intro H'0; apply H'2. + red; intro H'0; apply H'2. rewrite H'0; auto 8 using add_soustr_xy, add_soustr_1, add_soustr_2 with sets. Qed. @@ -177,7 +177,7 @@ Section Sets_as_an_algebra. exists (Subtract U X x). split; auto using incl_soustr_in, add_soustr_xy, add_soustr_1, add_soustr_2 with sets. red in H'0. - red in |- *. + red. intros x0 H'2; try assumption. lapply (Subtract_inv U X x x0); auto with sets. intro H'3; elim H'3; intros K K'; clear H'3. @@ -189,7 +189,7 @@ Section Sets_as_an_algebra. elim K'; auto with sets. intro H'1; left; try assumption. red in H'0. - red in |- *. + red. intros x0 H'2; try assumption. lapply (H'0 x0); auto with sets. intro H'3; try assumption. @@ -207,7 +207,7 @@ Section Sets_as_an_algebra. (forall z:Ensemble U, Included U x z -> Included U z y -> x = z \/ z = y). Proof. intros A x y H'; elim H'. - unfold Strict_Rel_of in |- *; simpl in |- *. + unfold Strict_Rel_of; simpl. intros H'0 H'1; split; [ auto with sets | idtac ]. intros z H'2 H'3; try assumption. elim (classic (x = z)); auto with sets. @@ -227,11 +227,11 @@ Section Sets_as_an_algebra. Proof. intros A a H' x H'0 H'1; try assumption. apply setcover_intro; auto with sets. - red in |- *. - split; [ idtac | red in |- *; intro H'2; try exact H'2 ]; auto with sets. + red. + split; [ idtac | red; intro H'2; try exact H'2 ]; auto with sets. apply H'1. rewrite H'2; auto with sets. - red in |- *; intro H'2; elim H'2; clear H'2. + red; intro H'2; elim H'2; clear H'2. intros z H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2. lapply (Strict_Included_inv U a z); auto with sets; clear H'3. intro H'2; elim H'2; intros H'3 H'5; elim H'5; clear H'2 H'5. @@ -249,7 +249,7 @@ Section Sets_as_an_algebra. red in K. elim K; intros H'11 H'12; apply H'12; clear K; auto with sets. rewrite H'15. - red in |- *. + red. intros x1 H'10; elim H'10; auto with sets. intros x2 H'11; elim H'11; auto with sets. Qed. @@ -275,11 +275,11 @@ Section Sets_as_an_algebra. elim (H'7 (Add U a x)); auto with sets. intro H'1. absurd (a = Add U a x); auto with sets. - red in |- *; intro H'8; try exact H'8. + red; intro H'8; try exact H'8. apply H'3. rewrite H'8; auto with sets. auto with sets. - red in |- *. + red. intros x0 H'1; elim H'1; auto with sets. intros x1 H'8; elim H'8; auto with sets. split; [ idtac | try assumption ]. diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v index f756f985..58e3f44d 100644 --- a/theories/Sets/Powerset_facts.v +++ b/theories/Sets/Powerset_facts.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -42,7 +42,7 @@ Section Sets_as_an_algebra. Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x. Proof. - unfold Add at 1 in |- *; auto using Empty_set_zero with sets. + unfold Add at 1; auto using Empty_set_zero with sets. Qed. Lemma less_than_empty : @@ -76,7 +76,7 @@ Section Sets_as_an_algebra. Theorem Couple_as_union : forall x y:U, Union U (Singleton U x) (Singleton U y) = Couple U x y. Proof. - intros x y; apply Extensionality_Ensembles; split; red in |- *. + intros x y; apply Extensionality_Ensembles; split; red. intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets). intros x0 H'; elim H'; auto with sets. Qed. @@ -86,7 +86,7 @@ Section Sets_as_an_algebra. Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z) = Triple U x y z. Proof. - intros x y z; apply Extensionality_Ensembles; split; red in |- *. + intros x y z; apply Extensionality_Ensembles; split; red. intros x0 H'; elim H'. intros x1 H'0; elim H'0; (intros x2 H'1; elim H'1; auto with sets). intros x1 H'0; elim H'0; auto with sets. @@ -114,7 +114,7 @@ Section Sets_as_an_algebra. Proof. intros A B. apply Extensionality_Ensembles. - split; red in |- *; intros x H'; elim H'; auto with sets. + split; red; intros x H'; elim H'; auto with sets. Qed. Theorem Distributivity : @@ -124,7 +124,7 @@ Section Sets_as_an_algebra. Proof. intros A B C. apply Extensionality_Ensembles. - split; red in |- *; intros x H'. + split; red; intros x H'. elim H'. intros x0 H'0 H'1; generalize H'0. elim H'1; auto with sets. @@ -138,7 +138,7 @@ Section Sets_as_an_algebra. Proof. intros A B C. apply Extensionality_Ensembles. - split; red in |- *; intros x H'. + split; red; intros x H'. elim H'; auto with sets. intros x0 H'0; elim H'0; auto with sets. elim H'. @@ -151,15 +151,15 @@ Section Sets_as_an_algebra. Theorem Union_add : forall (A B:Ensemble U) (x:U), Add U (Union U A B) x = Union U A (Add U B x). Proof. - unfold Add in |- *; auto using Union_associative with sets. + unfold Add; auto using Union_associative with sets. Qed. Theorem Non_disjoint_union : forall (X:Ensemble U) (x:U), In U X x -> Add U X x = X. Proof. - intros X x H'; unfold Add in |- *. - apply Extensionality_Ensembles; red in |- *. - split; red in |- *; auto with sets. + intros X x H'; unfold Add. + apply Extensionality_Ensembles; red. + split; red; auto with sets. intros x0 H'0; elim H'0; auto with sets. intros t H'1; elim H'1; auto with sets. Qed. @@ -167,12 +167,12 @@ Section Sets_as_an_algebra. Theorem Non_disjoint_union' : forall (X:Ensemble U) (x:U), ~ In U X x -> Subtract U X x = X. Proof. - intros X x H'; unfold Subtract in |- *. + intros X x H'; unfold Subtract. apply Extensionality_Ensembles. - split; red in |- *; auto with sets. + split; red; auto with sets. intros x0 H'0; elim H'0; auto with sets. intros x0 H'0; apply Setminus_intro; auto with sets. - red in |- *; intro H'1; elim H'1. + red; intro H'1; elim H'1. lapply (Singleton_inv U x x0); auto with sets. intro H'4; apply H'; rewrite H'4; auto with sets. Qed. @@ -186,7 +186,7 @@ Section Sets_as_an_algebra. forall (A B:Ensemble U) (x:U), Included U A B -> Included U (Add U A x) (Add U B x). Proof. - intros A B x H'; red in |- *; auto with sets. + intros A B x H'; red; auto with sets. intros x0 H'0. lapply (Add_inv U A x x0); auto with sets. intro H'1; elim H'1; @@ -198,7 +198,7 @@ Section Sets_as_an_algebra. forall (A B:Ensemble U) (x:U), ~ In U A x -> Included U (Add U A x) (Add U B x) -> Included U A B. Proof. - unfold Included in |- *. + unfold Included. intros A B x H' H'0 x0 H'1. lapply (H'0 x0); auto with sets. intro H'2; lapply (Add_inv U B x x0); auto with sets. @@ -212,7 +212,7 @@ Section Sets_as_an_algebra. forall (A:Ensemble U) (x y:U), Add U (Add U A x) y = Add U (Add U A y) x. Proof. intros A x y. - unfold Add in |- *. + unfold Add. rewrite (Union_associative A (Singleton U x) (Singleton U y)). rewrite (Union_commutative (Singleton U x) (Singleton U y)). rewrite <- (Union_associative A (Singleton U y) (Singleton U x)); @@ -234,7 +234,7 @@ Section Sets_as_an_algebra. Proof. intros A B x y H'; try assumption. rewrite <- (Union_add (Add U A x) B y). - unfold Add at 4 in |- *. + unfold Add at 4. rewrite (Union_commutative A (Singleton U x)). rewrite Union_associative. rewrite (Union_absorbs A B H'). diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v index a7fbb53d..229ef592 100644 --- a/theories/Sets/Relations_1.v +++ b/theories/Sets/Relations_1.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v index 0c8329dd..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-2010 *) +(* <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 *) @@ -33,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 : @@ -44,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. @@ -70,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. @@ -78,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. @@ -94,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. @@ -103,7 +103,7 @@ 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. diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v index e7a69c99..a371f316 100644 --- a/theories/Sets/Relations_2.v +++ b/theories/Sets/Relations_2.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v index 89b98c1f..676fd719 100644 --- a/theories/Sets/Relations_2_facts.v +++ b/theories/Sets/Relations_2_facts.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -43,13 +43,13 @@ Qed. Theorem Rstar_contains_R : forall (U:Type) (R:Relation U), contains U (Rstar U R) R. Proof. -intros U R; red in |- *; intros x y H'; apply Rstar_n with y; auto with sets. +intros U R; red; intros x y H'; apply Rstar_n with y; auto with sets. Qed. Theorem Rstar_contains_Rplus : forall (U:Type) (R:Relation U), contains U (Rstar U R) (Rplus U R). Proof. -intros U R; red in |- *. +intros U R; red. intros x y H'; elim H'. generalize Rstar_contains_R; intro T; red in T; auto with sets. intros x0 y0 z H'0 H'1 H'2; apply Rstar_n with y0; auto with sets. @@ -58,7 +58,7 @@ Qed. Theorem Rstar_transitive : forall (U:Type) (R:Relation U), Transitive U (Rstar U R). Proof. -intros U R; red in |- *. +intros U R; red. intros x y z H'; elim H'; auto with sets. intros x0 y0 z0 H'0 H'1 H'2 H'3; apply Rstar_n with y0; auto with sets. Qed. @@ -75,7 +75,7 @@ Theorem Rstar_equiv_Rstar1 : forall (U:Type) (R:Relation U), same_relation U (Rstar U R) (Rstar1 U R). Proof. generalize Rstar_contains_R; intro T; red in T. -intros U R; unfold same_relation, contains in |- *. +intros U R; unfold same_relation, contains. split; intros x y H'; elim H'; auto with sets. generalize Rstar_transitive; intro T1; red in T1. intros x0 y0 z H'0 H'1 H'2 H'3; apply T1 with y0; auto with sets. @@ -85,7 +85,7 @@ Qed. Theorem Rsym_imp_Rstarsym : forall (U:Type) (R:Relation U), Symmetric U R -> Symmetric U (Rstar U R). Proof. -intros U R H'; red in |- *. +intros U R H'; red. intros x y H'0; elim H'0; auto with sets. intros x0 y0 z H'1 H'2 H'3. generalize Rstar_transitive; intro T1; red in T1. @@ -97,7 +97,7 @@ Theorem Sstar_contains_Rstar : forall (U:Type) (R S:Relation U), contains U (Rstar U S) R -> contains U (Rstar U S) (Rstar U R). Proof. -unfold contains in |- *. +unfold contains. intros U R S H' x y H'0; elim H'0; auto with sets. generalize Rstar_transitive; intro T1; red in T1. intros x0 y0 z H'1 H'2 H'3; apply T1 with y0; auto with sets. diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v index 51092f7a..6d1853e2 100644 --- a/theories/Sets/Relations_3.v +++ b/theories/Sets/Relations_3.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v index 8ac6e7fb..a63f7c80 100644 --- a/theories/Sets/Relations_3_facts.v +++ b/theories/Sets/Relations_3_facts.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -33,7 +33,7 @@ Require Export Relations_3. Theorem Rstar_imp_coherent : forall (U:Type) (R:Relation U) (x y:U), Rstar U R x y -> coherent U R x y. Proof. -intros U R x y H'; red in |- *. +intros U R x y H'; red. exists y; auto with sets. Qed. Hint Resolve Rstar_imp_coherent. @@ -41,8 +41,8 @@ Hint Resolve Rstar_imp_coherent. Theorem coherent_symmetric : forall (U:Type) (R:Relation U), Symmetric U (coherent U R). Proof. -unfold coherent at 1 in |- *. -intros U R; red in |- *. +unfold coherent at 1. +intros U R; red. intros x y H'; elim H'. intros z H'0; exists z; tauto. Qed. @@ -50,9 +50,9 @@ Qed. Theorem Strong_confluence : forall (U:Type) (R:Relation U), Strongly_confluent U R -> Confluent U R. Proof. -intros U R H'; red in |- *. -intro x; red in |- *; intros a b H'0. -unfold coherent at 1 in |- *. +intros U R H'; red. +intro x; red; intros a b H'0. +unfold coherent at 1. generalize b; clear b. elim H'0; clear H'0. intros x0 b H'1; exists b; auto with sets. @@ -75,9 +75,9 @@ Qed. Theorem Strong_confluence_direct : forall (U:Type) (R:Relation U), Strongly_confluent U R -> Confluent U R. Proof. -intros U R H'; red in |- *. -intro x; red in |- *; intros a b H'0. -unfold coherent at 1 in |- *. +intros U R H'; red. +intro x; red; intros a b H'0. +unfold coherent at 1. generalize b; clear b. elim H'0; clear H'0. intros x0 b H'1; exists b; auto with sets. @@ -111,7 +111,7 @@ Theorem Noetherian_contains_Noetherian : forall (U:Type) (R R':Relation U), Noetherian U R -> contains U R R' -> Noetherian U R'. Proof. -unfold Noetherian at 2 in |- *. +unfold Noetherian at 2. intros U R R' H' H'0 x. elim (H' x); auto with sets. Qed. @@ -120,8 +120,8 @@ Theorem Newman : forall (U:Type) (R:Relation U), Noetherian U R -> Locally_confluent U R -> Confluent U R. Proof. -intros U R H' H'0; red in |- *; intro x. -elim (H' x); unfold confluent in |- *. +intros U R H' H'0; red; intro x. +elim (H' x); unfold confluent. intros x0 H'1 H'2 y z H'3 H'4. generalize (Rstar_cases U R x0 y); intro h; lapply h; [ intro h0; elim h0; @@ -163,7 +163,7 @@ generalize (H'2 v); intro h; lapply h; | clear h h0 ] | clear h h0 ] | clear h ]; auto with sets. -red in |- *; (exists z1; split); auto with sets. +red; (exists z1; split); auto with sets. apply T with y1; auto with sets. apply T with t; auto with sets. Qed. diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index bf1aaf8d..6e38b5e5 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -51,37 +51,37 @@ Hint Unfold seq. Lemma leb_refl : forall b:bool, leb b b. Proof. -destruct b; simpl in |- *; auto. +destruct b; simpl; auto. Qed. Hint Resolve leb_refl. Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2. Proof. -unfold incl in |- *; intros s1 s2 E a; elim (E a); auto. +unfold incl; intros s1 s2 E a; elim (E a); auto. Qed. Lemma incl_right : forall s1 s2:uniset, seq s1 s2 -> incl s2 s1. Proof. -unfold incl in |- *; intros s1 s2 E a; elim (E a); auto. +unfold incl; intros s1 s2 E a; elim (E a); auto. Qed. Lemma seq_refl : forall x:uniset, seq x x. Proof. -destruct x; unfold seq in |- *; auto. +destruct x; unfold seq; auto. Qed. Hint Resolve seq_refl. Lemma seq_trans : forall x y z:uniset, seq x y -> seq y z -> seq x z. Proof. -unfold seq in |- *. -destruct x; destruct y; destruct z; simpl in |- *; intros. +unfold seq. +destruct x; destruct y; destruct z; simpl; intros. rewrite H; auto. Qed. Lemma seq_sym : forall x y:uniset, seq x y -> seq y x. Proof. -unfold seq in |- *. -destruct x; destruct y; simpl in |- *; auto. +unfold seq. +destruct x; destruct y; simpl; auto. Qed. (** uniset union *) @@ -90,20 +90,20 @@ Definition union (m1 m2:uniset) := Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x). Proof. -unfold seq in |- *; unfold union in |- *; simpl in |- *; auto. +unfold seq; unfold union; simpl; auto. Qed. Hint Resolve union_empty_left. Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset). Proof. -unfold seq in |- *; unfold union in |- *; simpl in |- *. +unfold seq; unfold union; simpl. intros x a; rewrite (orb_b_false (charac x a)); auto. Qed. Hint Resolve union_empty_right. Lemma union_comm : forall x y:uniset, seq (union x y) (union y x). Proof. -unfold seq in |- *; unfold charac in |- *; unfold union in |- *. +unfold seq; unfold charac; unfold union. destruct x; destruct y; auto with bool. Qed. Hint Resolve union_comm. @@ -111,14 +111,14 @@ Hint Resolve union_comm. Lemma union_ass : forall x y z:uniset, seq (union (union x y) z) (union x (union y z)). Proof. -unfold seq in |- *; unfold union in |- *; unfold charac in |- *. +unfold seq; unfold union; unfold charac. destruct x; destruct y; destruct z; auto with bool. Qed. Hint Resolve union_ass. Lemma seq_left : forall x y z:uniset, seq x y -> seq (union x z) (union y z). Proof. -unfold seq in |- *; unfold union in |- *; unfold charac in |- *. +unfold seq; unfold union; unfold charac. destruct x; destruct y; destruct z. intros; elim H; auto. Qed. @@ -126,7 +126,7 @@ Hint Resolve seq_left. Lemma seq_right : forall x y z:uniset, seq x y -> seq (union z x) (union z y). Proof. -unfold seq in |- *; unfold union in |- *; unfold charac in |- *. +unfold seq; unfold union; unfold charac. destruct x; destruct y; destruct z. intros; elim H; auto. Qed. |