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

7 files changed, 68 insertions, 81 deletions

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.