Debug implementation of dependent induction/dependent destruction and document it.

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

1 files changed, 26 insertions, 26 deletions

diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index 78edda65e1..f45b592af8 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -9,8 +9,7 @@ Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall n, vecto
 Goal forall n, forall v : vector (S n), vector n.
 Proof.
   intros n H.
-  dependent induction H.
-  autoinjection.
+  dependent destruction H.
   assumption.
 Save.
 
@@ -19,11 +18,7 @@ Require Import ProofIrrelevance.
 Goal forall n, forall v : vector (S n), exists v' : vector n, exists a : A, v = vcons a v'.
 Proof.
   intros n H.
-
-  dependent induction H generalizing n.
-  inversion H0. subst.
-  rewrite (UIP_refl _ _ H0).
-  simpl.
+  dependent destruction H.
   exists H ; exists a.
   reflexivity.
 Save.
@@ -34,15 +29,13 @@ Inductive type : Type :=
 | base : type
 | arrow : type -> type -> type.
 
+Notation " t --> t' " := (arrow t t') (at level 20, t' at next level).
+
 Inductive ctx : Type :=
 | empty : ctx
 | snoc : ctx -> type -> ctx.
 
-Inductive term : ctx -> type -> Type :=
-| ax : forall G tau, term (snoc G tau) tau
-| weak : forall G tau, term G tau -> forall tau', term (snoc G tau') tau
-| abs : forall G tau tau', term (snoc G tau) tau' -> term G (arrow tau tau')
-| app : forall G tau tau', term G (arrow tau tau') -> term G tau -> term G tau'.
+Notation " G , tau " := (snoc G tau) (at level 20, t at next level).
 
 Fixpoint conc (G D : ctx) : ctx :=
   match D with
@@ -50,25 +43,32 @@ Fixpoint conc (G D : ctx) : ctx :=
     | snoc D' x => snoc (conc G D') x
   end.
 
-Hint Unfold conc.
-
 Notation " G ; D " := (conc G D) (at level 20).
-Notation " G , D " := (snoc G D) (at level 20,  D at next level).
+
+Inductive term : ctx -> type -> Type :=
+| ax : forall G tau, term (G, tau) tau
+| weak : forall G tau, 
+  term G tau -> forall tau', term (G, tau') tau
+| abs : forall G tau tau', 
+  term (G , tau) tau' -> term G (tau --> tau')
+| app : forall G tau tau', 
+  term G (tau --> tau') -> term G tau -> term G tau'.
 
 Lemma weakening : forall G D tau, term (G ; D) tau -> 
   forall tau', term (G , tau' ; D) tau.
-Proof with simpl in * ; program_simpl ; simpl_IHs_eqs.
+Proof with simpl in * ; auto ; simpl_depind.
   intros G D tau H.
 
-  dependent induction H generalizing G D...
+  dependent induction H generalizing G D.
 
   destruct D...
     apply weak ; apply ax.
     
     apply ax.
-
+    
   destruct D...
-    do 2 apply weak...
+    narrow IHterm with G empty...
+    apply weak...
 
     apply weak...
 
@@ -76,15 +76,15 @@ Proof with simpl in * ; program_simpl ; simpl_IHs_eqs.
     apply weak ; apply abs ; apply H.
 
     apply abs...
-    refine_hyp (IHterm G0 (D, t, tau))...
+    narrow IHterm with G0 (D, t, tau)...
 
   apply app with tau...
 Qed.
 
 Lemma exchange : forall G D alpha bet tau, term (G, alpha, bet ; D) tau -> term (G, bet, alpha ; D) tau.
-Proof with simpl in * ; program_simpl ; simpl_IHs_eqs.
-  intros G D alpha bet tau H.
-  dependent induction H generalizing G D alpha bet.
+Proof with simpl in * ; simpl_depind ; auto.
+  intros until 1.
+  dependent induction H generalizing G D alpha bet...
 
   destruct D...
     apply weak ; apply ax.
@@ -96,8 +96,8 @@ Proof with simpl in * ; program_simpl ; simpl_IHs_eqs.
 
     apply weak...
 
-  apply abs.
-  refine_hyp (IHterm G0 (D, tau))...
+  apply abs...
+  narrow IHterm with G0 (D, tau)...
 
   eapply app with tau...
-Qed.
\ No newline at end of file
+Save.