A reorganization of the "assert" tactics (hopefully uniform naming

scheme, redundancies, possibility of chaining a tactic knowing the
name of introduced hypothesis, new proof engine).

6 files changed, 140 insertions, 132 deletions

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 96e8e60bba..4a43b8038e 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -18,24 +18,26 @@ open Misctypes
 
 (* Absurd *)
 
-let absurd c gls =
-  let env = pf_env gls and sigma = project gls in
-  let j = Retyping.get_judgment_of env sigma c in
-  let sigma, j = Coercion.inh_coerce_to_sort Loc.ghost env sigma j in
-  let c = j.Environ.utj_val in
-  (tclTHENS
-     (tclTHEN (Proofview.V82.of_tactic (elim_type (build_coq_False ()))) (Proofview.V82.of_tactic (cut c)))
-     ([(tclTHENS
-          (Proofview.V82.of_tactic (cut (mkApp(build_coq_not (),[|c|]))))
-	  ([(tclTHEN (Proofview.V82.of_tactic intros)
-	       ((fun gl ->
-		   let ida = pf_nth_hyp_id gl 1
-                   and idna = pf_nth_hyp_id gl 2 in
-                   exact_no_check (mkApp(mkVar idna,[|mkVar ida|])) gl)));
-            tclIDTAC]));
-       tclIDTAC])) { gls with Evd.sigma; }
+let mk_absurd_proof t =
+  let id = Namegen.default_dependent_ident in
+  mkLambda (Names.Name id,mkApp(build_coq_not (),[|t|]),
+    mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|])))
 
-let absurd c = Proofview.V82.tactic (absurd c)
+let absurd c =
+  Proofview.Goal.raw_enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let j = Retyping.get_judgment_of env sigma c in
+    let sigma, j = Coercion.inh_coerce_to_sort Loc.ghost env sigma j in
+    let t = j.Environ.utj_val in
+    Tacticals.New.tclTHENLIST [
+      Proofview.V82.tclEVARS sigma;
+      elim_type (build_coq_False ());
+      Simple.apply (mk_absurd_proof t)
+    ]
+  end
+
+let absurd c = absurd c
 
 (* Contradiction *)
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 5f8e9f5030..28017f8533 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -907,7 +907,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort =
   let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
   Proofview.V82.tclEVARS sigma <*>
   Proofview.tclEFFECTS eff <*>
-  tclTHENS (cut_intro absurd_term)
+  tclTHENS (assert_after Anonymous absurd_term)
     [onLastHypId gen_absurdity; (Proofview.V82.tactic (refine pf))]
 
 let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
@@ -1514,7 +1514,8 @@ let cutSubstInHyp_LR eqn id =
   if not (dependent (mkRel 1) body) then raise NothingToRewrite;
   let refine = Proofview.V82.tactic (fun gl -> Tacmach.refine_no_check (mkVar id) gl) in
   let subst = tclTHENFIRST (bareRevSubstInConcl (lbeq,u) body eq) refine in
-    Proofview.V82.tclEVARS sigma <*> (cut_replacing id expected_goal subst)
+    Proofview.V82.tclEVARS sigma <*>
+      tclTHENLAST (assert_after_replacing id expected_goal) subst
   end
 
 let cutSubstInHyp_RL eqn id =
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 45f416c2cf..089fef4bc9 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -483,7 +483,7 @@ let raw_inversion inv_kind id status names =
     let neqns = List.length realargs in
     tclTHEN (Proofview.V82.tclEVARS sigma)
       (tclTHENS
-        (assert_tac Anonymous cut_concl)
+        (assert_before Anonymous cut_concl)
         [case_tac names
             (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns))
             (Some elim_predicate) ind (c, t);
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index a8a4b1dcce..29176e2df1 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1426,7 +1426,7 @@ let cl_rewrite_clause_tac ?abs strat clause gl =
 	let tac = 
 	  match clause, p with
 	  | Some id, Some p ->
-	      Proofview.V82.of_tactic (cut_replacing id newt (Proofview.V82.tactic (Tacmach.refine p)))
+	      tclTHENLAST (Proofview.V82.of_tactic (assert_after_replacing id newt)) (Tacmach.refine p)
 	  | Some id, None -> 
 	      change_in_hyp None (fun env sigma -> sigma, newt) (id, InHypTypeOnly)
 	  | None, Some p ->
@@ -2061,9 +2061,10 @@ let setoid_symmetry_in id =
   let he,c1,c2 =  mkApp (equiv, Array.of_list others),c1,c2 in
   let new_hyp' =  mkApp (he, [| c2 ; c1 |]) in
   let new_hyp = it_mkProd_or_LetIn new_hyp'  binders in
-    tclTHENS (Proofview.V82.of_tactic (Tactics.cut new_hyp))
-      [ intro_replacing id;
-	Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ]) ]
+   Proofview.V82.of_tactic
+    (Tacticals.New.tclTHENLAST
+      (Tactics.assert_after_replacing id new_hyp)
+      (Tacticals.New.tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ]))
       gl)
 
 let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0b9f722fad..f3a43be0bb 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-let a = 1
-
 open Pp
 open Errors
 open Util
@@ -155,23 +153,43 @@ end
 let convert x y = convert_gen Reduction.CONV x y
 let convert_leq x y = convert_gen Reduction.CUMUL x y
 
-let error_clear_dependency env id = function
+let clear_dependency_msg env id = function
+  | Evarutil.OccurHypInSimpleClause None ->
+      pr_id id ++ str " is used in conclusion."
+  | Evarutil.OccurHypInSimpleClause (Some id') ->
+      pr_id id ++ strbrk " is used in hypothesis " ++ pr_id id' ++ str"."
+  | Evarutil.EvarTypingBreak ev ->
+      str "Cannot remove " ++ pr_id id ++
+      strbrk " without breaking the typing of " ++
+      Printer.pr_existential env ev ++ str"."
+
+let error_clear_dependency env id err =
+  errorlabstrm "" (clear_dependency_msg env id err)
+
+let replacing_dependency_msg env id = function
   | Evarutil.OccurHypInSimpleClause None ->
-      errorlabstrm "" (pr_id id ++ str " is used in conclusion.")
+      str "Cannot change " ++ pr_id id ++ str ", it is used in conclusion."
   | Evarutil.OccurHypInSimpleClause (Some id') ->
-      errorlabstrm ""
-        (pr_id id ++ strbrk " is used in hypothesis " ++ pr_id id' ++ str".")
+      str "Cannot change " ++ pr_id id ++
+      strbrk ", it is used in hypothesis " ++ pr_id id' ++ str"."
   | Evarutil.EvarTypingBreak ev ->
-      errorlabstrm ""
-        (str "Cannot remove " ++ pr_id id ++
-	 strbrk " without breaking the typing of " ++
-	 Printer.pr_existential env ev ++ str".")
+      str "Cannot change " ++ pr_id id ++
+      strbrk " without breaking the typing of " ++
+      Printer.pr_existential env ev ++ str"."
+
+let error_replacing_dependency env id err =
+  errorlabstrm "" (replacing_dependency_msg env id err)
 
 let thin l gl =
   try thin l gl
   with Evarutil.ClearDependencyError (id,err) ->
     error_clear_dependency (pf_env gl) id err
 
+let thin_for_replacing l gl =
+  try Tacmach.thin l gl
+  with Evarutil.ClearDependencyError (id,err) ->
+    error_replacing_dependency (pf_env gl) id err
+
 let apply_clear_request clear_flag dft c =
   let check_isvar c =
     if not (isVar c) then
@@ -223,6 +241,10 @@ type name_flag =
   | NamingBasedOn of Id.t * Id.t list
   | NamingMustBe of Loc.t * Id.t
 
+let naming_of_name = function
+  | Anonymous -> NamingAvoid []
+  | Name id -> NamingMustBe (dloc,id)
+
 let find_name repl decl naming gl = match naming with
   | NamingAvoid idl ->
       (* this case must be compatible with [find_intro_names] below. *)
@@ -242,29 +264,41 @@ let find_name repl decl naming gl = match naming with
 (*            Cut rule                                        *)
 (**************************************************************)
 
-let internal_cut_gen b naming t =
+let assert_before_then_gen b naming t tac =
   Proofview.Goal.raw_enter begin fun gl ->
-  try 
     let id = find_name b (Anonymous,None,t) naming gl in
-    Proofview.V82.tactic (internal_cut b id t)
-  with Evarutil.ClearDependencyError (id,err) ->
-    error_clear_dependency (Proofview.Goal.env gl) id err
+    Tacticals.New.tclTHENLAST
+      (Proofview.V82.tactic
+         (fun gl ->
+           try internal_cut b id t gl
+           with Evarutil.ClearDependencyError (id,err) ->
+             error_replacing_dependency (pf_env gl) id err))
+      (tac id)
   end
 
-let internal_cut = internal_cut_gen false
-let internal_cut_replace = internal_cut_gen true
+let assert_before_gen b naming t =
+  assert_before_then_gen b naming t (fun _ -> Proofview.tclUNIT ())
 
-let internal_cut_rev_gen b naming t =
+let assert_before na = assert_before_gen false (naming_of_name na)
+let assert_before_replacing id = assert_before_gen true (NamingMustBe (dloc,id))
+
+let assert_after_then_gen b naming t tac =
   Proofview.Goal.raw_enter begin fun gl ->
-  try
     let id = find_name b (Anonymous,None,t) naming gl in
-    Proofview.V82.tactic (internal_cut_rev b id t)
-  with Evarutil.ClearDependencyError (id,err) ->
-    error_clear_dependency (Proofview.Goal.env gl) id err
+    Tacticals.New.tclTHENFIRST
+      (Proofview.V82.tactic
+         (fun gl ->
+           try internal_cut_rev b id t gl
+           with Evarutil.ClearDependencyError (id,err) ->
+             error_replacing_dependency (pf_env gl) id err))
+      (tac id)
   end
 
-let internal_cut_rev = internal_cut_rev_gen false
-let internal_cut_rev_replace = internal_cut_rev_gen true
+let assert_after_gen b naming t =
+  assert_after_then_gen b naming t (fun _ -> (Proofview.tclUNIT ()))
+
+let assert_after na = assert_after_gen false (naming_of_name na)
+let assert_after_replacing id = assert_after_gen true (NamingMustBe (dloc,id))
 
 (**************************************************************)
 (*          Fixpoints and CoFixpoints                         *)
@@ -605,22 +639,6 @@ let rec get_next_hyp_position id = function
       else
 	get_next_hyp_position id right
 
-let thin_for_replacing l gl =
-  try Tacmach.thin l gl
-  with Evarutil.ClearDependencyError (id,err) -> match err with
-  | Evarutil.OccurHypInSimpleClause None ->
-      errorlabstrm ""
-      (str "Cannot change " ++ pr_id id ++ str ", it is used in conclusion.")
-  | Evarutil.OccurHypInSimpleClause (Some id') ->
-      errorlabstrm ""
-        (str "Cannot change " ++ pr_id id ++
-	 strbrk ", it is used in hypothesis " ++ pr_id id' ++ str".")
-  | Evarutil.EvarTypingBreak ev ->
-      errorlabstrm ""
-        (str "Cannot change " ++ pr_id id ++
-	 strbrk " without breaking the typing of " ++
-	 Printer.pr_existential (pf_env gl) ev ++ str".")
-
 let intro_replacing id gl =
   let next_hyp = get_next_hyp_position id (pf_hyps gl) in
   tclTHENLIST
@@ -742,9 +760,9 @@ let map_induction_arg f = function
   | clear_flag,ElimOnAnonHyp n as x -> x
   | clear_flag,ElimOnIdent id as x -> x
 
-(**************************)
-(*     Cut tactics        *)
-(**************************)
+(****************************************)
+(* tactic "cut" (actually modus ponens) *)
+(****************************************)
 
 let cut c =
   Proofview.Goal.raw_enter begin fun gl ->
@@ -775,38 +793,6 @@ let cut c =
       Tacticals.New.tclZEROMSG (str "Not a proposition or a type.")
   end
 
-let cut_intro t = Tacticals.New.tclTHENFIRST (cut t) intro
-
-(* [assert_replacing id T tac] adds the subgoals of the proof of [T]
-   before the current goal
-
-   id:T0                 id:T0    id:T
-   =====   ------>   tac(=====) + ====
-    G                     T        G
-
-   It fails if the hypothesis to replace appears in the goal or in
-   another hypothesis.
-*)
-
-let assert_replacing id t tac =
-  Tacticals.New.tclTHENFIRST
-    (internal_cut_replace (NamingMustBe (dloc,id)) t) tac
-
-(* [cut_replacing id T tac] adds the subgoals of the proof of [T]
-   after the current goal
-
-   id:T0             id:T       id:T0
-   =====   ------>   ==== + tac(=====)
-    G                 G          T
-
-   It fails if the hypothesis to replace appears in the goal or in
-   another hypothesis.
-*)
-
-let cut_replacing id t tac =
-  Tacticals.New.tclTHENLAST
-    (internal_cut_rev_replace (NamingMustBe (dloc,id)) t) tac
-
 let error_uninstantiated_metas t clenv =
   let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
   let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta")
@@ -853,10 +839,10 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) nami
     (Proofview.V82.tclEVARS clenv.evd)
     (if sidecond_first then
        Tacticals.New.tclTHENFIRST
-         (internal_cut_gen with_clear naming new_hyp_typ) exact_tac
+         (assert_before_gen with_clear naming new_hyp_typ) exact_tac
      else
        Tacticals.New.tclTHENLAST
-         (internal_cut_rev_gen with_clear naming new_hyp_typ) exact_tac)
+         (assert_after_gen with_clear naming new_hyp_typ) exact_tac)
 
 (********************************************)
 (*       Elimination tactics                *)
@@ -1178,7 +1164,7 @@ let descend_in_conjunctions tac exit c =
 	    | None -> Tacticals.New.tclFAIL 0 (mt())
 	    | Some (p,pt) ->
 	    Tacticals.New.tclTHENS
-	      (internal_cut (NamingAvoid []) pt)
+	      (assert_before Anonymous pt)
 	      [Proofview.V82.tactic (refine p); (* Might be ill-typed due to forbidden elimination. *)
 	       Tacticals.New.onLastHypId (fun id ->
                  Tacticals.New.tclTHEN
@@ -1520,7 +1506,7 @@ let specialize (c,lbind) g =
        | Var id when Id.List.mem id (pf_ids_of_hyps g) ->
 	   tclTHEN tac
 	     (tclTHENFIRST
-	       (fun g -> Proofview.V82.of_tactic (internal_cut_replace (NamingMustBe (dloc,id)) (pf_type_of g term)) g)
+	       (fun g -> Proofview.V82.of_tactic (assert_before_replacing id (pf_type_of g term)) g)
 	       (exact_no_check term)) g
        | _ -> tclTHEN tac
 	   (tclTHENLAST
@@ -1830,7 +1816,7 @@ let intros_patterns = function
   | l -> intro_patterns_to MoveLast l
 
 (**************************)
-(*   Other cut tactics    *)
+(*   Forward reasoning    *)
 (**************************)
 
 let rec prepare_naming loc = function
@@ -1872,14 +1858,8 @@ let do_replace id = function
 let assert_as first ipat c =
   let naming,tac = prepare_intros IntroAnonymous ipat in
   let repl = do_replace (head_ident c) naming in
-  Tacticals.New.tclTHENS
-    ((if first then internal_cut_gen
-      else internal_cut_rev_gen) repl naming c)
-    (if first then [Proofview.tclUNIT (); Tacticals.New.onLastHypId tac]
-     else [Tacticals.New.onLastHypId tac; Proofview.tclUNIT ()])
-
-let assert_tac na = assert_as true (ipat_of_name na)
-let enough_tac na = assert_as false (ipat_of_name na)
+  if first then assert_before_then_gen repl naming c tac
+  else assert_after_then_gen repl naming c tac
 
 (* apply in as *)
 
@@ -1990,7 +1970,7 @@ let letin_tac with_eq name c ty occs =
 let letin_pat_tac with_eq name c occs =
   letin_tac_gen with_eq (AbstractPattern (name,c,occs,false,tactic_infer_flags)) None
 
-(* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *)
+(* Tactics "pose proof" (usetac=None) and "assert"/"enough" (otherwise) *)
 let forward b usetac ipat c =
   match usetac with
   | None ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 77e1938c68..19ecc2f89e 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -280,7 +280,7 @@ val induction : evars_flag ->
 val general_case_analysis : evars_flag -> clear_flag -> constr with_bindings ->  unit Proofview.tactic
 val simplest_case         : constr -> unit Proofview.tactic
 
-val simple_destruct          : quantified_hypothesis -> unit Proofview.tactic
+val simple_destruct       : quantified_hypothesis -> unit Proofview.tactic
 val destruct : evars_flag ->
   (evar_map * constr with_bindings) induction_arg list ->
   constr with_bindings option ->
@@ -300,8 +300,8 @@ val induction_destruct : rec_flag -> evars_flag ->
 
 (** {6 Eliminations giving the type instead of the proof. } *)
 
-val case_type         : constr  -> unit Proofview.tactic
-val elim_type         : constr  -> unit Proofview.tactic
+val case_type         : types -> unit Proofview.tactic
+val elim_type         : types -> unit Proofview.tactic
 
 (** {6 Introduction tactics. } *)
 
@@ -341,22 +341,46 @@ val transitivity                : constr -> unit Proofview.tactic
 val etransitivity               : unit Proofview.tactic
 val intros_transitivity         : constr option -> unit Proofview.tactic
 
-val cut                         : constr -> unit Proofview.tactic
-val cut_intro                   : constr -> unit Proofview.tactic
-val assert_replacing            : Id.t -> types -> unit Proofview.tactic -> unit Proofview.tactic
-val cut_replacing               : Id.t -> types -> unit Proofview.tactic -> unit Proofview.tactic
-
-val assert_as : bool -> intro_pattern_expr located option -> constr -> unit Proofview.tactic
-val forward   : bool -> unit Proofview.tactic option -> intro_pattern_expr located option -> constr -> unit Proofview.tactic
-val letin_tac : (bool * intro_pattern_naming_expr located) option -> Name.t ->
-  constr -> types option -> clause -> unit Proofview.tactic
-val letin_pat_tac : (bool * intro_pattern_naming_expr located) option -> Name.t ->
-  evar_map * constr -> clause -> unit Proofview.tactic
-val assert_tac : Name.t -> types -> unit Proofview.tactic
-val enough_tac : Name.t -> types -> unit Proofview.tactic
-val assert_by  : Name.t -> types -> unit Proofview.tactic -> unit Proofview.tactic
-val enough_by  : Name.t -> types -> unit Proofview.tactic -> unit Proofview.tactic
-val pose_proof : Name.t -> constr -> unit Proofview.tactic
+(** {6 Cut tactics. } *)
+
+val assert_before_replacing: Id.t -> types -> unit Proofview.tactic
+val assert_after_replacing : Id.t -> types -> unit Proofview.tactic
+val assert_before : Name.t -> types -> unit Proofview.tactic
+val assert_after  : Name.t -> types -> unit Proofview.tactic
+
+val assert_as     : (* true = before *) bool ->
+  intro_pattern_expr located option -> constr -> unit Proofview.tactic
+
+(** Implements the tactics assert, enough and pose proof; note that "by"
+    applies on the first goal for both assert and enough *)
+
+val assert_by  : Name.t -> types -> unit Proofview.tactic ->
+  unit Proofview.tactic
+val enough_by  : Name.t -> types -> unit Proofview.tactic ->
+  unit Proofview.tactic
+val pose_proof : Name.t -> constr ->
+  unit Proofview.tactic
+
+(** Common entry point for user-level "assert", "enough" and "pose proof" *)
+
+val forward   : bool -> unit Proofview.tactic option ->
+  intro_pattern_expr located option -> constr -> unit Proofview.tactic
+
+(** Implements the tactic cut, actually a modus ponens rule *)
+
+val cut        : types -> unit Proofview.tactic
+
+(** {6 Tactics for adding local definitions. } *)
+
+val letin_tac : (bool * intro_pattern_naming_expr located) option ->
+  Name.t -> constr -> types option -> clause -> unit Proofview.tactic
+
+(** Common entry point for user-level "set", "pose" and "remember" *)
+
+val letin_pat_tac : (bool * intro_pattern_naming_expr located) option ->
+  Name.t -> evar_map * constr -> clause -> unit Proofview.tactic
+
+(** {6 Generalize tactics. } *)
 
 val generalize      : constr list -> tactic
 val generalize_gen  : ((occurrences * constr) * Name.t) list -> tactic