From 19dd83cf1b0e57fb13a8d970251822afd6a04ced Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 23 Sep 2003 21:00:49 +0000 Subject: Remplacement de Induction/Destruct par NewInduction/NewDestruct git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4463 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Wellfounded/Disjoint_Union.v | 16 +++--- theories/Wellfounded/Inclusion.v | 2 +- theories/Wellfounded/Inverse_Image.v | 16 +++--- theories/Wellfounded/Lexicographic_Product.v | 73 +++++++++++++--------------- theories/Wellfounded/Transitive_Closure.v | 14 ++---- theories/Wellfounded/Union.v | 25 +++++----- theories/Wellfounded/Well_Ordering.v | 3 +- 7 files changed, 68 insertions(+), 81 deletions(-) (limited to 'theories/Wellfounded') diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v index 6e9cbf062..44c2f8661 100644 --- a/theories/Wellfounded/Disjoint_Union.v +++ b/theories/Wellfounded/Disjoint_Union.v @@ -23,8 +23,8 @@ Notation Le_AsB := (le_AsB A B leA leB). Lemma acc_A_sum: (x:A)(Acc A leA x)->(Acc A+B Le_AsB (inl A B x)). Proof. - Induction 1;Intros. - Apply Acc_intro;Intros. + NewInduction 1. + Apply Acc_intro;Intros y H2. Inversion_clear H2. Auto with sets. Qed. @@ -32,8 +32,8 @@ Qed. Lemma acc_B_sum: (well_founded A leA) ->(x:B)(Acc B leB x) ->(Acc A+B Le_AsB (inr A B x)). Proof. - Induction 2;Intros. - Apply Acc_intro;Intros. + NewInduction 2. + Apply Acc_intro;Intros y H3. Inversion_clear H3;Auto with sets. Apply acc_A_sum;Auto with sets. Qed. @@ -45,12 +45,10 @@ Lemma wf_disjoint_sum: Proof. Intros. Unfold well_founded . - Induction a. - Intro a0. - Apply (acc_A_sum a0). - Apply (H a0). + NewDestruct a as [a|b]. + Apply (acc_A_sum a). + Apply (H a). - Intro b. Apply (acc_B_sum H b). Apply (H0 b). Qed. diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v index d2658e717..2038b34bf 100644 --- a/theories/Wellfounded/Inclusion.v +++ b/theories/Wellfounded/Inclusion.v @@ -18,7 +18,7 @@ Section WfInclusion. Lemma Acc_incl: (inclusion A R1 R2)->(z:A)(Acc A R2 z)->(Acc A R1 z). Proof. - Induction 2;Intros. + NewInduction 2. Apply Acc_intro;Auto with sets. Qed. diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v index 9afffc95c..ac828ac1a 100644 --- a/theories/Wellfounded/Inverse_Image.v +++ b/theories/Wellfounded/Inverse_Image.v @@ -19,10 +19,10 @@ Section Inverse_Image. Local Rof : A->A->Prop := [x,y:A](R (f x) (f y)). Remark Acc_lemma : (y:B)(Acc B R y)->(x:A)(y=(f x))->(Acc A Rof x). - Induction 1; Intros. - Apply Acc_intro; Intros. - Apply (H1 (f y0)); Try Trivial. - Rewrite H2; Trivial. + NewInduction 1 as [y _ IHAcc]; Intros x H. + Apply Acc_intro; Intros y0 H1. + Apply (IHAcc (f y0)); Try Trivial. + Rewrite H; Trivial. Qed. Lemma Acc_inverse_image : (x:A)(Acc B R (f x)) -> (Acc A Rof x). @@ -39,10 +39,10 @@ Section Inverse_Image. Lemma Acc_inverse_rel : (b:B)(Acc B R b)->(x:A)(F x b)->(Acc A RoF x). -Induction 1; Intros. -Constructor; Intros. -Case H3; Intros. -Apply (H1 x1); Auto. +NewInduction 1 as [x _ IHAcc]; Intros x0 H2. +Constructor; Intros y H3. +NewDestruct H3. +Apply (IHAcc x1); Auto. Save. diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index 39b00e676..b8f74c9ff 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -(** Authors: Bruno Barras,Cristina Cornes *) +(** Authors: Bruno Barras, Cristina Cornes *) Require Eqdep. Require Relation_Operators. @@ -32,14 +32,13 @@ Lemma acc_A_B_lexprod : (x:A)(Acc A leA x) ->(y:(B x))(Acc (B x) (leB x) y) ->(Acc (sigS A B) LexProd (existS A B x y)). Proof. - Induction 1; Intros x0 H0 H1 H2 y. - Induction 1;Intros. + NewInduction 1 as [x _ IHAcc]; Intros H2 y. + NewInduction 1 as [x0 H IHAcc0];Intros. Apply Acc_intro. - Induction y0. - Intros x2 y1 H6. - Simple Inversion H6;Intros. - Cut (leA x2 x0);Intros. - Apply H1;Auto with sets. + NewDestruct y as [x2 y1]; Intro H6. + Simple Inversion H6; Intro. + Cut (leA x2 x);Intros. + Apply IHAcc;Auto with sets. Intros. Apply H2. Apply t_trans with x2 ;Auto with sets. @@ -48,20 +47,16 @@ Proof. Apply H2. Auto with sets. - Injection H8. - Induction 2. - Injection H9. - Induction 2;Auto with sets. + Injection H1. + NewDestruct 2. + Injection H3. + NewDestruct 2;Auto with sets. - Elim H8. - Generalize y2 y' H9 H7 . - Replace x3 with x0. - Clear H7 H8 H9 y2 y' x3 H6 y1 x2 y0. - Intros. - Apply H5. - Elim inj_pair2 with A B x0 y' x1 ;Auto with sets. - - Injection H9;Auto with sets. + Rewrite <- H1. + Injection H3; Intros _ Hx1. + Subst x1. + Apply IHAcc0. + Elim inj_pair2 with A B x y' x0; Assumption. Qed. Theorem wf_lexprod: @@ -69,7 +64,7 @@ Theorem wf_lexprod: -> (well_founded (sigS A B) LexProd). Proof. Intros wfA wfB;Unfold well_founded . - Induction a;Intros. + NewDestruct a. Apply acc_A_B_lexprod;Auto with sets;Intros. Red in wfB. Auto with sets. @@ -108,13 +103,13 @@ i*) Lemma Acc_symprod: (x:A)(Acc A leA x)->(y:B)(Acc B leB y) ->(Acc (A*B) Symprod (x,y)). -Proof. - Induction 1;Intros. - Elim H2;Intros. - Apply Acc_intro;Intros. + Proof. + NewInduction 1 as [x _ IHAcc]; Intros y H2. + NewInduction H2 as [x1 H3 IHAcc1]. + Apply Acc_intro;Intros y H5. Inversion_clear H5;Auto with sets. - Apply H1;Auto with sets. - Apply Acc_intro;Auto with sets. + Apply IHAcc; Auto. + Apply Acc_intro;Trivial. Qed. @@ -122,7 +117,7 @@ Lemma wf_symprod: (well_founded A leA)->(well_founded B leB) ->(well_founded (A*B) Symprod). Proof. Red. - Induction a;Intros. + NewDestruct a. Apply Acc_symprod;Auto with sets. Qed. @@ -161,24 +156,24 @@ Qed. Lemma Acc_swapprod: (x,y:A)(Acc A R x)->(Acc A R y) ->(Acc A*A SwapProd (x,y)). Proof. - Induction 1;Intros. + NewInduction 1 as [x0 _ IHAcc0];Intros H2. Cut (y0:A)(R y0 x0)->(Acc ? SwapProd (y0,y)). - Clear H1. - Elim H2;Intros. + Clear IHAcc0. + NewInduction H2 as [x1 _ IHAcc1]; Intros H4. Cut (y:A)(R y x1)->(Acc ? SwapProd (x0,y)). - Clear H3. + Clear IHAcc1. Intro. Apply Acc_intro. - Induction y0;Intros. + NewDestruct y; Intro H5. Inversion_clear H5. - Inversion_clear H6;Auto with sets. + Inversion_clear H0;Auto with sets. Apply swap_Acc. - Inversion_clear H6;Auto with sets. + Inversion_clear H0;Auto with sets. Intros. - Apply H3;Auto with sets;Intros. - Apply Acc_inv with (y1,x1) ;Auto with sets. + Apply IHAcc1;Auto with sets;Intros. + Apply Acc_inv with (y0,x1) ;Auto with sets. Apply sp_noswap. Apply right_sym;Auto with sets. @@ -189,7 +184,7 @@ Qed. Lemma wf_swapprod: (well_founded A R)->(well_founded A*A SwapProd). Proof. Red. - Induction a;Intros. + NewDestruct a;Intros. Apply Acc_swapprod;Auto with sets. Qed. diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index 1198c1d47..c650d4675 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -24,23 +24,19 @@ Section Wf_Transitive_Closure. Qed. Lemma Acc_clos_trans: (x:A)(Acc A R x)->(Acc A trans_clos x). - Induction 1. - Intros x0 H0 H1. + NewInduction 1 as [x0 _ H1]. Apply Acc_intro. Intros y H2. - Generalize H1 . - Elim H2;Auto with sets. - Intros x1 y0 z H3 H4 H5 H6 H7. - Apply Acc_inv with y0 ;Auto with sets. + NewInduction H2;Auto with sets. + Apply Acc_inv with y ;Auto with sets. Qed. Hints Resolve Acc_clos_trans. Lemma Acc_inv_trans: (x,y:A)(trans_clos y x)->(Acc A R x)->(Acc A R y). Proof. - Induction 1;Auto with sets. - Intros x0 y0 H0 H1. - Apply Acc_inv with y0 ;Auto with sets. + NewInduction 1 as [|x y];Auto with sets. + Intro; Apply Acc_inv with y; Assumption. Qed. Theorem wf_clos_trans: (well_founded A R) ->(well_founded A trans_clos). diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v index 084538d8c..ee45a9476 100644 --- a/theories/Wellfounded/Union.v +++ b/theories/Wellfounded/Union.v @@ -26,35 +26,34 @@ Remark strip_commut: (commut A R1 R2)->(x,y:A)(clos_trans A R1 y x)->(z:A)(R2 z y) ->(EX y':A | (R2 y' x) & (clos_trans A R1 z y')). Proof. - Induction 2;Intros. - Elim H with y0 x0 z ;Auto with sets;Intros. - Exists x1;Auto with sets. + NewInduction 2 as [x y|x y z H0 IH1 H1 IH2]; Intros. + Elim H with y x z ;Auto with sets;Intros x0 H2 H3. + Exists x0;Auto with sets. - Elim H2 with z0 ;Auto with sets;Intros. - Elim H4 with x1 ;Auto with sets;Intros. - Exists x2;Auto with sets. - Apply t_trans with x1 ;Auto with sets. + Elim IH1 with z0 ;Auto with sets;Intros. + Elim IH2 with x0 ;Auto with sets;Intros. + Exists x1;Auto with sets. + Apply t_trans with x0; Auto with sets. Qed. Lemma Acc_union: (commut A R1 R2)->((x:A)(Acc A R2 x)->(Acc A R1 x)) ->(a:A)(Acc A R2 a)->(Acc A Union a). Proof. - Induction 3. - Intros. + NewInduction 3 as [x H1 H2]. Apply Acc_intro;Intros. - Elim H4;Intros;Auto with sets. + Elim H3;Intros;Auto with sets. Cut (clos_trans A R1 y x);Auto with sets. ElimType (Acc A (clos_trans A R1) y);Intros. Apply Acc_intro;Intros. - Elim H9;Intros. - Apply H7;Auto with sets. + Elim H8;Intros. + Apply H6;Auto with sets. Apply t_trans with x0 ;Auto with sets. Elim strip_commut with x x0 y0 ;Auto with sets;Intros. Apply Acc_inv_trans with x1 ;Auto with sets. Unfold union . - Elim H12;Auto with sets;Intros. + Elim H11;Auto with sets;Intros. Apply t_trans with y1 ;Auto with sets. Apply (Acc_clos_trans A). diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index ebd4925d1..49595dd2b 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.v @@ -65,8 +65,7 @@ Proof. Intros. Apply (sup A B x). Unfold 1 B . - Induction 1. - Intros. + NewDestruct 1 as [x0]. Apply (H1 x0);Auto. Qed. -- cgit v1.2.3