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

6 files changed, 103 insertions, 55 deletions

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 28fc7e2906..cf9c90e17e 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -147,7 +147,9 @@ let new_instance ctx (instid, bk, cl) props =
 	  App (c, args) -> 
 	    let cl = Option.get (class_of_constr c) in
 	      cl, ctx, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args))
-	| _ -> assert false)
+	| _ -> 
+	    let cl = Option.get (class_of_constr c) in
+	      cl, ctx, [])
   in
   let env' = Classes.push_named_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 36a0e9c91a..986825f25c 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -566,8 +566,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  (pretype_type empty_valcon env isevars lvar c).utj_val in
     let evd,_ = consider_remaining_unif_problems env !isevars in
     let evd = nf_evar_defs evd in
-    let c' = nf_evar (evars_of evd) c' in
-(*     let evd = undefined_evars evd in *)
     let evd = Typeclasses.resolve_typeclasses env (evars_of evd) evd in
     let c' = nf_evar (evars_of evd) c' in
       isevars := evd;
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index db46c621ff..eb62f602aa 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -327,11 +327,4 @@ val tclABSTRACT : identifier option -> tactic -> tactic
 
 val admit_as_an_axiom : tactic
 
-val make_abstract_generalize :     'a ->
-    Names.identifier ->
-    Term.constr ->
-    Sign.rel_context ->
-    Term.types ->
-    Term.types list ->
-    Term.constr list -> Term.constr list -> Term.constr -> Term.constr
 val abstract_generalize : identifier -> tactic
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index d81589fc47..78edda65e1 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
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 85ed188910..c570aa9836 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -1,3 +1,4 @@
+(* -*- coq-prog-args: ("-emacs-U") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -13,6 +14,8 @@
 Require Export ProofIrrelevance.
 Require Export JMeq.
 
+Require Import Coq.Program.Tactics.
+
 (** Notation for heterogenous equality. *)
 
 Notation " [ x : X ] = [ y : Y ] " := (@JMeq X x Y y) (at level 0, X at next level, Y at next level).
@@ -170,27 +173,36 @@ Ltac simplify_eqs :=
   simpl ; simpl_eqs ; clear_eq_ctx ; clear_refl_eqs ;  
     try subst ; simpl ; repeat simpl_uip ; rewrite_refl_id.
 
-(** A tactic to remove trivial equality guards in hypotheses. *)
+(** A tactic that tries to remove trivial equality guards in induction hypotheses coming
+   from [dependent induction]/[generalize_eqs] invocations. *)
 
 Ltac simpl_IH_eq H :=
-  let tac H' := clear H ; rename H' into H in
-  let H' := fresh "H" in
-    match type of H with
-      | JMeq _ _ -> _ =>
-        assert (H' := H (JMeq_refl _)) ; tac H'
-      | _ = _ -> _ =>
-        assert (H' := H (refl_equal _)) ; tac H'
-    end.
+  match type of H with
+    | JMeq _ _ -> _ =>
+      refine_hyp (H (JMeq_refl _))
+    | ?x = _ -> _ =>
+      refine_hyp (H (refl_equal x))
+    | _ -> ?x = _ -> _ =>
+      refine_hyp (H _ (refl_equal x))
+    | _ -> _ -> ?x = _ -> _ =>
+      refine_hyp (H _ _ (refl_equal x))
+    | _ -> _ -> _ -> ?x = _ -> _ =>
+      refine_hyp (H _ _ _ (refl_equal x))
+    | _ -> _ -> _ -> _ -> ?x = _ -> _ =>
+      refine_hyp (H _ _ _ _ (refl_equal x))
+    | _ -> _ -> _ -> _ -> _ -> ?x = _ -> _ =>
+      refine_hyp (H _ _ _ _ _ (refl_equal x))
+  end.
 
 Ltac simpl_IH_eqs H := repeat simpl_IH_eq H.
 
-Ltac simpl_IHs_eqs := 
+Ltac do_simpl_IHs_eqs := 
   match goal with
-    | [ H : JMeq _ _ -> _ |- _ ] => simpl_IH_eqs H
-    | [ H : _ = _ -> _ |- _ ] => simpl_IH_eqs H
+    | [ H : context [ JMeq _ _ -> _ ] |- _ ] => progress (simpl_IH_eqs H)
+    | [ H : context [ _ = _ -> _ ] |- _ ] => progress (simpl_IH_eqs H)
   end.
 
-Require Import Coq.Program.Tactics.
+Ltac simpl_IHs_eqs := repeat do_simpl_IHs_eqs.
 
 (** The following tactics allow to do induction on an already instantiated inductive predicate
    by first generalizing it and adding the proper equalities to the context, in a maner similar to 
@@ -198,10 +210,10 @@ Require Import Coq.Program.Tactics.
 
 Tactic Notation "dependent" "induction" ident(H) := 
   generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; 
-    induction H ; intros ; subst* ; try discriminates ; try simpl_IHs_eqs.
+    induction H ; intros ; subst* ; try discriminates ; simpl_IHs_eqs.
 
 (** This tactic also generalizes the goal by the given variables before the induction. *)
 
 Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := 
   generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; 
-    generalize l ; clear l ; induction H ; intros ; subst* ; try discriminates ; try simpl_IHs_eqs.
+    generalize l ; clear l ; induction H ; intros ; subst* ; try discriminates ; simpl_IHs_eqs.
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index ad03de2f40..bb06f37b5a 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -8,7 +8,8 @@
 
 (*i $Id$ i*)
 
-(** This module implements various tactics used to simplify the goals produced by Program. *)
+(** This module implements various tactics used to simplify the goals produced by Program,
+   which are also generally useful. *)
 
 (** Destructs one pair, without care regarding naming. *)
 
@@ -166,6 +167,23 @@ Ltac add_hypothesis H' p :=
     end
   end.
 
+Tactic Notation "pose" constr(c) "as" ident(H) := assert(H:=c).
+
+(** A tactic to refine an hypothesis by supplying some of its arguments. *)
+
+Ltac refine_hyp c :=
+  let H' := fresh "H" in
+  let tac H := assert(H' := c) ; clear H ; rename H' into H in
+    match c with
+      | ?H _ => tac H
+      | ?H _ _ => tac H
+      | ?H _ _ _ => tac H
+      | ?H _ _ _ _ => tac H
+      | ?H _ _ _ _ _ => tac H
+      | ?H _ _ _ _ _ _ => tac H
+      | ?H _ _ _ _ _ _ _ => tac H
+      | ?H _ _ _ _ _ _ _ _ => tac H
+    end.
 
 (** The default simplification tactic used by Program is defined by [program_simpl], sometimes [auto with *]
    is overkill and slows things down, better rebind using [Obligations Tactic := tac] in this case, 
@@ -175,6 +193,6 @@ Ltac program_simplify :=
   simpl ; intros ; destruct_conjs ; simpl proj1_sig in * ; subst* ; try autoinjection ; try discriminates ;
     try (solve [ red ; intros ; destruct_conjs ; try autoinjection ; discriminates ]).
 
-Ltac default_program_simpl := program_simplify ; auto with *.
+Ltac program_simpl := program_simplify ; auto with *.
 
-Ltac program_simpl := default_program_simpl.
+Ltac obligations_tactic := program_simpl.