Destruct/Induction -> NewDestruct/NewInduction

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

8 files changed, 130 insertions, 128 deletions

diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 2d5104af26..14b2453358 100755
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -42,7 +42,7 @@ Lemma between_Sk_l : (k,l:nat)(between k l)->(le (S k) l)->(between (S k) l).
 Proof.
 NewInduction 1.
 Intros; Absurd (le (S k) k); Auto with arith.
-Induction H; Auto with arith.
+NewDestruct H; Auto with arith.
 Qed.
 Hints Resolve between_Sk_l : arith v62.
 
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index e12d2f2ba1..92e56206b3 100755
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -62,9 +62,9 @@ Hints Immediate le_S_n : arith v62.
 
 Lemma le_pred : (n,m:nat)(le n m)->(le (pred n) (pred m)).
 Proof.
-Induction n. Simpl. Auto with arith.
-Intros n0 Hn0. Induction m. Simpl. Intro H. Inversion H.
-Intros n1 H H0. Simpl. Auto with arith.
+NewInduction n as [|n IHn]. Simpl. Auto with arith.
+NewDestruct m as [|m]. Simpl. Intro H. Inversion H.
+Simpl. Auto with arith.
 Qed.
 
 (** Negative properties *)
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 14dd98dacb..00a3b945a9 100755
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -123,7 +123,7 @@ Hints Resolve mult_lt : arith.
 Lemma lt_mult_right :
   (m,n,p:nat) (lt m n) -> (lt (0) p) -> (lt (mult m p) (mult n p)).
 Intros m n p H H0.
-Induction p.
+NewInduction p.
 Elim (lt_n_n ? H0).
 Rewrite mult_sym.
 Replace (mult n (S p)) with (mult (S p) n); Auto with arith.
@@ -162,8 +162,8 @@ Fixpoint mult_acc [s,m,n:nat] : nat :=
 
 Lemma mult_acc_aux : (n,s,m:nat)(plus s (mult n m))= (mult_acc s m n).
 Proof.
-Induction n; Simpl;Auto.
-Intros p H s m; Rewrite <- plus_tail_plus; Rewrite <- H.
+NewInduction n as [|p IHp]; Simpl;Auto.
+Intros s m; Rewrite <- plus_tail_plus; Rewrite <- IHp.
 Rewrite <- plus_assoc_r; Apply (f_equal2 nat nat);Auto.
 Rewrite plus_sym;Auto.
 Qed.
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 2285c544cd..843ba07394 100755
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -176,6 +176,6 @@ Fixpoint plus_acc [q,n:nat] : nat :=
 Definition tail_plus := [n,m:nat](plus_acc m n).
 
 Lemma plus_tail_plus : (n,m:nat)(n+m)=(tail_plus n m).
-Induction n; Unfold tail_plus; Simpl; Auto.
-Intros p H m; Rewrite <- H; Simpl; Auto.
+Unfold tail_plus; NewInduction n as [|n IHn]; Simpl; Auto.
+Intro m; Rewrite <- IHn; Simpl; Auto.
 Qed.
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 :
diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v
index 455d6f6494..8979966709 100755
--- a/theories/Lists/TheoryList.v
+++ b/theories/Lists/TheoryList.v
@@ -108,9 +108,9 @@ Fixpoint Length_l [l:(list A)] : nat -> nat
 
 (* A tail recursive version *)
 Lemma Length_l_pf : (l:(list A))(n:nat){m:nat|(plus n (length l))=m}.
-Induction l.
+NewInduction l as [|a m lrec].
 Intro n; Exists n; Simpl; Auto.
-Intros a m lrec n; Elim (lrec (S n)); Simpl; Intros.
+Intro n; Elim (lrec (S n)); Simpl; Intros.
 Exists x; Transitivity (S (plus n (length m))); Auto.
 (*
 Realizer Length_l.
@@ -194,16 +194,16 @@ Inductive fst_nth_spec : (list A)->nat->A->Prop :=
 Hints Resolve fst_nth_O fst_nth_S.
 
 Lemma fst_nth_nth : (l:(list A))(n:nat)(a:A)(fst_nth_spec l n a)->(nth_spec l n a).
-Induction 1; Auto.
+NewInduction 1; Auto.
 Qed.
 Hints Immediate fst_nth_nth.
 
 Lemma nth_lt_O : (l:(list A))(n:nat)(a:A)(nth_spec l n a)->(lt O n).
-Induction 1; Auto.
+NewInduction 1; Auto.
 Qed.
 
 Lemma nth_le_length : (l:(list A))(n:nat)(a:A)(nth_spec l n a)->(le n (length l)).
-  Induction 1; Simpl; Auto with arith.
+NewInduction 1; Simpl; Auto with arith.
 Qed.
 
 Fixpoint Nth_func [l:(list A)] : nat -> (Exc A) 
@@ -215,14 +215,13 @@ Fixpoint Nth_func [l:(list A)] : nat -> (Exc A)
 
 Lemma Nth : (l:(list A))(n:nat)
             {a:A|(nth_spec l n a)}+{(n=O)\/(lt (length l) n)}.
-Induction l.
+NewInduction l as [|a l IHl].
 Intro n; Case n; Simpl; Auto with arith.
-Intros; Case n; Simpl; Auto.
-Intro n0; Case n0.
+Intro n; NewDestruct n as [|[|n1]]; Simpl; Auto.
 Left; Exists a; Auto.
-Intro n1; Case (H (S n1)); Intro.
-Case s; Intros b p; Left; Exists b; Auto.
-Right; Case o; Intro.
+NewDestruct (IHl (S n1)) as [[b]|o].
+Left; Exists b; Auto.
+Right; NewDestruct o.
 Absurd (S n1)=O; Auto.
 Auto with arith.
 
@@ -252,14 +251,14 @@ Fixpoint index_p [a:A;l:(list A)] : nat -> (Exc nat) :=
 
 Lemma Index_p : (a:A)(l:(list A))(p:nat)
      {n:nat|(fst_nth_spec l (minus (S n) p) a)}+{(AllS [b:A]~a=b l)}.
-Induction l.
+NewInduction l as [|b m irec].
 Auto.
-Intros b m irec p.
-Case  (eqA_dec a b); Intro e.
+Intro p.
+NewDestruct (eqA_dec a b) as [e|e].
 Left; Exists p.
-Case e; Elim minus_Sn_m; Trivial; Elim minus_n_n; Auto with arith.
-Case (irec (S p)); Intro.
-Case s; Intros n H; Left; Exists n; Auto with arith.
+NewDestruct e; Elim minus_Sn_m; Trivial; Elim minus_n_n; Auto with arith.
+NewDestruct (irec (S p)) as [[n H]|].
+Left; Exists n; Auto with arith.
 Elim minus_Sn_m; Auto with arith.
 Apply lt_le_weak; Apply lt_O_minus_lt; Apply nth_lt_O with m a; Auto with arith.
 Auto.
@@ -298,7 +297,7 @@ Definition InR_inv :=
                end.
 
 Lemma InR_INV : (l:(list A))(InR l)->(InR_inv l).
-Induction 1; Simpl; Auto.
+NewInduction 1; Simpl; Auto.
 Qed.
 
 Lemma InR_cons_inv : (a:A)(l:(list A))(InR (cons a l))->((R a)\/(InR l)).
@@ -306,9 +305,9 @@ Intros a l H; Exact (InR_INV H).
 Qed.
 
 Lemma InR_or_app : (l,m:(list A))((InR l)\/(InR m))->(InR (app l m)).
-Induction 1.
-Induction 1; Simpl; Auto.
-Intro; Elim l; Simpl; Auto.
+Intros l m [|].
+NewInduction 1; Simpl; Auto.
+Intro. NewInduction l; Simpl; Auto.
 Qed.
 
 Lemma InR_app_or : (l,m:(list A))(InR (app l m))->((InR l)\/(InR m)).
@@ -325,11 +324,9 @@ Fixpoint find [l:(list A)] : (Exc A) :=
         end.
 
 Lemma Find : (l:(list A)){a:A | (In a l) & (R a)}+{(AllS P l)}.
-Induction l; Auto.
-Intros a m H.
-Case H.
-Intros (b,H1,H2); Left; Exists b; Auto.
-Intro; Case (RS_dec a); Intro.
+NewInduction l as [|a m [[b H1 H2]|H]]; Auto.
+Left; Exists b; Auto.
+NewDestruct (RS_dec a).
 Left; Exists a; Auto.
 Auto.
 (*
@@ -354,14 +351,11 @@ Fixpoint try_find [l:(list A)] : (Exc B) :=
    end.
 
 Lemma Try_find : (l:(list A)){c:B|(EX a:A |(In a l) & (T a c))}+{(AllS P l)}.
-Induction l.
+NewInduction l as [|a m [[b H1]|H]].
 Auto.
-Intros a m H.
-Case H.
-Intros (b,H1); Left; Exists b.
-Case H1; Intros a' H2 H3; Exists a'; Auto.
-Intro; Case (TS_dec a); Intro.
-Case s; Intros c H1; Left; Exists c.
+Left; Exists b; NewDestruct H1 as [a' H2 H3]; Exists a'; Auto.
+NewDestruct (TS_dec a) as [[c H1]|].
+Left; Exists c.
 Exists a; Auto.
 Auto.
 
@@ -389,14 +383,20 @@ Inductive AllS_assoc [P:A -> Prop]: (list A*B) -> Prop :=
 
 Hints Resolve allS_assoc_nil allS_assoc_cons.
 
+(* The specification seems too weak: it is enough to return b if the
+   list has at least an element (a,b); probably the intention is to have
+   the specification
+
+   (a:A)(l:(list A*B)){b:B|(In_spec (a,b) l)}+{(AllS_assoc [a':A]~(a=a') l)}.
+*)
+
 Lemma Assoc : (a:A)(l:(list A*B))(B+{(AllS_assoc [a':A]~(a=a') l)}).
-Induction l; Auto.
-Intros (a',b) m assrec.
-Case (eqA_dec a a'); Intro.
+NewInduction l as [|[a' b] m assrec]. Auto.
+NewDestruct (eqA_dec a a').
 Left; Exact b.
-Case assrec.
-Intro b'; Left; Exact b'.
-Auto.
+NewDestruct assrec as [b'|].
+Left; Exact b'.
+Right; Auto.
 (*
 Realizer assoc.
 Program_all.