Ajout de la tactique "apply in".

Au passage, déplacement des tactiques cut and co plus en amont + commentaires.


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

5 files changed, 152 insertions, 50 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index b593411eaf..a0064b13b8 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -74,6 +74,26 @@ let clenv_get_type_of ce c =
       (meta_list ce.env) in
   Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) metamap c
 
+exception NotExtensibleClause
+
+let clenv_push_prod cl =
+  let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in
+  let rec clrec typ = match kind_of_term typ with
+    | Cast (t,_,_) -> clrec t
+    | Prod (na,t,u) ->
+	let mv = new_meta () in
+	let dep = dependent (mkRel 1) u in
+	let na' = if dep then na else Anonymous in
+	let e' = meta_declare mv t ~name:na' cl.env in
+	let concl = if dep then subst1 (mkMeta mv) u else u in
+	let def = applist (cl.templval.rebus,[mkMeta mv]) in
+	{ templval = mk_freelisted def;
+	  templtyp = mk_freelisted concl;
+	  env = e';
+	  templenv = cl.templenv }
+    | _ -> raise NotExtensibleClause
+  in clrec typ
+
 let clenv_environments evd bound c =
   let rec clrec (e,metas) n c =
     match n, kind_of_term c with
@@ -258,7 +278,20 @@ let connect_clenv gls clenv =
  * resolution can cause unification of already-existing metavars, and
  * of the fresh ones which get created.  This operation is a composite
  * of operations which pose new metavars, perform unification on
- * terms, and make bindings.  *)
+ * terms, and make bindings. 
+
+   Otherwise said, from 
+
+     [clenv] = [env;sigma;metas |- c:T]
+     [clenv'] = [env';sigma';metas' |- d:U]
+     [mv] = [mi] of type [Ti] in [metas]
+
+   then, if the unification of [Ti] and [U] produces map [rho], the
+   chaining is [env';sigma';rho'(metas),rho(metas') |- c:rho'(T)] for
+   [rho'] being [rho;mi:=d].
+
+   In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma].
+*)
 let clenv_fchain mv clenv nextclenv =
   (* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
   let clenv' =
@@ -422,7 +455,7 @@ let make_clenv_binding_gen n gls (c,t) = function
   | NoBindings ->
       mk_clenv_from_n gls n (c,t)
 
-let make_clenv_binding_apply wc n = make_clenv_binding_gen (Some n) wc
+let make_clenv_binding_apply gls n = make_clenv_binding_gen (Some n) gls
 let make_clenv_binding = make_clenv_binding_gen None
 
 (****************************************************************)
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index b1f08a6916..53a106ade5 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -105,12 +105,27 @@ val make_clenv_binding_apply :
 val make_clenv_binding :
   evar_info sigma -> constr * constr -> constr Rawterm.bindings -> clausenv
 
-(* other stuff *)
+(* [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where
+   [lmetas] is a list of metas to be applied to a proof of [t] so that
+   it produces the unification pattern [ccl]; [sigma'] is [sigma]
+   extended with [lmetas]; if [n] is defined, it limits the size of
+   the list even if [ccl] is still a product; otherwise, it stops when
+   [ccl] is not a product; example: if [t] is [forall x y, x=y -> y=x]
+   and [n] is [None], then [lmetas] is [Meta n1;Meta n2;Meta n3] and
+   [ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1]
+   and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *)
 val clenv_environments :
  evar_defs -> int option -> types -> evar_defs * constr list * types
+
+(* [clenv_environments_evars env sigma n t] does the same but returns
+   a list of Evar's defined in [env] and extends [sigma] accordingly *)
 val clenv_environments_evars :
  env -> evar_defs -> int option -> types -> evar_defs * constr list * types
 
+(* if the clause is a product, add an extra meta for this product *)
+exception NotExtensibleClause
+val clenv_push_prod : clausenv -> clausenv
+
 (***************************************************************)
 (* Pretty-print *)
 val pr_clenv : clausenv -> Pp.std_ppcmds
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 9d376a7388..52fa2a8607 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -399,3 +399,9 @@ VERNAC COMMAND EXTEND ImplicitTactic
 | [ "Declare" "Implicit" "Tactic" tactic(tac) ] ->
     [ Tacinterp.declare_implicit_tactic (Tacinterp.interp tac) ]
 END
+
+TACTIC EXTEND apply_in
+| ["apply" constr_with_bindings(c) "in" hyp(id) ] -> [ apply_in id [c] ]
+| ["apply" constr_with_bindings(c) "," constr_with_bindings_list_sep(cl,",") 
+   "in" hyp(id) ] -> [ apply_in id (c::cl) ]
+END
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2befb7e42e..d0e8645453 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -447,12 +447,9 @@ let rec intros_rmove = function
  		    move_to_rhyp destopt;
 		    intros_rmove rest ]
 
-(****************************************************)
-(*            Resolution tactics                    *)
-(****************************************************)
-
-(*  Refinement tactic: unification with the head of the head normal form
- *  of the type of a term. *)
+(**************************)
+(*  Refinement tactics    *)
+(**************************)
 
 let apply_type hdcty argl gl =
   refine (applist (mkCast (Evarutil.mk_new_meta(),DEFAULTcast, hdcty),argl)) gl
@@ -468,6 +465,48 @@ let bring_hyps hyps =
       let f = mkCast (Evarutil.mk_new_meta(),DEFAULTcast, newcl) in
       refine_no_check (mkApp (f, instance_from_named_context hyps)) gl)
 
+(**************************)
+(*     Cut tactics        *)
+(**************************)
+
+let cut c gl =
+  match kind_of_term (hnf_type_of gl c) with
+    | Sort _ ->
+        let id=next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
+        let t = mkProd (Anonymous, c, pf_concl gl) in
+          tclTHENFIRST
+            (internal_cut_rev id c)
+            (tclTHEN (apply_type t [mkVar id]) (thin [id]))
+            gl
+    | _  -> error "Not a proposition or a type"
+
+let cut_intro t = tclTHENFIRST (cut t) intro
+
+(* let cut_replacing id t tac = 
+  tclTHENS (cut t)
+    [tclORELSE
+	(intro_replacing id) 
+	(tclORELSE (intro_erasing id) (intro_using id));
+     tac (refine_no_check (mkVar id)) ] *)
+
+(* cut_replacing échoue si l'hypothèse à remplacer apparaît dans le
+   but, ou dans une autre hypothèse *)
+let cut_replacing id t tac = 
+  tclTHENS (cut t) [
+      tclORELSE (intro_replacing id) (intro_erasing id); 
+      tac (refine_no_check (mkVar id)) ]
+
+let cut_in_parallel l = 
+  let rec prec = function
+    | [] -> tclIDTAC 
+    | h::t -> tclTHENFIRST (cut h) (prec t)
+  in 
+    prec (List.rev l)
+
+(****************************************************)
+(*            Resolution tactics                    *)
+(****************************************************)
+
 (* Resolution with missing arguments *)
 
 let apply_with_bindings (c,lbind) gl = 
@@ -490,7 +529,7 @@ let apply_with_bindings (c,lbind) gl =
   with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) ->
     (* Last chance: if the head is a variable, apply may try
        second order unification *)
-    let clause = make_clenv_binding_apply gl (-1) (c,thm_ty0) lbind in 
+    let clause = make_clenv_binding gl (c,thm_ty0) lbind in 
     Clenvtac.res_pf clause gl
 
 let apply c = apply_with_bindings (c,NoBindings)
@@ -505,6 +544,44 @@ let apply_without_reduce c gl =
   let clause = mk_clenv_type_of gl c in 
   res_pf clause gl
 
+(* [apply_in hyp c] replaces
+
+   hyp : forall y1, ti -> t             hyp : rho(u)
+   ========================    with     ============  and the =======
+   goal                                 goal                  rho(ti)
+
+   assuming that [c] has type [forall x1..xn -> t' -> u] for some [t]
+   unifiable with [t'] with unifier [rho]
+*)
+
+let find_matching_clause unifier clause =
+  let rec find clause =
+    try unifier clause
+    with exn when catchable_exception exn ->
+    try find (clenv_push_prod clause)
+    with NotExtensibleClause -> error "Cannot apply"
+  in find clause
+
+let apply_in_once gls innerclause (d,lbind) =
+  let thm = nf_betaiota (pf_type_of gls d) in
+  let clause = make_clenv_binding gls (d,thm) lbind in
+  let ordered_metas = List.rev (clenv_independent clause) in
+  if ordered_metas = [] then error "Statement without assumptions";
+  let f mv = find_matching_clause (clenv_fchain mv clause) innerclause in
+  try list_try_find f ordered_metas
+  with Failure _ -> error "Unable to unify"
+
+let apply_in id lemmas gls =
+  let t' = pf_get_hyp_typ gls id in
+  let innermostclause = mk_clenv_from_n gls (Some 0) (mkVar id,t') in
+  let clause = List.fold_left (apply_in_once gls) innermostclause lemmas in
+  let new_hyp_prf  = clenv_value clause in
+  let new_hyp_typ  = clenv_type clause in
+  tclTHEN
+    (tclEVARS (evars_of clause.env))
+    (cut_replacing id new_hyp_typ
+      (fun x gls -> refine_no_check new_hyp_prf gls)) gls
+
 (* A useful resolution tactic which, if c:A->B, transforms |- C into
    |- B -> C and |- A
 
@@ -522,10 +599,6 @@ let apply_without_reduce c gl =
   end.
 *)
 
-(**************************)
-(*     Cut tactics        *)
-(**************************)
-
 let cut_and_apply c gl =
   let goal_constr = pf_concl gl in 
     match kind_of_term (pf_hnf_constr gl (pf_type_of gl c)) with
@@ -535,40 +608,6 @@ let cut_and_apply c gl =
 	    (apply_term c [mkMeta (new_meta())]) gl
       | _ -> error "Imp_elim needs a non-dependent product"
 
-let cut c gl =
-  match kind_of_term (hnf_type_of gl c) with
-    | Sort _ ->
-        let id=next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
-        let t = mkProd (Anonymous, c, pf_concl gl) in
-          tclTHENFIRST
-            (internal_cut_rev id c)
-            (tclTHEN (apply_type t [mkVar id]) (thin [id]))
-            gl
-    | _  -> error "Not a proposition or a type"
-
-let cut_intro t = tclTHENFIRST (cut t) intro
-
-(* let cut_replacing id t tac = 
-  tclTHENS (cut t)
-    [tclORELSE
-	(intro_replacing id) 
-	(tclORELSE (intro_erasing id) (intro_using id));
-     tac (refine_no_check (mkVar id)) ] *)
-
-(* cut_replacing échoue si l'hypothèse à remplacer apparaît dans le
-   but, ou dans une autre hypothèse *)
-let cut_replacing id t tac = 
-  tclTHENS (cut t) [
-      tclORELSE (intro_replacing id) (intro_erasing id); 
-      tac (refine_no_check (mkVar id)) ]
-
-let cut_in_parallel l = 
-  let rec prec = function
-    | [] -> tclIDTAC 
-    | h::t -> tclTHENFIRST (cut h) (prec t)
-  in 
-    prec (List.rev l)
-
 (********************************************************************)
 (*               Exact tactics                                      *)
 (********************************************************************)
@@ -774,6 +813,14 @@ let elim (c,lbindc as cx) elim =
 let simplest_elim c = default_elim (c,NoBindings)
 
 (* Elimination in hypothesis *)
+(* Typically, elimclause := (eq_ind ?x ?P ?H ?y ?Heq : ?P ?y)
+              indclause : forall ..., hyps -> a=b    (to take place of ?Heq)
+              id : phi(a)                            (to take place of ?H)
+      and the result is to overwrite id with the proof of phi(b)
+
+   but this generalizes to any elimination scheme with one constructor
+   (e.g. it could replace id:A->B->C by id:C, knowing A/\B)
+*)
 
 let elimination_in_clause_scheme id elimclause indclause gl =
   let (hypmv,indmv) = 
@@ -784,8 +831,7 @@ let elimination_in_clause_scheme id elimclause indclause gl =
   let elimclause'  = clenv_fchain indmv elimclause indclause in 
   let hyp = mkVar id in
   let hyp_typ = pf_type_of gl hyp in
-  let hypclause =
-    mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in
+  let hypclause = mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in
   let elimclause'' = clenv_fchain hypmv elimclause' hypclause in  
   let new_hyp_prf  = clenv_value elimclause'' in
   let new_hyp_typ  = clenv_type elimclause'' in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 9411a772bf..c1b8782b3a 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -169,6 +169,8 @@ val apply_with_bindings   : constr with_bindings -> tactic
 
 val cut_and_apply         : constr -> tactic
 
+val apply_in              : identifier -> constr with_bindings list -> tactic
+
 (*s Elimination tactics. *)