Work on dependent induction tactic and friends, finish the test-suite example

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

1 files changed, 52 insertions, 27 deletions

diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index d81589fc4..78edda65e 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -1,4 +1,6 @@
 Require Import Coq.Program.Program.
+Set Implicit Arguments.
+Unset Strict Implicit.
 
 Variable A : Set.
 
@@ -8,17 +10,18 @@ Goal forall n, forall v : vector (S n), vector n.
 Proof.
   intros n H.
   dependent induction H.
-  inversion H0 ; subst.
+  autoinjection.
   assumption.
 Save.
 
 Require Import ProofIrrelevance.
 
-Goal forall n, forall v : vector (S n), exists v' : vector n, exists a : A, v = vcons a n v'.
+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.
+  inversion H0. subst.
   rewrite (UIP_refl _ _ H0).
   simpl.
   exists H ; exists a.
@@ -38,41 +41,63 @@ Inductive ctx : Type :=
 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').
+| 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'.
 
-Fixpoint app (G D : ctx) : ctx :=
+Fixpoint conc (G D : ctx) : ctx :=
   match D with
     | empty => G
-    | snoc D' x => snoc (app G D') x
+    | snoc D' x => snoc (conc G D') x
   end.
 
-Lemma weakening : forall G D tau, term (app G D) tau -> forall tau', term (app (snoc G tau') D) tau.
-Proof with simpl in * ; auto.
+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).
+
+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.
   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...
+
+    apply weak...
+
+  destruct D...
+    apply weak ; apply abs ; apply H.
+
+    apply abs...
+    refine_hyp (IHterm 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.
 
   destruct D...
-    subst.
     apply weak ; apply ax.
 
-    inversion H ; subst.
     apply ax.
-    
+
   destruct D...
-    subst.
-    do 2 apply weak.
-    assumption.
-
-    apply weak.
-    apply IHterm.
-    inversion H0 ; subst ; reflexivity.
-
-  cut(term (snoc (app G0 D) tau'0) (arrow tau tau') -> term (app (snoc G0 tau'0) D) (arrow tau tau')).
-  intros.
-  apply H0.
-  apply weak.
+    pose (weakening (G:=G0) (D:=(empty, alpha)))...
+
+    apply weak...
+
   apply abs.
-  assumption.
+  refine_hyp (IHterm G0 (D, tau))...
 
-  intros.
-Admitted.
+  eapply app with tau...
+Qed.
\ No newline at end of file