Destruct/Induction -> NewDestruct/NewInduction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4469 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 82 insertions, 80 deletions

diff --git a/theories/IntMap/Adalloc.v b/theories/IntMap/Adalloc.v
index e348cfafb6..d2ca86b2f8 100644
--- a/theories/IntMap/Adalloc.v
+++ b/theories/IntMap/Adalloc.v
@@ -37,15 +37,15 @@ Section AdAlloc.
 
   Lemma nat_le_correct : (m,n:nat) (le m n) -> (nat_le m n)=true.
   Proof.
-    Induction m. Trivial.
-    Induction n0. Intro. Elim (le_Sn_O ? H0).
-    Intros. Simpl. Apply H. Apply le_S_n. Assumption.
+    NewInduction m as [|m IHm]. Trivial.
+    NewDestruct n. Intro H. Elim (le_Sn_O ? H).
+    Intros. Simpl. Apply IHm. Apply le_S_n. Assumption.
   Qed.
 
   Lemma nat_le_complete : (m,n:nat) (nat_le m n)=true -> (le m n).
   Proof.
-    Induction m. Trivial with arith.
-    Induction n0. Intro. Discriminate H0.
+    NewInduction m. Trivial with arith.
+    NewDestruct n. Intro H. Discriminate H.
     Auto with arith.
   Qed.
 
@@ -69,14 +69,14 @@ Section AdAlloc.
 
   Lemma ad_of_nat_of_ad : (a:ad) (ad_of_nat (nat_of_ad a))=a.
   Proof.
-    Induction a. Reflexivity.
-    Intro. Simpl. Elim (ZL4 p). Intros p' H. Rewrite H. Simpl. Rewrite <- bij1 in H.
+    NewDestruct a as [|p]. Reflexivity.
+    Simpl. Elim (ZL4 p). Intros n H. Rewrite H. Simpl. Rewrite <- bij1 in H.
     Rewrite convert_intro with 1:=H. Reflexivity.
   Qed.
 
   Lemma nat_of_ad_of_nat : (n:nat) (nat_of_ad (ad_of_nat n))=n.
   Proof.
-    Induction n. Trivial.
+    NewInduction n. Trivial.
     Intros. Simpl. Apply bij1.
   Qed.
 
@@ -203,12 +203,12 @@ Section AdAlloc.
 
   Lemma ad_alloc_opt_allocates_1 : (m:(Map A)) (MapGet A m (ad_alloc_opt m))=(NONE A).
   Proof.
-    Induction m. Reflexivity.
-    Simpl. Intros. Elim (sumbool_of_bool (ad_eq a ad_z)). Intro H. Rewrite H.
+    NewInduction m as [|a|m0 H m1 H0]. Reflexivity.
+    Simpl. Elim (sumbool_of_bool (ad_eq a ad_z)). Intro H. Rewrite H.
     Rewrite (ad_eq_complete ? ? H). Reflexivity.
     Intro H. Rewrite H. Rewrite H. Reflexivity.
-    Intros. Change (MapGet A (M2 A m0 m1)
-         (ad_min (ad_double (ad_alloc_opt m0)) (ad_double_plus_un (ad_alloc_opt m1))))=(NONE A).
+    Intros. Change (ad_alloc_opt (M2 A m0 m1)) with
+         (ad_min (ad_double (ad_alloc_opt m0)) (ad_double_plus_un (ad_alloc_opt m1))).
     Elim (ad_min_choice (ad_double (ad_alloc_opt m0)) (ad_double_plus_un (ad_alloc_opt m1))).
     Intro H1. Rewrite H1. Rewrite MapGet_M2_bit_0_0. Rewrite ad_double_div_2. Assumption.
     Apply ad_double_bit_0.
@@ -226,15 +226,15 @@ Section AdAlloc.
 
   Lemma nat_of_ad_double : (a:ad) (nat_of_ad (ad_double a))=(mult (2) (nat_of_ad a)).
   Proof.
-    Induction a. Trivial.
-    Exact convert_xO.
+    NewDestruct a as [|p]. Trivial.
+    Exact (convert_xO p).
   Qed.
 
   Lemma nat_of_ad_double_plus_un : (a:ad)
       (nat_of_ad (ad_double_plus_un a))=(S (mult (2) (nat_of_ad a))).
   Proof.
-    Induction a. Trivial.
-    Exact convert_xI.
+    NewDestruct a as [|p]. Trivial.
+    Exact (convert_xI p).
   Qed.
 
   Lemma ad_le_double_mono : (a,b:ad) (ad_le a b)=true -> 
@@ -306,8 +306,8 @@ Section AdAlloc.
   Lemma ad_alloc_opt_optimal_1 : (m:(Map A)) (a:ad) (ad_le (ad_alloc_opt m) a)=false ->
       {y:A | (MapGet A m a)=(SOME A y)}.
   Proof.
-    Induction m. Simpl. Unfold ad_le. Simpl. Intros. Discriminate H.
-    Simpl. Intros a y b H. Elim (sumbool_of_bool (ad_eq a ad_z)). Intro H0. Rewrite H0 in H.
+    NewInduction m as [|a y|m0 H m1 H0]. Simpl. Unfold ad_le. Simpl. Intros. Discriminate H.
+    Simpl. Intros b H. Elim (sumbool_of_bool (ad_eq a ad_z)). Intro H0. Rewrite H0 in H.
     Unfold ad_le in H. Cut ad_z=b. Intro. Split with y. Rewrite <- H1. Rewrite H0. Reflexivity.
     Rewrite <- (ad_of_nat_of_ad b).
     Rewrite <- (le_n_O_eq ? (le_S_n ? ? (nat_le_complete_conv ? ? H))). Reflexivity.
diff --git a/theories/IntMap/Addec.v b/theories/IntMap/Addec.v
index 17742d60c4..f0ec7b37d2 100644
--- a/theories/IntMap/Addec.v
+++ b/theories/IntMap/Addec.v
@@ -31,27 +31,29 @@ Definition ad_eq := [a,a':ad]
 
 Lemma ad_eq_correct : (a:ad) (ad_eq a a)=true.
 Proof.
-  Induction a; Trivial.
-  Induction p; Trivial.
+  NewDestruct a; Trivial.
+  NewInduction p; Trivial.
 Qed.
 
 Lemma ad_eq_complete : (a,a':ad) (ad_eq a a')=true -> a=a'.
 Proof.
-  Induction a. Induction a'; Trivial. Induction p. Intros. Discriminate H0.
-  Intros. Discriminate H0.
-  Intros. Discriminate H.
-  Induction a'. Intros. Discriminate H.
+  NewDestruct a. NewDestruct a'; Trivial. NewDestruct p.
+  Discriminate 1.
+  Discriminate 1.
+  Discriminate 1.
+  NewDestruct a'. Intros. Discriminate H.
   Unfold ad_eq. Intros. Cut p=p0. Intros. Rewrite H0. Reflexivity.
-  Generalize p0 H. Elim p. Induction p2. Intros. 
-  Rewrite (H0 p3). Reflexivity.
-  Exact H2.
-  Intros. Discriminate H2.
-  Intros. Discriminate H1.
-  Induction p2. Intros. Discriminate H2.
-  Intros. Rewrite (H0 p3 H2). Reflexivity.
-  Intros. Discriminate H1.
-  Induction p1. Intros. Discriminate H1.
-  Intros. Discriminate H1.
+  Generalize Dependent p0.
+  NewInduction p as [p IHp|p IHp|]. NewDestruct p0; Intro H.
+  Rewrite (IHp p0). Reflexivity.
+  Exact H.
+  Discriminate H.
+  Discriminate H.
+  NewDestruct p0; Intro H. Discriminate H.
+  Rewrite (IHp p0 H). Reflexivity.
+  Discriminate H.
+  NewDestruct p0; Intro H. Discriminate H.
+  Discriminate H.
   Trivial.
 Qed.
 
@@ -60,10 +62,10 @@ Proof.
   Intros. Cut (b,b':bool)(ad_eq a a')=b->(ad_eq a' a)=b'->b=b'.
   Intros. Apply H. Reflexivity.
   Reflexivity.
-  Induction b. Intros. Cut a=a'.
+  NewDestruct b. Intros. Cut a=a'.
   Intro. Rewrite H1 in H0. Rewrite (ad_eq_correct a') in H0. Exact H0.
   Apply ad_eq_complete. Exact H.
-  Induction b'. Intros. Cut a'=a.
+  NewDestruct b'. Intros. Cut a'=a.
   Intro. Rewrite H1 in H. Rewrite H1 in H0. Rewrite <- H. Exact H0.
   Apply ad_eq_complete. Exact H0.
   Trivial.
@@ -143,9 +145,9 @@ Qed.
 Lemma ad_div_bit_eq : (a,a':ad) (ad_bit_0 a)=(ad_bit_0 a') ->
     (ad_div_2 a)=(ad_div_2 a') -> a=a'.
 Proof.
-  Intros. Apply ad_faithful. Unfold eqf. Induction n.
+  Intros. Apply ad_faithful. Unfold eqf. NewDestruct n.
   Rewrite ad_bit_0_correct. Rewrite ad_bit_0_correct. Assumption.
-  Intros. Rewrite <- ad_div_2_correct. Rewrite <- ad_div_2_correct.
+  Rewrite <- ad_div_2_correct. Rewrite <- ad_div_2_correct.
   Rewrite H0. Reflexivity.
 Qed.
 
diff --git a/theories/IntMap/Addr.v b/theories/IntMap/Addr.v
index 435a7c21c3..cff8936b6f 100644
--- a/theories/IntMap/Addr.v
+++ b/theories/IntMap/Addr.v
@@ -69,28 +69,28 @@ Qed.
 
 Lemma ad_xor_neutral_right : (a:ad) (ad_xor a ad_z)=a.
 Proof.
-  Induction a; Trivial.
+  NewDestruct a; Trivial.
 Qed.
 
 Lemma ad_xor_comm : (a,a':ad) (ad_xor a a')=(ad_xor a' a).
 Proof.
   NewDestruct a; NewDestruct a'; Simpl; Auto.
-  Generalize p0; Clear p0; Induction p; Simpl; Auto.
+  Generalize p0; Clear p0; NewInduction p as [p Hrecp|p Hrecp|]; Simpl; Auto.
   NewDestruct p0; Simpl; Trivial; Intros.
   Rewrite Hrecp; Trivial.
   Rewrite Hrecp; Trivial.
   NewDestruct p0; Simpl; Trivial; Intros.
   Rewrite Hrecp; Trivial.
   Rewrite Hrecp; Trivial.
-  Induction p0; Simpl; Auto.
+  NewDestruct p0; Simpl; Auto.
 Qed.
 
 Lemma ad_xor_nilpotent : (a:ad) (ad_xor a a)=ad_z.
 Proof.
-  Induction a; Trivial.
-  Induction p; Trivial.
-  Simpl; Intros. Rewrite H; Reflexivity.
-  Simpl; Intros. Rewrite H; Reflexivity.
+  NewDestruct a; Trivial.
+  Simpl. NewInduction p as [p IHp|p IHp|]; Trivial.
+  Simpl. Rewrite IHp; Reflexivity.
+  Simpl. Rewrite IHp; Reflexivity.
 Qed.
 
 Fixpoint ad_bit_1 [p:positive] : nat -> bool :=
@@ -119,23 +119,23 @@ Definition eqf := [f,g:nat->bool] (n:nat) (f n)=(g n).
 
 Lemma ad_faithful_1 : (a:ad) (eqf (ad_bit ad_z) (ad_bit a)) -> ad_z=a.
 Proof.
-  Induction a. Trivial.
-  Induction p. Intros. Absurd ad_z=(ad_x p0). Discriminate.
-  Exact (H [n:nat](H0 (S n))).
-  Intros. Absurd ad_z=(ad_x p0). Discriminate.
-  Exact (H [n:nat](H0 (S n))).
-  Intros. Absurd false=true. Discriminate.
+  NewDestruct a. Trivial.
+  NewInduction p as [p IHp|p IHp|];Intro H. Absurd ad_z=(ad_x p). Discriminate.
+  Exact (IHp [n:nat](H (S n))).
+  Absurd ad_z=(ad_x p). Discriminate.
+  Exact (IHp [n:nat](H (S n))).
+  Absurd false=true. Discriminate.
   Exact (H O).
 Qed.
 
 Lemma ad_faithful_2 : (a:ad) (eqf (ad_bit (ad_x xH)) (ad_bit a)) -> (ad_x xH)=a.
 Proof.
-  Induction a. Intros. Absurd true=false. Discriminate.
+  NewDestruct a. Intros. Absurd true=false. Discriminate.
   Exact (H O).
-  Induction p. Intros. Absurd ad_z=(ad_x p0). Discriminate.
-  Exact (ad_faithful_1 (ad_x p0) [n:nat](H0 (S n))).
+  NewDestruct p. Intro H. Absurd ad_z=(ad_x p). Discriminate.
+  Exact (ad_faithful_1 (ad_x p) [n:nat](H (S n))).
   Intros. Absurd true=false. Discriminate.
-  Exact (H0 O).
+  Exact (H O).
   Trivial.
 Qed.
 
@@ -145,10 +145,10 @@ Lemma ad_faithful_3 :
         (eqf (ad_bit (ad_x (xO p))) (ad_bit a)) ->
           (ad_x (xO p))=a.
 Proof.
-  Induction a. Intros. Cut (eqf (ad_bit ad_z) (ad_bit (ad_x (xO p)))).
+  NewDestruct a. Intros. Cut (eqf (ad_bit ad_z) (ad_bit (ad_x (xO p)))).
   Intro. Rewrite (ad_faithful_1 (ad_x (xO p)) H1). Reflexivity.
   Unfold eqf. Intro. Unfold eqf in H0. Rewrite H0. Reflexivity.
-  Intro. Case p. Intros. Absurd false=true. Discriminate.
+  Case p. Intros. Absurd false=true. Discriminate.
   Exact (H0 O).
   Intros. Rewrite (H p0 [n:nat](H0 (S n))). Reflexivity.
   Intros. Absurd false=true. Discriminate.
@@ -161,10 +161,10 @@ Lemma ad_faithful_4 :
         (eqf (ad_bit (ad_x (xI p))) (ad_bit a)) ->
           (ad_x (xI p))=a.
 Proof.
-  Induction a. Intros. Cut (eqf (ad_bit ad_z) (ad_bit (ad_x (xI p)))).
+  NewDestruct a. Intros. Cut (eqf (ad_bit ad_z) (ad_bit (ad_x (xI p)))).
   Intro. Rewrite (ad_faithful_1 (ad_x (xI p)) H1). Reflexivity.
   Unfold eqf. Intro. Unfold eqf in H0. Rewrite H0. Reflexivity.
-  Intro. Case p. Intros. Rewrite (H p0 [n:nat](H0 (S n))). Reflexivity.
+  Case p. Intros. Rewrite (H p0 [n:nat](H0 (S n))). Reflexivity.
   Intros. Absurd true=false. Discriminate.
   Exact (H0 O).
   Intros. Absurd ad_z=(ad_x p0). Discriminate.
@@ -175,13 +175,13 @@ Qed.
 
 Lemma ad_faithful : (a,a':ad) (eqf (ad_bit a) (ad_bit a')) -> a=a'.
 Proof.
-  Induction a. Exact ad_faithful_1.
-  Induction p. Intros. Apply ad_faithful_4. Intros. Cut (ad_x p0)=(ad_x p').
-  Intro. Inversion H2. Reflexivity.
-  Exact (H (ad_x p') H1).
+  NewDestruct a. Exact ad_faithful_1.
+  NewInduction p. Intros a' H. Apply ad_faithful_4. Intros. Cut (ad_x p)=(ad_x p').
+  Intro. Inversion H1. Reflexivity.
+  Exact (IHp (ad_x p') H0).
   Assumption.
-  Intros. Apply ad_faithful_3. Intros. Cut (ad_x p0)=(ad_x p'). Intro. Inversion H2. Reflexivity.
-  Exact (H (ad_x p') H1).
+  Intros. Apply ad_faithful_3. Intros. Cut (ad_x p)=(ad_x p'). Intro. Inversion H1. Reflexivity.
+  Exact (IHp (ad_x p') H0).
   Assumption.
   Exact ad_faithful_2.
 Qed.
@@ -223,8 +223,8 @@ Qed.
 Lemma ad_xor_sem_5 :
     (a,a':ad) (ad_bit (ad_xor a a') O)=(adf_xor (ad_bit a) (ad_bit a') O).
 Proof.
-  Induction a. Intro. Change (ad_bit a' O)=(xorb false (ad_bit a' O)). Rewrite false_xorb. Trivial.
-  Intro. Case p. Exact ad_xor_sem_4.
+  NewDestruct a. Intro. Change (ad_bit a' O)=(xorb false (ad_bit a' O)). Rewrite false_xorb. Trivial.
+  Case p. Exact ad_xor_sem_4.
   Intros. Change (ad_bit (ad_xor (ad_x (xO p0)) a') O)=(xorb false (ad_bit a' O)).
   Rewrite false_xorb. Apply ad_xor_sem_3. Exact ad_xor_sem_2.
 Qed.
@@ -345,12 +345,12 @@ Definition ad_div_2 := [a:ad]
 
 Lemma ad_double_div_2 : (a:ad) (ad_div_2 (ad_double a))=a.
 Proof.
-  Induction a; Trivial.
+  NewDestruct a; Trivial.
 Qed.
 
 Lemma ad_double_plus_un_div_2 : (a:ad) (ad_div_2 (ad_double_plus_un a))=a.
 Proof.
-  Induction a; Trivial.
+  NewDestruct a; Trivial.
 Qed.
 
 Lemma ad_double_inj : (a0,a1:ad) (ad_double a0)=(ad_double a1) -> a0=a1.
@@ -373,40 +373,40 @@ Definition ad_bit_0 := [a:ad]
 
 Lemma ad_double_bit_0 : (a:ad) (ad_bit_0 (ad_double a))=false.
 Proof.
-  Induction a; Trivial.
+  NewDestruct a; Trivial.
 Qed.
 
 Lemma ad_double_plus_un_bit_0 : (a:ad) (ad_bit_0 (ad_double_plus_un a))=true.
 Proof.
-  Induction a; Trivial.
+  NewDestruct a; Trivial.
 Qed.
 
 Lemma ad_div_2_double : (a:ad) (ad_bit_0 a)=false -> (ad_double (ad_div_2 a))=a.
 Proof.
-  Induction a. Trivial. Induction p. Intros. Discriminate H0.
+  NewDestruct a. Trivial. NewDestruct p. Intro H. Discriminate H.
   Intros. Reflexivity.
-  Intro. Discriminate H.
+  Intro H. Discriminate H.
 Qed.
 
 Lemma ad_div_2_double_plus_un :
     (a:ad) (ad_bit_0 a)=true -> (ad_double_plus_un (ad_div_2 a))=a.
 Proof.
-  Induction a. Intro. Discriminate H.
-  Induction p. Intros. Reflexivity.
-  Intros. Discriminate H0.
+  NewDestruct a. Intro. Discriminate H.
+  NewDestruct p. Intros. Reflexivity.
+  Intro H. Discriminate H.
   Intro. Reflexivity.
 Qed.
 
 Lemma ad_bit_0_correct : (a:ad) (ad_bit a O)=(ad_bit_0 a).
 Proof.
-  Induction a; Trivial.
-  Induction p; Trivial.
+  NewDestruct a; Trivial.
+  NewDestruct p; Trivial.
 Qed.
 
 Lemma ad_div_2_correct : (a:ad) (n:nat) (ad_bit (ad_div_2 a) n)=(ad_bit a (S n)).
 Proof.
-  Induction a; Trivial.
-  Induction p; Trivial.
+  NewDestruct a; Trivial.
+  NewDestruct p; Trivial.
 Qed.
 
 Lemma ad_xor_bit_0 :