From f841c27c1cfd38aada72f3c8f90e2ed1ec22db6a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 21 Dec 2015 22:19:34 +0100
Subject: Adding an "as" clause to specialize.

Comments
--------

- The tactic specialize conveys a somehow intuitive reasoning concept
  and I would support continuing maintaining it even if the design
  comes in my opinion with some oddities. (Note that the experience of
  MathComp and SSReflect also suggests that specialize is an
  interesting concept in itself).

There are two variants to specialize:

- specialize (H args) with H an hypothesis looks natural: we
  specialize H with extra arguments and the "as pattern" clause comes
  naturally as an extension of it, destructuring the result using the
  pattern.
- specialize term with bindings makes the choice of fully applying the
  term filling missing expressions with bindings and to then behave as
  generalize. Wouldn't we like a more fine-grained approach and the
  result to remain in the context?
  In this second case, the "as" clause works as if the term were posed
  in the context with "pose proof".
---
 ltac/coretactics.ml4            |  5 ++++-
 tactics/tactics.ml              | 42 ++++++++++++++++++++++++++---------------
 tactics/tactics.mli             |  2 +-
 test-suite/success/specialize.v |  8 ++++++++
 4 files changed, 40 insertions(+), 17 deletions(-)

diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index 321d50df38..de4d589eee 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -142,7 +142,10 @@ END
 
 TACTIC EXTEND specialize
   [ "specialize" constr_with_bindings(c) ] -> [
-    Tacticals.New.tclDELAYEDWITHHOLES false c Tactics.specialize
+    Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None)
+  ]
+| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> [
+    Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat))
   ]
 END
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 23aadf3933..d4158d7872 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2859,7 +2859,7 @@ let quantify lconstr =
 
 (* Modifying/Adding an hypothesis  *)
 
-let specialize (c,lbind) =
+let specialize (c,lbind) ipat =
   Proofview.Goal.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
@@ -2880,24 +2880,36 @@ let specialize (c,lbind) =
       let term = applist(thd,List.map (nf_evar clause.evd) tstack) in
       if occur_meta term then
 	errorlabstrm "" (str "Cannot infer an instance for " ++
+
           pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++
 	  str ".");
       clause.evd, term in
   let typ = Retyping.get_type_of env sigma term in
-  match kind_of_term (fst(decompose_app (snd(decompose_lam_assum c)))) with
-  | Var id when Id.List.mem id (Tacmach.New.pf_ids_of_hyps gl) ->
-      Tacticals.New.tclTHEN
-        (Proofview.Unsafe.tclEVARS sigma)
-	(Tacticals.New.tclTHENFIRST
-	   (assert_before_replacing id typ)
-	   (exact_no_check term))
-  | _ ->
-      (* To deprecate in favor of generalize? *)
-      Tacticals.New.tclTHEN
-        (Proofview.Unsafe.tclEVARS sigma)
-	(Tacticals.New.tclTHENLAST
-           (cut typ)
-           (exact_no_check term))
+  let tac =
+    match kind_of_term (fst(decompose_app (snd(decompose_lam_assum c)))) with
+    | Var id when Id.List.mem id (Tacmach.New.pf_ids_of_hyps gl) ->
+      (* Like assert (id:=id args) but with the concept of specialization *)
+      let naming,tac =
+        prepare_intros false (IntroIdentifier id) MoveLast ipat in
+      let repl = do_replace (Some id) naming in
+      Tacticals.New.tclTHENFIRST
+        (assert_before_then_gen repl naming typ tac)
+	(exact_no_check term)
+    | _ ->
+      match ipat with
+      | None ->
+        (* Like generalize with extra support for "with" bindings *)
+        (* even though the "with" bindings forces full application *)
+        Tacticals.New.tclTHENLAST (cut typ) (exact_no_check term)
+      | Some (loc,ipat) ->
+        (* Like pose proof with extra support for "with" bindings *)
+        (* even though the "with" bindings forces full application *)
+        let naming,tac = prepare_intros_loc loc false IntroAnonymous MoveLast ipat in
+        Tacticals.New.tclTHENFIRST
+          (assert_before_then_gen false naming typ tac)
+	  (exact_no_check term)
+  in
+  Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac
   end }
 
 (*****************************)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 012c75091a..fb033363e8 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -174,7 +174,7 @@ val unfold_body   : Id.t -> unit Proofview.tactic
 val keep          : Id.t list -> unit Proofview.tactic
 val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic
 
-val specialize    : constr with_bindings -> unit Proofview.tactic
+val specialize    : constr with_bindings -> intro_pattern option -> unit Proofview.tactic
 
 val move_hyp      : Id.t -> Id.t move_location -> unit Proofview.tactic
 val rename_hyp    : (Id.t * Id.t) list -> unit Proofview.tactic
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index 3faa1ca43a..fba05cd902 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -64,3 +64,11 @@ assert (H:=H I).
 match goal with H:_ |- _ => clear H end.
 match goal with H:_ |- _ => exact H end.
 Qed.
+
+(* Test specialize as *)
+
+Goal (forall x, x=0) -> 1=0.
+intros.
+specialize (H 1) as ->.
+reflexivity.
+Qed.
-- 
cgit v1.2.3