Experimentally adding an option for automatically erasing an

hypothesis when using it in apply or rewrite (prefix ">",
undocumented), and a modifier to explicitly keep it in induction or
destruct (prefix "!", reminiscent of non-linerarity).

Also added undocumented option "Set Default Clearing Used Hypotheses"
which makes apply and rewrite default to erasing the hypothesis they
use (if ever their argument is indeed an hypothesis of the context).

1 files changed, 132 insertions, 71 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cb6894fefa..2de4e26f3f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -99,6 +99,19 @@ let _ = Goptions.declare_bool_option {
   Goptions.optwrite = (fun a -> apply_solve_class_goals:=a);
 }
 
+let clear_hyp_by_default = ref false
+
+let use_clear_hyp_by_default () = !clear_hyp_by_default
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "default clearing of hypotheses after use";
+      optkey   = ["Default";"Clearing";"Used";"Hypotheses"];
+      optread  = (fun () -> !clear_hyp_by_default) ;
+      optwrite = (fun b -> clear_hyp_by_default := b) }
+
 (*********************************************)
 (*                 Tactics                   *)
 (*********************************************)
@@ -159,6 +172,16 @@ let thin l gl =
   with Evarutil.ClearDependencyError (id,err) ->
     error_clear_dependency (pf_env gl) id err
 
+let apply_clear_request clear_flag dft c =
+  let check_isvar c =
+    if not (isVar c) then
+      error "keep/clear modifiers apply only to hypothesis names." in
+  let clear = match clear_flag with
+    | None -> dft && isVar c
+    | Some clear -> check_isvar c; clear in
+  if clear then Proofview.V82.tactic (thin [destVar c])
+  else Tacticals.New.tclIDTAC
+
 let internal_cut_gen b d t gl =
   try internal_cut b d t gl
   with Evarutil.ClearDependencyError (id,err) ->
@@ -167,8 +190,8 @@ let internal_cut_gen b d t gl =
 let internal_cut = internal_cut_gen false
 let internal_cut_replace = internal_cut_gen true
 
-let internal_cut_rev_gen b d t gl =
-  try internal_cut_rev b d t gl
+let internal_cut_rev_gen b id t gl =
+  try internal_cut_rev b id t gl
   with Evarutil.ClearDependencyError (id,err) ->
     error_clear_dependency (pf_env gl) id err
 
@@ -678,31 +701,36 @@ let rec intros_move = function
    or a term with bindings *)
 
 let onOpenInductionArg tac = function
-  | ElimOnConstr cbl ->
-      tac cbl
-  | ElimOnAnonHyp n ->
+  | clear_flag,ElimOnConstr cbl ->
+      tac clear_flag cbl
+  | clear_flag,ElimOnAnonHyp n ->
       Tacticals.New.tclTHEN
         (intros_until_n n)
-        (Tacticals.New.onLastHyp (fun c -> tac (Evd.empty,(c,NoBindings))))
-  | ElimOnIdent (_,id) ->
+        (Tacticals.New.onLastHyp
+           (fun c -> tac clear_flag (Evd.empty,(c,NoBindings))))
+  | clear_flag,ElimOnIdent (_,id) ->
       (* A quantified hypothesis *)
       Tacticals.New.tclTHEN
         (try_intros_until_id_check id)
-        (tac (Evd.empty,(mkVar id,NoBindings)))
+        (tac clear_flag (Evd.empty,(mkVar id,NoBindings)))
 
 let onInductionArg tac = function
-  | ElimOnConstr cbl ->
-      tac cbl
-  | ElimOnAnonHyp n ->
-      Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHyp (fun c -> tac (c,NoBindings)))
-  | ElimOnIdent (_,id) ->
+  | clear_flag,ElimOnConstr cbl ->
+      tac clear_flag cbl
+  | clear_flag,ElimOnAnonHyp n ->
+      Tacticals.New.tclTHEN
+        (intros_until_n n)
+        (Tacticals.New.onLastHyp (fun c -> tac clear_flag (c,NoBindings)))
+  | clear_flag,ElimOnIdent (_,id) ->
       (* A quantified hypothesis *)
-      Tacticals.New.tclTHEN (try_intros_until_id_check id) (tac (mkVar id,NoBindings))
+      Tacticals.New.tclTHEN
+        (try_intros_until_id_check id)
+        (tac clear_flag (mkVar id,NoBindings))
 
 let map_induction_arg f = function
-  | ElimOnConstr (sigma,(c,bl)) -> ElimOnConstr (f (sigma,c),bl)
-  | ElimOnAnonHyp n -> ElimOnAnonHyp n
-  | ElimOnIdent id -> ElimOnIdent id
+  | clear_flag,ElimOnConstr (sigma,(c,bl)) -> clear_flag,ElimOnConstr (f (sigma,c),bl)
+  | clear_flag,ElimOnAnonHyp n as x -> x
+  | clear_flag,ElimOnIdent id as x -> x
 
 (**************************)
 (*     Cut tactics        *)
@@ -782,13 +810,19 @@ let check_unresolved_evars_of_metas clenv =
   | _ -> ())
   (meta_list clenv.evd)
 
+let clear_of_flag flag =
+  match flag with
+  | None -> true (* default for apply in *)
+  | Some b -> b
+
 (* For a clenv expressing some lemma [C[?1:T1,...,?n:Tn] : P] and some
    goal [G], [clenv_refine_in] returns [n+1] subgoals, the [n] last
    ones (resp [n] first ones if [sidecond_first] is [true]) being the
    [Ti] and the first one (resp last one) being [G] whose hypothesis
    [id] is replaced by P using the proof given by [tac] *)
 
-let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) id clenv gl =
+let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) clear_flag id clenv gl =
+  let with_clear = clear_of_flag clear_flag in
   let clenv = Clenvtac.clenv_pose_dependent_evars with_evars clenv in
   let clenv =
     if with_classes then
@@ -800,10 +834,15 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) id c
   if not with_evars && occur_meta new_hyp_typ then
     error_uninstantiated_metas new_hyp_typ clenv;
   let new_hyp_prf = clenv_value clenv in
+  let id' = if with_clear then id else fresh_id [] id gl in
+  let exact_tac = refine_no_check new_hyp_prf in
   tclTHEN
     (tclEVARS clenv.evd)
-    ((if sidecond_first then assert_replacing else cut_replacing)
-      id new_hyp_typ (refine_no_check new_hyp_prf)) gl
+    (if sidecond_first then
+       tclTHENFIRST (internal_cut_gen with_clear id' new_hyp_typ) exact_tac
+     else
+       tclTHENLAST (internal_cut_rev_gen with_clear id' new_hyp_typ) exact_tac)
+    gl
 
 (********************************************)
 (*       Elimination tactics                *)
@@ -900,16 +939,20 @@ let general_elim_clause_gen elimtac indclause elim gl =
     match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in
   elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause gl
 
-let general_elim with_evars (c, lbindc) elim gl =
+let general_elim with_evars clear_flag (c, lbindc) elim gl =
   let ct = pf_type_of gl c in
   let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
   let elimtac = elimination_clause_scheme with_evars in
   let indclause  = pf_apply make_clenv_binding gl (c, t) lbindc in
-  general_elim_clause_gen elimtac indclause elim gl
+  tclTHEN
+    (general_elim_clause_gen elimtac indclause elim)
+    (Proofview.V82.of_tactic
+       (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
+    gl
 
 (* Case analysis tactics *)
 
-let general_case_analysis_in_context with_evars (c,lbindc) gl =
+let general_case_analysis_in_context with_evars clear_flag (c,lbindc) gl =
   let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
   let sort = elimination_sort_of_goal gl in
   let sigma, elim =
@@ -918,19 +961,21 @@ let general_case_analysis_in_context with_evars (c,lbindc) gl =
     else
       pf_apply build_case_analysis_scheme_default gl mind sort in
   tclTHEN (tclEVARS sigma)
-  (general_elim with_evars (c,lbindc)
+  (general_elim with_evars clear_flag (c,lbindc)
    {elimindex = None; elimbody = (elim,NoBindings);
     elimrename = Some (false, constructors_nrealdecls (fst mind))}) gl
 
-let general_case_analysis with_evars (c,lbindc as cx) =
+let general_case_analysis with_evars clear_flag (c,lbindc as cx) =
   match kind_of_term c with
     | Var id when lbindc == NoBindings ->
 	Tacticals.New.tclTHEN (try_intros_until_id_check id)
-	  (Proofview.V82.tactic (general_case_analysis_in_context with_evars cx))
+	  (Proofview.V82.tactic
+             (general_case_analysis_in_context with_evars clear_flag cx))
     | _ ->
-	Proofview.V82.tactic (general_case_analysis_in_context with_evars cx)
+	Proofview.V82.tactic
+          (general_case_analysis_in_context with_evars clear_flag cx)
 
-let simplest_case c = general_case_analysis false (c,NoBindings)
+let simplest_case c = general_case_analysis false None (c,NoBindings)
 
 (* Elimination tactic with bindings but using the default elimination
  * constant associated with the type. *)
@@ -951,39 +996,39 @@ let find_eliminator c gl =
     evd, {elimindex = None; elimbody = (c,NoBindings);
           elimrename = Some (true, constructors_nrealdecls ind)}
 
-let default_elim with_evars (c,_ as cx) =
+let default_elim with_evars clear_flag (c,_ as cx) =
   Proofview.tclORELSE
     (Proofview.Goal.raw_enter begin fun gl ->
       let evd, elim = find_eliminator c gl in
 	Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evd)
-	  (Proofview.V82.tactic (general_elim with_evars cx elim))
+	  (Proofview.V82.tactic (general_elim with_evars clear_flag cx elim))
     end)
     begin function
       | IsRecord ->
           (* For records, induction principles aren't there by default
              anymore.  Instead, we do a case analysis instead. *)
-          general_case_analysis with_evars cx
+          general_case_analysis with_evars clear_flag cx
       | e -> Proofview.tclZERO e
     end
 
-let elim_in_context with_evars c = function
+let elim_in_context with_evars clear_flag c = function
   | Some elim ->
       Proofview.V82.tactic
-        (general_elim with_evars c {elimindex = Some (-1); elimbody = elim;
+        (general_elim with_evars clear_flag c {elimindex = Some (-1); elimbody = elim;
                                     elimrename = None})
-  | None -> default_elim with_evars c
+  | None -> default_elim with_evars clear_flag c
 
-let elim with_evars (c,lbindc as cx) elim =
+let elim with_evars clear_flag (c,lbindc as cx) elim =
   match kind_of_term c with
     | Var id when lbindc == NoBindings ->
 	Tacticals.New.tclTHEN (try_intros_until_id_check id)
-	  (elim_in_context with_evars cx elim)
+	  (elim_in_context with_evars clear_flag cx elim)
     | _ ->
-	elim_in_context with_evars cx elim
+	elim_in_context with_evars clear_flag cx elim
 
 (* The simplest elimination tactic, with no substitutions at all. *)
 
-let simplest_elim c = default_elim false (c,NoBindings)
+let simplest_elim c = default_elim false None (c,NoBindings)
 
 (* Elimination in hypothesis *)
 (* Typically, elimclause := (eq_ind ?x ?P ?H ?y ?Heq : ?P ?y)
@@ -1019,7 +1064,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (
   if eq_constr hyp_typ new_hyp_typ then
     errorlabstrm "general_rewrite_in"
       (str "Nothing to rewrite in " ++ pr_id id ++ str".");
-  clenv_refine_in with_evars id elimclause'' gl
+  clenv_refine_in with_evars None id elimclause'' gl
 
 let general_elim_clause with_evars flags id c e =
   let elim = match id with
@@ -1117,7 +1162,7 @@ let solve_remaining_apply_goals gl =
     with Not_found -> tclIDTAC gl
   else tclIDTAC gl
     
-let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 =
+let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) gl0 =
   let flags =
     if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
   (* The actual type of the theorem. It will be matched against the
@@ -1153,21 +1198,26 @@ let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 =
 		Loc.raise loc exn
 	in try_red_apply thm_ty0
   in
-    tclTHEN (try_main_apply with_destruct c) solve_remaining_apply_goals gl0
+    tclTHENLIST [
+      try_main_apply with_destruct c;
+      solve_remaining_apply_goals;
+      Proofview.V82.of_tactic
+        (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)
+    ] gl0
 
 let rec apply_with_bindings_gen b e = function
   | [] -> tclIDTAC
-  | [cb] -> general_apply b b e cb
-  | cb::cbl ->
-      tclTHENLAST (general_apply b b e cb) (apply_with_bindings_gen b e cbl)
+  | [k,cb] -> general_apply b b e k cb
+  | (k,cb)::cbl ->
+      tclTHENLAST (general_apply b b e k cb) (apply_with_bindings_gen b e cbl)
 
-let apply_with_bindings cb = apply_with_bindings_gen false false [dloc,cb]
+let apply_with_bindings cb = apply_with_bindings_gen false false [None,(dloc,cb)]
 
-let eapply_with_bindings cb = apply_with_bindings_gen false true [dloc,cb]
+let eapply_with_bindings cb = apply_with_bindings_gen false true [None,(dloc,cb)]
 
-let apply c = apply_with_bindings_gen false false [dloc,(c,NoBindings)]
+let apply c = apply_with_bindings_gen false false [None,(dloc,(c,NoBindings))]
 
-let eapply c = apply_with_bindings_gen false true [dloc,(c,NoBindings)]
+let eapply c = apply_with_bindings_gen false true [None,(dloc,(c,NoBindings))]
 
 let apply_list = function
   | c::l -> apply_with_bindings (c,ImplicitBindings l)
@@ -1212,15 +1262,19 @@ let apply_in_once_main flags innerclause (d,lbind) gl =
   in
   aux (pf_apply make_clenv_binding gl (d,thm) lbind)
 
-let apply_in_once sidecond_first with_delta with_destruct with_evars id
-  (loc,(d,lbind)) gl0 =
+let apply_in_once sidecond_first with_delta with_destruct with_evars hyp_clear_flag
+    id (clear_flag,(loc,(d,lbind))) gl0 =
   let flags = if with_delta then elim_flags () else elim_no_delta_flags () in
   let t' = pf_get_hyp_typ gl0 id in
   let innerclause = mk_clenv_from_n gl0 (Some 0) (mkVar id,t') in
   let rec aux with_destruct c gl =
     try
       let clause = apply_in_once_main flags innerclause (c,lbind) gl in
-      clenv_refine_in ~sidecond_first with_evars id clause gl
+      tclTHEN
+        (clenv_refine_in ~sidecond_first with_evars hyp_clear_flag id clause)
+        (Proofview.V82.of_tactic
+           (apply_clear_request clear_flag false c))
+        gl
     with e when with_destruct ->
       let e = Errors.push e in
       descend_in_conjunctions aux (fun _ -> raise e) c gl
@@ -1435,7 +1489,7 @@ let constructor_tac with_evars expctdnumopt i lbind =
 	(Proofview.Goal.env gl) (Proofview.Goal.sigma gl) (fst mind, i) in
       let cons = mkConstructU cons in
 	
-      let apply_tac = Proofview.V82.tactic (general_apply true false with_evars (dloc,(cons,lbind))) in
+      let apply_tac = Proofview.V82.tactic (general_apply true false with_evars None (dloc,(cons,lbind))) in
 	(Tacticals.New.tclTHENLIST
            [Proofview.V82.tclEVARS sigma; Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast); intros; apply_tac])
   end
@@ -1770,23 +1824,23 @@ let tclMAPFIRST tacfun l =
   List.fold_right (fun x -> Tacticals.New.tclTHENFIRST (tacfun x)) l (Proofview.tclUNIT())
 
 let general_apply_in sidecond_first with_delta with_destruct with_evars
-    id lemmas ipat =
+    with_clear id lemmas ipat =
   if sidecond_first then
     (* Skip the side conditions of the applied lemma *)
     Tacticals.New.tclTHENLAST
       (tclMAPLAST
-	(apply_in_once sidecond_first with_delta with_destruct with_evars id)
+	(apply_in_once sidecond_first with_delta with_destruct with_evars with_clear id)
 	lemmas)
       (as_tac id ipat)
   else
     Tacticals.New.tclTHENFIRST
       (tclMAPFIRST
-	(apply_in_once sidecond_first with_delta with_destruct with_evars id)
+	(apply_in_once sidecond_first with_delta with_destruct with_evars with_clear id)
 	lemmas)
       (as_tac id ipat)
 
-let apply_in simple with_evars id lemmas ipat =
-  general_apply_in false simple simple with_evars id lemmas ipat
+let apply_in simple with_evars clear_flag id lemmas ipat =
+  general_apply_in false simple simple with_evars clear_flag id lemmas ipat
 
 (*****************************)
 (* Tactics abstracting terms *)
@@ -3283,7 +3337,7 @@ let induction_tac with_evars elim (varname,lbind) typ gl =
   let elimc = mkCast (elimc, DEFAULTcast, elimt) in
   elimination_clause_scheme with_evars rename i (elimc, elimt, lbindelimc) indclause gl
 
-let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) names
+let induction_from_context clear_flag isrec with_evars (indref,nparams,elim) (hyp0,lbind) names
   inhyps =
   Proofview.Goal.enter begin fun gl ->
   let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
@@ -3295,18 +3349,19 @@ let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) n
   let induct_tac elim = Proofview.V82.tactic (tclTHENLIST [
     induction_tac with_evars elim (hyp0,lbind) typ0;
     tclTRY (unfold_body hyp0);
-    thin [hyp0]
+    Proofview.V82.of_tactic
+      (apply_clear_request clear_flag true (mkVar hyp0))
   ]) in
   apply_induction_in_context
     (Some (hyp0,inhyps)) elim indvars names induct_tac
   end
 
-let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbind) inhyps =
+let induction_with_atomization_of_ind_arg clear_flag isrec with_evars elim names (hyp0,lbind) inhyps =
   Proofview.Goal.enter begin fun gl ->
   let sigma, elim_info = find_induction_type isrec elim hyp0 gl in
   Tacticals.New.tclTHENLIST
     [Proofview.V82.tclEVARS sigma; (atomize_param_of_ind elim_info hyp0);
-    (induction_from_context isrec with_evars elim_info
+    (induction_from_context clear_flag isrec with_evars elim_info
       (hyp0,lbind) names inhyps)]
   end
 
@@ -3358,7 +3413,7 @@ let clear_unselected_context id inhyps cls gl =
 	  thin ids gl
       | None -> tclIDTAC gl
 
-let induction_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
+let induction_gen clear_flag isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
   let inhyps = match cls with
   | Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps
   | _ -> [] in
@@ -3369,7 +3424,7 @@ let induction_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
 	Tacticals.New.tclTHEN
           (Proofview.V82.tactic (clear_unselected_context id inhyps cls))
 	  (induction_with_atomization_of_ind_arg
-	    isrec with_evars elim names (id,lbind) inhyps)
+	    clear_flag isrec with_evars elim names (id,lbind) inhyps)
     | _        ->
         Proofview.Goal.raw_enter begin fun gl ->
           let env = Proofview.Goal.env gl in
@@ -3385,7 +3440,8 @@ let induction_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
 	      (letin_tac_gen with_eq
                  (AbstractPattern (Name id,(sigma,c),(Option.default allHypsAndConcl cls),false,tactic_infer_flags)) None)
 	      (induction_with_atomization_of_ind_arg
-	         isrec with_evars elim names (id,lbind) inhyps)
+	         (Some true)
+                 isrec with_evars elim names (id,lbind) inhyps)
           end
         end
 
@@ -3447,7 +3503,7 @@ let induction_destruct_core isrec with_evars (lc,elim,names,cls) =
   if Int.equal (List.length lc) 1 && not ifi then
     (* standard induction *)
     onOpenInductionArg
-      (fun c -> induction_gen isrec with_evars elim names c cls)
+      (fun clear_flag c -> induction_gen clear_flag isrec with_evars elim names c cls)
       (List.hd lc)
   else begin
     (* functional induction *)
@@ -3467,7 +3523,7 @@ let induction_destruct_core isrec with_evars (lc,elim,names,cls) =
       (* Hook to recover standard induction on non-standard induction schemes *)
       (* will be removable when is_functional_induction will be more clever *)
       onInductionArg
-	(fun (c,lbind) ->
+	(fun _clear_flag (c,lbind) ->
 	  if lbind != NoBindings then
 	    error "'with' clause not supported here.";
 	  induction_gen_l isrec with_evars elim names [c]) (List.hd lc)
@@ -3475,7 +3531,7 @@ let induction_destruct_core isrec with_evars (lc,elim,names,cls) =
       let newlc =
 	List.map (fun x ->
 	  match x with (* FIXME: should we deal with ElimOnIdent? *)
-	  | ElimOnConstr (x,NoBindings) -> x
+	  | _clear_flag,ElimOnConstr (x,NoBindings) -> x
 	  | _ -> error "Don't know where to find some argument.")
 	  lc in
       induction_gen_l isrec with_evars elim names newlc
@@ -3910,10 +3966,15 @@ module Simple = struct
     generalize_gen (List.map (fun c -> ((AllOccurrences,c),Names.Anonymous))
                         cl)
 
-  let apply c = apply_with_bindings_gen false false [Loc.ghost,(c,NoBindings)]
-  let eapply c = apply_with_bindings_gen false true [Loc.ghost,(c,NoBindings)]
-  let elim c   = elim false (c,NoBindings) None
-  let case   c = general_case_analysis false (c,NoBindings)
+  let apply c =
+    apply_with_bindings_gen false false [None,(Loc.ghost,(c,NoBindings))]
+  let eapply c =
+    apply_with_bindings_gen false true [None,(Loc.ghost,(c,NoBindings))]
+  let elim c   = elim false None (c,NoBindings) None
+  let case   c = general_case_analysis false None (c,NoBindings)
+
+  let apply_in id c =
+    apply_in false false None id [None,(Loc.ghost, (c, NoBindings))] None
 
 end