Ajout d'un suffixe "as [ names ]" pour nommer manuellement les

variables introduites par NewDestruct et NewInduction


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

10 files changed, 106 insertions, 88 deletions

diff --git a/CHANGES b/CHANGES
index 1519fca56c..70bff3ebe0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -51,6 +51,7 @@ Tactics
   for Intros until)
 - NewDestruct now accepts terms with missing hypotheses
 - NewDestruct and NewInduction now accept user-provided elimination scheme
+- NewDestruct and NewInduction now accept user-provided introduction names
 - Omega could solve goals such as ~`x<y` |- `x>=y` but failed when the
   hypothesis was unfolded to `x < y` -> False. This is fixed. In addition,
   it can also recognize 'False' in the hypothesis and use it to solve the
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index ef4d614612..2866423759 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -240,6 +240,10 @@ GEXTEND Gram
   eliminator:
     [ [ "using"; el = constr_with_bindings -> el ] ]
   ;
+  with_names:
+    [ [ "as"; "["; ids = LIST1 (LIST0 Prim.ident) SEP "|"; "]" -> ids
+      | -> [] ] ]
+  ;
   simple_tactic:
     [ [ 
       (* Basic tactics *)
@@ -294,13 +298,13 @@ GEXTEND Gram
 
       (* Derived basic tactics *)
       | IDENT "Induction"; h = quantified_hypothesis -> TacOldInduction h
-      | IDENT "NewInduction"; c = induction_arg; el = OPT eliminator ->
-          TacNewInduction (c,el)
+      | IDENT "NewInduction"; c = induction_arg; el = OPT eliminator;
+          ids = with_names -> TacNewInduction (c,el,ids)
       | IDENT "Double"; IDENT "Induction"; h1 = quantified_hypothesis;
 	  h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
       | IDENT "Destruct"; h = quantified_hypothesis -> TacOldDestruct h
-      | IDENT "NewDestruct"; c = induction_arg; el = OPT eliminator ->
-          TacNewDestruct (c,el)
+      | IDENT "NewDestruct"; c = induction_arg; el = OPT eliminator; 
+          ids = with_names -> TacNewDestruct (c,el,ids)
       | IDENT "Decompose"; IDENT "Record" ; c = constr -> TacDecomposeAnd c
       | IDENT "Decompose"; IDENT "Sum"; c = constr -> TacDecomposeOr c
       | IDENT "Decompose"; "["; l = LIST1 qualid_or_ltac_ref; "]"; c = constr
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index e0f8bd3f1e..2abdc68138 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -99,6 +99,12 @@ let pr_bindings prc = function
 
 let pr_with_bindings prc (c,bl) = prc c ++ hv 0 (pr_bindings prc bl)
 
+let pr_with_names = function
+  | [] -> mt ()
+  | ids -> spc () ++ str "as [" ++
+      hv 0 (prlist_with_sep (fun () -> spc () ++ str "| ")
+              (prlist_with_sep spc pr_id) ids ++ str "]")
+
 let rec pr_intro_pattern = function
   | IntroOrAndPattern pll ->
       str "[" ++
@@ -383,14 +389,14 @@ and pr_atom1 = function
   (* Derived basic tactics *)
   | TacOldInduction h ->
       hov 1 (str "Induction" ++ pr_arg pr_quantified_hypothesis h)
-  | TacNewInduction (h,e) ->
+  | TacNewInduction (h,e,ids) ->
       hov 1 (str "NewInduction" ++ spc () ++ pr_induction_arg pr_constr h ++
-        pr_opt pr_eliminator e)
+        pr_opt pr_eliminator e ++ pr_with_names ids)
   | TacOldDestruct h ->
       hov 1 (str "Destruct" ++ pr_arg pr_quantified_hypothesis h)
-  | TacNewDestruct (h,e) ->
+  | TacNewDestruct (h,e,ids) ->
       hov 1 (str "NewDestruct" ++ spc () ++ pr_induction_arg pr_constr h ++
-        pr_opt pr_eliminator e)
+        pr_opt pr_eliminator e ++ pr_with_names ids)
   | TacDoubleInduction (h1,h2) ->
       hov 1
         (str "Double Induction" ++ 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index ac97261065..086eed8a52 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -355,14 +355,16 @@ let rec mlexpr_of_atomic_tactic = function
   (* Derived basic tactics *)
   | Tacexpr.TacOldInduction h ->
       <:expr< Tacexpr.TacOldInduction $mlexpr_of_quantified_hypothesis h$ >>
-  | Tacexpr.TacNewInduction (c,cbo) ->
+  | Tacexpr.TacNewInduction (c,cbo,ids) ->
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
-      <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ >>
+      let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_ident) ids in
+      <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ $ids$>>
   | Tacexpr.TacOldDestruct h ->
       <:expr< Tacexpr.TacOldDestruct $mlexpr_of_quantified_hypothesis h$ >>
-  | Tacexpr.TacNewDestruct (c,cbo) ->
+  | Tacexpr.TacNewDestruct (c,cbo,ids) ->
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
-      <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ >>
+      let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_ident) ids in
+      <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ $ids$ >>
 
   (* Context management *)
   | Tacexpr.TacClear l ->
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 3eaaea5739..a1d7ff16b7 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -117,8 +117,10 @@ type ('constr,'cst,'ind,'id) gen_atomic_tactic_expr =
   (* Derived basic tactics *)
   | TacOldInduction of quantified_hypothesis
   | TacNewInduction of 'constr induction_arg * 'constr with_bindings option
+      * identifier list list
   | TacOldDestruct of quantified_hypothesis
   | TacNewDestruct of 'constr induction_arg * 'constr with_bindings option
+      * identifier list list
 
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
   | TacDecomposeAnd of 'constr
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index a5496f91d4..1fcf1e6bd0 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -52,10 +52,10 @@ let h_instantiate n c =
 (* Derived basic tactics *)
 let h_old_induction h = abstract_tactic (TacOldInduction h) (old_induct h)
 let h_old_destruct h  = abstract_tactic (TacOldDestruct h) (old_destruct h)
-let h_new_induction c e =
-  abstract_tactic (TacNewInduction (c,e)) (new_induct c e)
-let h_new_destruct c e =
-  abstract_tactic (TacNewDestruct (c,e)) (new_destruct c e)
+let h_new_induction c e idl =
+  abstract_tactic (TacNewInduction (c,e,idl)) (new_induct c e idl)
+let h_new_destruct c e idl =
+  abstract_tactic (TacNewDestruct (c,e,idl)) (new_destruct c e idl)
 let h_specialize n (c,bl as d) =
   abstract_tactic (TacSpecialize (n,d)) (new_hyp n c bl)
 let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c)
@@ -94,29 +94,7 @@ let h_symmetry       = abstract_tactic TacSymmetry intros_symmetry
 let h_transitivity c =
   abstract_tactic (TacTransitivity c) (intros_transitivity c)
 
-(*
-let h_clear ids         = v_clear  [(Clause (List.map (fun x -> InHyp x) ids))]
-let h_move dep id1 id2  = 
- (if dep then v_move else v_move_dep) [Identifier id1;Identifier id2]
-let h_reflexivity       = v_reflexivity   []
-let h_symmetry          = v_symmetry      []
-let h_one_constructor i = v_constructor [(Integer i)]
-let h_any_constructor   = v_constructor []
-let h_transitivity c    = v_transitivity [(Constr c)]
-let h_simplest_left     = v_left [(Cbindings [])]
-let h_simplest_right    = v_right [(Cbindings [])]
-let h_split     c       = v_split [(Constr c);(Cbindings [])]
-*)
-
 let h_simplest_apply c  = h_apply (c,NoBindings)
 let h_simplest_elim c   = h_elim (c,NoBindings) None
-(*
-let h_inductionInt  i   = v_induction[(Integer i)]
-let h_inductionId   id  = v_induction[(Identifier id)]
-*)
 let h_simplest_case   c = h_case (c,NoBindings)
-(*
-let h_destructInt  i    = v_destruct [(Integer i)]
-let h_destructId   id   = v_destruct [(Identifier id)]
-*)
 
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 6b4a1cbc15..797315d642 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -56,9 +56,11 @@ val h_instantiate     : int -> constr -> tactic
 val h_old_induction   : quantified_hypothesis -> tactic
 val h_old_destruct    : quantified_hypothesis -> tactic
 val h_new_induction   :
-  constr induction_arg -> constr with_bindings option -> tactic
+  constr induction_arg -> constr with_bindings option ->
+    identifier list list -> tactic
 val h_new_destruct    :
-  constr induction_arg -> constr with_bindings option -> tactic
+  constr induction_arg -> constr with_bindings option -> 
+    identifier list list -> tactic
 val h_specialize      : int option -> constr with_bindings -> tactic
 val h_lapply          : constr -> tactic
 
@@ -95,18 +97,6 @@ val h_reflexivity     : tactic
 val h_symmetry        : tactic
 val h_transitivity    : constr -> tactic
 
-(*
-val h_reflexivity     : tactic
-val h_symmetry        : tactic
-val h_transitivity    : constr -> tactic
-*)
 val h_simplest_apply  : constr -> tactic 
 val h_simplest_elim   : constr -> tactic
 val h_simplest_case   : constr -> tactic
-(*
-val h_inductionInt    : int -> tactic 
-val h_inductionId     : identifier -> tactic 
-val h_destructInt     : int -> tactic
-val h_destructId      : identifier -> tactic
-*)
-
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index afc77834d2..568ffd021d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -503,13 +503,15 @@ let rec glob_atomic lf ist = function
 
   (* Derived basic tactics *)
   | TacOldInduction h -> TacOldInduction (glob_quantified_hypothesis ist h)
-  | TacNewInduction (c,cbo) ->
+  | TacNewInduction (c,cbo,ids) ->
       TacNewInduction (glob_induction_arg ist c,
-               option_app (glob_constr_with_bindings ist) cbo)
+               option_app (glob_constr_with_bindings ist) cbo,
+               List.map (List.map (glob_ident lf ist)) ids)
   | TacOldDestruct h -> TacOldDestruct (glob_quantified_hypothesis ist h)
-  | TacNewDestruct (c,cbo) ->
+  | TacNewDestruct (c,cbo,ids) ->
       TacNewDestruct (glob_induction_arg ist c,
-               option_app (glob_constr_with_bindings ist) cbo)
+               option_app (glob_constr_with_bindings ist) cbo,
+               List.map (List.map (glob_ident lf ist)) ids)
   | TacDoubleInduction (h1,h2) ->
       let h1 = glob_quantified_hypothesis ist h1 in
       let h2 = glob_quantified_hypothesis ist h2 in
@@ -1638,13 +1640,15 @@ and interp_atomic ist = function
 
   (* Derived basic tactics *)
   | TacOldInduction h -> h_old_induction (interp_quantified_hypothesis ist h)
-  | TacNewInduction (c,cbo) ->
+  | TacNewInduction (c,cbo,ids) ->
       h_new_induction (interp_induction_arg ist c)
         (option_app (interp_constr_with_bindings ist) cbo)
+        (List.map (List.map (ident_interp ist)) ids)
   | TacOldDestruct h -> h_old_destruct (interp_quantified_hypothesis ist h)
-  | TacNewDestruct (c,cbo) -> 
+  | TacNewDestruct (c,cbo,ids) -> 
       h_new_destruct (interp_induction_arg ist c)
         (option_app (interp_constr_with_bindings ist) cbo)
+        (List.map (List.map (ident_interp ist)) ids)
   | TacDoubleInduction (h1,h2) ->
       let h1 = interp_quantified_hypothesis ist h1 in
       let h2 = interp_quantified_hypothesis ist h2 in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2c589f07fa..bea28226b0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1001,6 +1001,12 @@ let general_elim_in id (c,lbindc) (elimc,lbindelimc) gl =
 
  *)
 
+let check_unused_names names =
+  if names <> [] & Options.is_verbose () then
+    let s,are = if List.tl names = [] then " "," is" else "s "," are" in
+    let names = String.concat " " (List.map string_of_id names) in
+    warning ("Name"^s^names^are^" unused")
+
 (* We recompute recargs because we are not sure the elimination lemma
 comes from a canonically generated one *)
 (* dead code ?
@@ -1017,7 +1023,8 @@ let rec recargs indpath env sigma t =
 	::(recargs indpath (push_rel_assum (na,t) env) sigma c2)
     | _ -> []
 *)
-let induct_discharge old_style mind statuslists cname destopt avoid ra gl =
+let induct_discharge old_style mind statuslists cname destopt avoid ra names gl
+  =
   let (lstatus,rstatus) = statuslists in
   let tophyp = ref None in
   let n = List.fold_left (fun n b -> if b then n+1 else n) 0 ra in
@@ -1054,30 +1061,43 @@ let induct_discharge old_style mind statuslists cname destopt avoid ra gl =
           else avoid in
       cname, hyprecname, avoid
   in
-  let rec peel_tac = function
+  let rec peel_tac ra names gl = match ra with
     | true :: ra' ->
 		 (* For lstatus but _buggy_: if intro_gen renames
 		    hyprecname differently (because it already exists
 		    in goal, then hypothesis associated to None in
 		    lstatus will be moved at a wrong place *)
-	if !tophyp=None then
-	  tophyp := Some (next_ident_away hyprecname avoid);
+        let recvar,hyprec,names = match names with
+          | [] ->
+              next_ident_away recvarname avoid,
+              next_ident_away hyprecname avoid,
+              []
+          | [id] ->
+              id, next_ident_away (add_prefix "IH" id) avoid, []
+          | id1::id2::names -> (id1,id2,names) in
+	if !tophyp=None then tophyp := Some hyprec;
         tclTHENLIST
-	  [ intro_gen (IntroBasedOn (recvarname,avoid)) destopt false;
-	    intro_gen (IntroBasedOn (hyprecname,avoid)) None false;
-	    peel_tac ra']
+	  [ intro_gen (IntroMustBe (recvar)) destopt false;
+	    intro_gen (IntroMustBe (hyprec)) None false;
+	    peel_tac ra' names ] gl
     | false :: ra' ->
-	tclTHEN (intro_gen (IntroAvoid avoid) destopt false)
-	  (peel_tac ra')
-    | [] -> tclIDTAC
+        let introstyle,names = match names with
+          | [] -> IntroAvoid avoid, []
+          | id::names -> IntroMustBe id,names in
+	tclTHEN (intro_gen introstyle destopt false)
+	  (peel_tac ra' names) gl
+    | [] ->
+        check_unused_names names;
+        tclIDTAC gl
   in
-  let evaluated_peel_tac = peel_tac ra in (* because side effect on tophyp *)
-  let newlstatus = (* if some IH has taken place at the top of hyps *)
-    List.map (function (hyp,None) -> (hyp,!tophyp) | x -> x) lstatus
+  let intros_move lstatus =
+    let newlstatus = (* if some IH has taken place at the top of hyps *)
+      List.map (function (hyp,None) -> (hyp,!tophyp) | x -> x) lstatus in
+    intros_move newlstatus
   in 
-  tclTHENLIST [ evaluated_peel_tac;
+  tclTHENLIST [ peel_tac ra names;
 		intros_rmove rstatus;
-		intros_move newlstatus ] gl
+		intros_move lstatus ] gl
 
 (* - le recalcul de indtyp à chaque itération de atomize_one est pour ne pas
      s'embêter à regarder si un letin_tac ne fait pas des
@@ -1249,6 +1269,13 @@ let induction_tac varname typ (elimc,elimt,lbindelimc) gl =
     make_clenv_binding wc (mkCast (elimc,elimt),elimt) lbindelimc in
   elimination_clause_scheme kONT elimclause indclause gl
 
+let compute_induction_names n names =
+  let names = if names = [] then Array.make n [] else Array.of_list names in
+  if Array.length names <> n then
+    errorlabstrm "induction_from_context"
+      (str "Expect " ++ int n ++ str " lists of names");
+  names
+
 let is_indhyp p n t =
   let c,_ = decompose_app t in 
   match kind_of_term c with
@@ -1283,7 +1310,7 @@ let compute_elim_signature_and_roughly_check elimt mind =
   let _,elimt3 = decompose_prod_n npred elimt2 in
   Array.of_list (check_elim elimt3 0)
 
-let induction_from_context isrec style elim hyp0 gl =
+let induction_from_context isrec style elim hyp0 names gl =
   (*test suivant sans doute inutile car refait par le letin_tac*)
   if List.mem hyp0 (ids_of_named_context (Global.named_context())) then
     errorlabstrm "induction" 
@@ -1305,6 +1332,7 @@ let induction_from_context isrec style elim hyp0 gl =
   let (statlists,lhyp0,indhyps,deps) = cook_sign hyp0 indvars env in
   let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in
   let lr = compute_elim_signature_and_roughly_check elimt mind in
+  let names = compute_induction_names (Array.length lr) names in
   let dephyps = List.map (fun (id,_,_) -> id) deps in
   let args =
     List.fold_left
@@ -1329,39 +1357,40 @@ let induction_from_context isrec style elim hyp0 gl =
        	(tclTHEN
 	   (induction_tac hyp0 typ0 (elimc,elimt,lbindelimc))
 	   (thin (hyp0::indhyps)))
-       	(Array.map
+       	(array_map2
 	   (induct_discharge style mind statlists hyp0 lhyp0
-              (List.rev dephyps)) lr)
+              (List.rev dephyps)) lr names)
     ]
     gl
 
-let induction_with_atomization_of_ind_arg isrec elim hyp0 =
+let induction_with_atomization_of_ind_arg isrec elim names hyp0 =
   tclTHEN
     (atomize_param_of_ind hyp0)
-    (induction_from_context isrec false elim hyp0)
+    (induction_from_context isrec false elim hyp0 names)
 
 (* This is Induction since V7 ("natural" induction both in quantified
    premisses and introduced ones) *)
-let new_induct_gen isrec elim c gl =
+let new_induct_gen isrec elim names c gl =
   match kind_of_term c with
     | Var id when not (mem_named_context id (Global.named_context())) ->
-	induction_with_atomization_of_ind_arg isrec elim id gl
+	induction_with_atomization_of_ind_arg isrec elim names id gl
     | _        ->
 	let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) 
 		  Anonymous in
 	let id = fresh_id [] x gl in
 	tclTHEN
 	  (letin_tac true (Name id) c (None,[]))
-	  (induction_with_atomization_of_ind_arg isrec elim id) gl
+	  (induction_with_atomization_of_ind_arg isrec elim names id) gl
 
-let new_induct_destruct isrec c elim = match c with
-  | ElimOnConstr c -> new_induct_gen isrec elim c
+let new_induct_destruct isrec c elim names = match c with
+  | ElimOnConstr c -> new_induct_gen isrec elim names c
   | ElimOnAnonHyp n ->
-      tclTHEN (intros_until_n n) (tclLAST_HYP (new_induct_gen isrec elim))
+      tclTHEN (intros_until_n n)
+        (tclLAST_HYP (new_induct_gen isrec elim names))
   (* Identifier apart because id can be quantified in goal and not typable *)
   | ElimOnIdent (_,id) ->
       tclTHEN (tclTRY (intros_until_id id))
-        (new_induct_gen isrec elim (mkVar id))
+        (new_induct_gen isrec elim names (mkVar id))
 
 let new_induct = new_induct_destruct true
 let new_destruct = new_induct_destruct false
@@ -1377,7 +1406,7 @@ let raw_induct_nodep n = tclTHEN (intros_until_n n) (tclLAST_HYP simplest_elim)
 
 (* This was Induction in 6.3 (hybrid form) *)
 let old_induct_id s =
-  tclORELSE (raw_induct s) (induction_from_context true true None s)
+  tclORELSE (raw_induct s) (induction_from_context true true None s [])
 let old_induct_nodep = raw_induct_nodep
 
 let old_induct = function
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 8dd0e34740..ce31a4dcc7 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -171,7 +171,8 @@ val old_induct     : quantified_hypothesis -> tactic
 val general_elim_in : identifier -> constr * constr substitution ->
                       constr * constr substitution -> tactic
 
-val new_induct : constr induction_arg -> constr with_bindings option -> tactic
+val new_induct : constr induction_arg -> constr with_bindings option ->
+  identifier list list -> tactic
 
 (*s Case analysis tactics. *)
 
@@ -179,7 +180,8 @@ val general_case_analysis : constr with_bindings ->  tactic
 val simplest_case         : constr -> tactic
 
 val old_destruct          : quantified_hypothesis -> tactic
-val new_destruct : constr induction_arg -> constr with_bindings option ->tactic
+val new_destruct : constr induction_arg -> constr with_bindings option ->
+  identifier list list -> tactic
 
 (*s Eliminations giving the type instead of the proof. *)