Various little improvements:

- A new [dependent pattern] tactic to do a pattern on an object in an
inductive family and generalize by both the indexes and the object
itself. Useful to prepare a goal for elimination with a dependent
principle.
- Better dependent elimination simplification tactic that doesn't
throw away non-dependent equalities if they can't be injected.
- Add [fold_sub] and [unfold_sub] tactics for folding/unfolding
well-founded definitions using measures built by Program.


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

5 files changed, 47 insertions, 6 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 37498b13f0..d595bfe43e 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -505,6 +505,10 @@ TACTIC EXTEND generalize_eqs_vars
 | ["generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize id ~generalize_vars:true ]
 END
 
+TACTIC EXTEND dependent_pattern
+| ["dependent_pattern" constr(c) ] -> [ dependent_pattern c ]
+END
+
 TACTIC EXTEND conv
 | ["conv" constr(x) constr(y) ] -> [ conv x y ]
 END
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 36ec22ee61..02d9544f00 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2073,6 +2073,26 @@ let abstract_generalize id ?(generalize_vars=true) gl =
 			 tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars]) gl
 	    else tac gl
 	      
+let dependent_pattern c gl =
+  let cty = pf_type_of gl c in
+  let deps = 
+    match kind_of_term cty with
+    | App (f, args) -> Array.to_list args
+    | _ -> []
+  in
+  let varname c = match kind_of_term c with
+    | Var id -> id
+    | _ -> id_of_string (hdchar (pf_env gl) c)
+  in
+  let mklambda ty (c, id, cty) =
+    let conclvar = subst_term_occ all_occurrences c ty in
+      mkNamedLambda id cty conclvar
+  in
+  let subst = (c, varname c, cty) :: List.map (fun c -> (c, varname c, pf_type_of gl c)) deps in
+  let concllda = List.fold_left mklambda (pf_concl gl) subst in 
+  let conclapp = applistc concllda (List.rev_map pi1 subst) in
+    convert_concl_no_check conclapp DEFAULTcast gl
+      
 let occur_rel n c = 
   let res = not (noccurn n c) in
   res
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 58df7155e7..1ebaec3b4e 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -365,5 +365,7 @@ val admit_as_an_axiom : tactic
 
 val abstract_generalize : identifier -> ?generalize_vars:bool -> tactic
 
+val dependent_pattern : constr -> tactic
+
 val register_general_multi_rewrite : 
   (bool -> evars_flag -> constr with_ebindings -> clause -> tactic) -> unit
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 2b914ace76..d37fd62f6e 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -359,9 +359,9 @@ Definition block_dep_elim {A : Type} (a : A) := a.
 
 Ltac simplify_one_dep_elim_term c :=
   match c with
-    | @JMeq ?A ?a ?A ?b -> _ => refine (simplification_heq _ _ _ _ _)
+    | @JMeq _ _ _ _ -> _ => refine (simplification_heq _ _ _ _ _)
     | ?t = ?t -> _ => intros _ || refine (simplification_K _ t _ _)
-    | eq (existT ?P ?p _) (existT ?P ?p _) -> _ => refine (simplification_existT _ _ _ _ _ _ _)
+    | eq (existT _ _ _) (existT _ _ _) -> _ => refine (simplification_existT _ _ _ _ _ _ _)
     | ?x = ?y -> _ => (* variables case *)
       (let hyp := fresh in intros hyp ;
         move dependent hyp before x ;
@@ -370,11 +370,12 @@ Ltac simplify_one_dep_elim_term c :=
         move dependent hyp before y ;
           generalize dependent y ; refine (solution_right _ _ _ _) ; intros until 0)
     | @eq ?A ?t ?u -> ?P => apply (noConfusion (I:=A) P)
-    | ?f ?x = ?g ?y -> _ => let H := fresh in intros H ; injection H ; clear H
+    | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H)
     | ?t = ?u -> _ => let hyp := fresh in
       intros hyp ; elimtype False ; discriminate
     | ?x = ?y -> _ => let hyp := fresh in
-      intros hyp ; case hyp ; clear hyp
+      intros hyp ; (try (clear hyp ; (* If non dependent, don't clear it! *) fail 1)) ;
+        case hyp ; clear hyp
     | block_dep_elim ?T => fail 1 (* Do not put any part of the rhs in the hyps *)
     | _ => intro
   end.
diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v
index 440217bfec..8bd2dfb905 100644
--- a/theories/Program/FunctionalExtensionality.v
+++ b/theories/Program/FunctionalExtensionality.v
@@ -22,7 +22,7 @@ Require Import Coq.Program.Equality.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** The converse of functional equality. *)
+(** The converse of functional extensionality. *)
 
 Lemma equal_f : forall A B : Type, forall (f g : A -> B), 
   f = g -> forall x, f x = g x.
@@ -32,7 +32,7 @@ Proof.
   auto.
 Qed.
 
-(** Statements of functional equality for simple and dependent functions. *)
+(** Statements of functional extensionality for simple and dependent functions. *)
 
 Axiom fun_extensionality_dep : forall A, forall B : (A -> Type), 
   forall (f g : forall x : A, B x), 
@@ -106,4 +106,18 @@ Proof.
   rewrite H0 ; auto.
 Qed.
 
+(** Tactics to fold/unfold definitions based on [Fix_measure_sub]. *)
 
+Ltac fold_sub f :=
+  match goal with
+    | [ |- ?T ] => 
+      match T with
+        appcontext C [ @Fix_measure_sub _ _ _ _ ?arg ] => 
+        let app := context C [ f arg ] in
+         change app
+      end
+  end.
+
+Ltac unfold_sub f fargs := 
+  set (call:=fargs) ; unfold f in call ; unfold call ; clear call ; 
+  rewrite fix_sub_measure_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig.