diff options
author | Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
commit | e0d682ec25282a348d35c5b169abafec48555690 (patch) | |
tree | 1a46f0142a85df553388c932110793881f3af52f /theories/Wellfounded | |
parent | 86535d84cc3cffeee1dcd8545343f234e7285530 (diff) |
Imported Upstream version 8.4dfsgupstream/8.4dfsg
Diffstat (limited to 'theories/Wellfounded')
-rw-r--r-- | theories/Wellfounded/Disjoint_Union.v | 4 | ||||
-rw-r--r-- | theories/Wellfounded/Inclusion.v | 4 | ||||
-rw-r--r-- | theories/Wellfounded/Inverse_Image.v | 6 | ||||
-rw-r--r-- | theories/Wellfounded/Lexicographic_Exponentiation.v | 28 | ||||
-rw-r--r-- | theories/Wellfounded/Lexicographic_Product.v | 10 | ||||
-rw-r--r-- | theories/Wellfounded/Transitive_Closure.v | 6 | ||||
-rw-r--r-- | theories/Wellfounded/Union.v | 6 | ||||
-rw-r--r-- | theories/Wellfounded/Well_Ordering.v | 8 | ||||
-rw-r--r-- | theories/Wellfounded/Wellfounded.v | 2 |
9 files changed, 37 insertions, 37 deletions
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v index f5daa301..8f5c0957 100644 --- a/theories/Wellfounded/Disjoint_Union.v +++ b/theories/Wellfounded/Disjoint_Union.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 *) @@ -41,7 +41,7 @@ Section Wf_Disjoint_Union. well_founded leA -> well_founded leB -> well_founded Le_AsB. Proof. intros. - unfold well_founded in |- *. + unfold well_founded. destruct a as [a| b]. apply (acc_A_sum a). apply (H a). diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v index 1c83c481..c7cc29b5 100644 --- a/theories/Wellfounded/Inclusion.v +++ b/theories/Wellfounded/Inclusion.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 *) @@ -24,7 +24,7 @@ Section WfInclusion. Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1. Proof. - unfold well_founded in |- *; auto with sets. + unfold well_founded; auto with sets. Qed. End WfInclusion. diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v index 27a1c381..e38b2157 100644 --- a/theories/Wellfounded/Inverse_Image.v +++ b/theories/Wellfounded/Inverse_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 *) @@ -31,7 +31,7 @@ Section Inverse_Image. Theorem wf_inverse_image : well_founded R -> well_founded Rof. Proof. - red in |- *; intros; apply Acc_inverse_image; auto. + red; intros; apply Acc_inverse_image; auto. Qed. Variable F : A -> B -> Prop. @@ -49,7 +49,7 @@ Section Inverse_Image. Theorem wf_inverse_rel : well_founded R -> well_founded RoF. Proof. - red in |- *; constructor; intros. + red; constructor; intros. case H0; intros. apply (Acc_inverse_rel x); auto. Qed. diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index 6d5b663b..13db01a3 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.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,11 +36,11 @@ Section Wf_Lexicographic_Exponentiation. Proof. simple induction x. simple induction z. - simpl in |- *; intros H. + simpl; intros H. inversion_clear H. - simpl in |- *; intros; apply (Lt_nil A leA). + simpl; intros; apply (Lt_nil A leA). intros a l HInd. - simpl in |- *. + simpl. intros. inversion_clear H. apply (Lt_hd A leA); auto with sets. @@ -54,7 +54,7 @@ Section Wf_Lexicographic_Exponentiation. ltl x (y ++ z) -> ltl x y \/ (exists y' : List, x = y ++ y' /\ ltl y' z). Proof. intros x y; generalize x. - elim y; simpl in |- *. + elim y; simpl. right. exists x0; auto with sets. intros. @@ -196,7 +196,7 @@ Section Wf_Lexicographic_Exponentiation. Descl x0 /\ Descl (l0 ++ Cons x1 Nil)). - simpl in |- *. + simpl. split. generalize (app_inj_tail _ _ _ _ H2); simple induction 1. simple induction 1; auto with sets. @@ -239,7 +239,7 @@ Section Wf_Lexicographic_Exponentiation. Proof. intros a b x. case x. - simpl in |- *. + simpl. simple induction 1. intros. inversion H1; auto with sets. @@ -267,7 +267,7 @@ Section Wf_Lexicographic_Exponentiation. case x. intros; apply (Lt_nil A leA). - simpl in |- *; intros. + simpl; intros. inversion_clear H0. apply (Lt_hd A leA a b); auto with sets. @@ -284,17 +284,17 @@ Section Wf_Lexicographic_Exponentiation. apply (Acc_inv (R:=Lex_Exp) (x:=<< x1 ++ x2, y1 >>)). auto with sets. - unfold lex_exp in |- *; simpl in |- *; auto with sets. + unfold lex_exp; simpl; auto with sets. Qed. Theorem wf_lex_exp : well_founded leA -> well_founded Lex_Exp. Proof. - unfold well_founded at 2 in |- *. + unfold well_founded at 2. simple induction a; intros x y. apply Acc_intro. simple induction y0. - unfold lex_exp at 1 in |- *; simpl in |- *. + unfold lex_exp at 1; simpl. apply rev_ind with (A := A) (P := fun x:List => @@ -335,8 +335,8 @@ Section Wf_Lexicographic_Exponentiation. intro. apply Acc_intro. simple induction y2. - unfold lex_exp at 1 in |- *. - simpl in |- *; intros x4 y3. intros. + unfold lex_exp at 1. + simpl; intros x4 y3. intros. apply (H0 x4 y3); auto with sets. intros. @@ -357,7 +357,7 @@ Section Wf_Lexicographic_Exponentiation. generalize (HInd2 f); intro. apply Acc_intro. simple induction y3. - unfold lex_exp at 1 in |- *; simpl in |- *; intros. + unfold lex_exp at 1; simpl; intros. apply H15; auto with sets. Qed. diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index 0e096100..c3e8c92c 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.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 *) @@ -27,7 +27,7 @@ Section WfLexicographic_Product. forall x:A, Acc leA x -> (forall x0:A, clos_trans A leA x0 x -> well_founded (leB x0)) -> - forall y:B x, Acc (leB x) y -> Acc LexProd (existS B x y). + forall y:B x, Acc (leB x) y -> Acc LexProd (existT B x y). Proof. induction 1 as [x _ IHAcc]; intros H2 y. induction 1 as [x0 H IHAcc0]; intros. @@ -60,7 +60,7 @@ Section WfLexicographic_Product. well_founded leA -> (forall x:A, well_founded (leB x)) -> well_founded LexProd. Proof. - intros wfA wfB; unfold well_founded in |- *. + intros wfA wfB; unfold well_founded. destruct a. apply acc_A_B_lexprod; auto with sets; intros. red in wfB. @@ -94,7 +94,7 @@ Section Wf_Symmetric_Product. Lemma wf_symprod : well_founded leA -> well_founded leB -> well_founded Symprod. Proof. - red in |- *. + red. destruct a. apply Acc_symprod; auto with sets. Defined. @@ -161,7 +161,7 @@ Section Swap. Lemma wf_swapprod : well_founded R -> well_founded SwapProd. Proof. - red in |- *. + red. destruct a; intros. apply Acc_swapprod; auto with sets. Defined. diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index e9bc7ccf..943840cd 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.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 *) @@ -18,7 +18,7 @@ Section Wf_Transitive_Closure. Notation trans_clos := (clos_trans A R). Lemma incl_clos_trans : inclusion A R trans_clos. - red in |- *; auto with sets. + red; auto with sets. Qed. Lemma Acc_clos_trans : forall x:A, Acc R x -> Acc trans_clos x. @@ -39,7 +39,7 @@ Section Wf_Transitive_Closure. Theorem wf_clos_trans : well_founded R -> well_founded trans_clos. Proof. - unfold well_founded in |- *; auto with sets. + unfold well_founded; auto with sets. Defined. End Wf_Transitive_Closure. diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v index e3fdc4c5..5e4fec65 100644 --- a/theories/Wellfounded/Union.v +++ b/theories/Wellfounded/Union.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,7 +51,7 @@ Section WfUnion. elim strip_commut with x x0 y0; auto with sets; intros. apply Acc_inv_trans with x1; auto with sets. - unfold union in |- *. + unfold union. elim H11; auto with sets; intros. apply t_trans with y1; auto with sets. @@ -65,7 +65,7 @@ Section WfUnion. Theorem wf_union : commut A R1 R2 -> well_founded R1 -> well_founded R2 -> well_founded Union. Proof. - unfold well_founded in |- *. + unfold well_founded. intros. apply Acc_union; auto with sets. Qed. diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index fc4e2ebc..df6d9ed6 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.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 *) @@ -25,7 +25,7 @@ Section WellOrdering. Theorem wf_WO : well_founded le_WO. Proof. - unfold well_founded in |- *; intro. + unfold well_founded; intro. apply Acc_intro. elim a. intros. @@ -37,7 +37,7 @@ Section WellOrdering. apply (H v0 y0). cut (f = f1). intros E; rewrite E; auto. - symmetry in |- *. + symmetry . apply (inj_pair2 A (fun a0:A => B a0 -> WO) a0 f1 f H5). Qed. @@ -61,7 +61,7 @@ Section Characterisation_wf_relations. apply (well_founded_induction_type H (fun a:A => WO A B)); auto. intros x H1. apply (sup A B x). - unfold B at 1 in |- *. + unfold B at 1. destruct 1 as [x0]. apply (H1 x0); auto. Qed. diff --git a/theories/Wellfounded/Wellfounded.v b/theories/Wellfounded/Wellfounded.v index 4dc4d59d..b8c6653b 100644 --- a/theories/Wellfounded/Wellfounded.v +++ b/theories/Wellfounded/Wellfounded.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 *) |