From 11aaa1fd8230a347f1dca1a0f349ea7c7f2768c3 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 10 Jun 2016 18:58:24 -0400
Subject: Add support for transparent abstract (no syntax)

This is a small change that allows a transparent version of tclABSTRACT.
Additionally, it factors the machinery of [abstract] through a
plugin-accessible function which allows alternate continuations (other
than exact_no_check.

It might be nice to factor it further, into a cache_term function that
caches a term, and a separate bit that calls cache_term with the result
of running the tactic.
---
 tactics/tactics.ml  | 28 ++++++++++++++++++----------
 tactics/tactics.mli |  4 +++-
 2 files changed, 21 insertions(+), 11 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e792585822..19627eb530 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4907,7 +4907,7 @@ let shrink_entry sign const =
   } in
   (const, args)
 
-let abstract_subproof id gk tac =
+let cache_term_by_tactic_then id gk ?(opaque=true) tac tacK =
   let open Tacticals.New in
   let open Tacmach.New in
   let open Proofview.Notations in
@@ -4957,8 +4957,8 @@ let abstract_subproof id gk tac =
     else (const, List.rev (Context.Named.to_instance Constr.mkVar sign))
   in
   let args = List.map EConstr.of_constr args in
-  let cd = Entries.DefinitionEntry const in
-  let decl = (cd, IsProof Lemma) in
+  let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in
+  let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in
   let cst () =
     (** do not compute the implicit arguments, it may be costly *)
     let () = Impargs.make_implicit_args false in
@@ -4976,18 +4976,21 @@ let abstract_subproof id gk tac =
     Entries.(snd (Future.force const.const_entry_body)) in
   let solve =
     Proofview.tclEFFECTS effs <*>
-    exact_no_check (applist (lem, args))
+    tacK lem args
   in
   let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in
   Sigma.Unsafe.of_pair (tac, evd)
   end }
 
+let abstract_subproof id gk tac ?(opaque=true) =
+  cache_term_by_tactic_then id gk ~opaque:opaque tac (fun lem args -> exact_no_check (applist (lem, args)))
+
 let anon_id = Id.of_string "anonymous"
 
-let tclABSTRACT name_op tac =
+let name_op_to_name name_op object_kind suffix =
   let open Proof_global in
-  let default_gk = (Global, false, Proof Theorem) in
-  let s, gk = match name_op with
+  let default_gk = (Global, false, object_kind) in
+  match name_op with
     | Some s ->
       (try let _, gk, _ = current_proof_statement () in s, gk
        with NoCurrentProof -> s, default_gk)
@@ -4995,9 +4998,14 @@ let tclABSTRACT name_op tac =
       let name, gk =
 	try let name, gk, _ = current_proof_statement () in name, gk
 	with NoCurrentProof -> anon_id, default_gk in
-      add_suffix name "_subproof", gk
-  in
-  abstract_subproof s gk tac
+      add_suffix name suffix, gk
+
+let tclABSTRACT ?(opaque=true) name_op tac =
+  let open Proof_global in
+  let s, gk = if opaque
+    then name_op_to_name name_op (Proof Theorem) "_subproof"
+    else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in
+  abstract_subproof s gk tac ~opaque:opaque
 
 let unify ?(state=full_transparent_state) x y =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index ba4a9706de..d206011eed 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -401,7 +401,9 @@ val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -
 
 val unify           : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic
 
-val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
+val cache_term_by_tactic_then : Id.t -> Decl_kinds.goal_kind -> ?opaque:bool -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic
+
+val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
 
 val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic
 val specialize_eqs : Id.t -> unit Proofview.tactic
-- 
cgit v1.2.3


From 5f3d20dc53ffd0537a84c93acd761c3c69081342 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 10 Jun 2016 19:12:49 -0400
Subject: Add transparent_abstract tactic

---
 doc/refman/RefMan-ltac.tex                | 14 +++++++++-----
 plugins/ltac/extratactics.ml4             | 13 +++++++++++++
 test-suite/success/transparent_abstract.v | 21 +++++++++++++++++++++
 theories/Init/Prelude.v                   |  2 +-
 4 files changed, 44 insertions(+), 6 deletions(-)
 create mode 100644 test-suite/success/transparent_abstract.v

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 9378529cbe..46274e12f3 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1087,8 +1087,8 @@ Fail all:let n:= numgoals in guard n=2.
 Reset Initial.
 \end{coq_eval}
 
-\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\comindex{Qed exporting}
-\index{Tacticals!abstract@{\tt abstract}}}
+\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\tacindex{transparent\_abstract}\comindex{Qed exporting}
+\index{Tacticals!abstract@{\tt abstract}}\index{Tacticals!transparent\_abstract@{\tt transparent\_abstract}}}
 
 From the outside ``\texttt{abstract \tacexpr}'' is the same as
 {\tt solve \tacexpr}. Internally it saves an auxiliary lemma called
@@ -1114,13 +1114,17 @@ on. This can be obtained thanks to the option below.
 {\tt Set Shrink Abstract}
 \end{quote}
 
-When set, all lemmas generated through \texttt{abstract {\tacexpr}} are
-quantified only over the variables that appear in the term constructed by
-\texttt{\tacexpr}.
+When set, all lemmas generated through \texttt{abstract {\tacexpr}}
+and \texttt{transparent\_abstract {\tacexpr}} are quantified only over the
+variables that appear in the term constructed by \texttt{\tacexpr}.
 
 \begin{Variants}
 \item \texttt{abstract {\tacexpr} using {\ident}}.\\
   Give explicitly the name of the auxiliary lemma.
+\item \texttt{transparent\_abstract {\tacexpr}}.\\
+  Save the subproof in a transparent lemma rather than an opaque one.
+\item \texttt{transparent\_abstract {\tacexpr} using {\ident}}.\\
+  Give explicitly the name of the auxiliary transparent lemma.
 \end{Variants}
 
 \ErrMsg \errindex{Proof is not complete}
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 38fdfb7599..a96623a5f6 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -815,6 +815,19 @@ TACTIC EXTEND destauto
 | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ]
 END
 
+(**********************************************************************)
+
+(**********************************************************************)
+(* A version of abstract constructing transparent terms               *)
+(* Introduced by Jason Gross and Benjamin Delaware in June 2016       *)
+(**********************************************************************)
+
+TACTIC EXTEND transparent_abstract
+| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter { enter = fun gl ->
+      Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) } ]
+| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter { enter = fun gl ->
+      Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) } ]
+END
 
 (* ********************************************************************* *)
 
diff --git a/test-suite/success/transparent_abstract.v b/test-suite/success/transparent_abstract.v
new file mode 100644
index 0000000000..ff4509c4a8
--- /dev/null
+++ b/test-suite/success/transparent_abstract.v
@@ -0,0 +1,21 @@
+Class by_transparent_abstract {T} (x : T) := make_by_transparent_abstract : T.
+Hint Extern 0 (@by_transparent_abstract ?T ?x) => change T; transparent_abstract exact_no_check x : typeclass_instances.
+
+Goal True /\ True.
+Proof.
+  split.
+  transparent_abstract exact I using foo.
+  let x := (eval hnf in foo) in constr_eq x I.
+  let x := constr:(ltac:(constructor) : True) in
+  let T := type of x in
+  let x := constr:(_ : by_transparent_abstract x) in
+  let x := (eval cbv delta [by_transparent_abstract] in (let y : T := x in y)) in
+  pose x as x'.
+  simpl in x'.
+  let v := eval cbv [x'] in x' in tryif constr_eq v I then fail 0 else idtac.
+  hnf in x'.
+  let v := eval cbv [x'] in x' in tryif constr_eq v I then idtac else fail 0.
+  exact x'.
+Defined.
+Check eq_refl : I = foo.
+Eval compute in foo.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index c58d23dad0..e71a8774ed 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -23,4 +23,4 @@ Declare ML Module "cc_plugin".
 Declare ML Module "ground_plugin".
 Declare ML Module "recdef_plugin".
 (* Default substrings not considered by queries like SearchAbout *)
-Add Search Blacklist "_subproof" "Private_".
+Add Search Blacklist "_subproof" "_subterm" "Private_".
-- 
cgit v1.2.3


From 84845f766d9b9d532f615352fbc8a0e78e1727e9 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 27 Mar 2017 13:28:17 -0400
Subject: Mark transparent_abstract as risky in docs

As per Enrico's request.
---
 doc/refman/RefMan-ltac.tex | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 46274e12f3..c2f52e23bc 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1121,10 +1121,17 @@ variables that appear in the term constructed by \texttt{\tacexpr}.
 \begin{Variants}
 \item \texttt{abstract {\tacexpr} using {\ident}}.\\
   Give explicitly the name of the auxiliary lemma.
+  Use this feature at your own risk; explicitly named and reused subterms
+  don't play well with asynchronous proofs.
 \item \texttt{transparent\_abstract {\tacexpr}}.\\
   Save the subproof in a transparent lemma rather than an opaque one.
+  Use this feature at your own risk; building computationally relevant terms
+  with tactics is fragile.
 \item \texttt{transparent\_abstract {\tacexpr} using {\ident}}.\\
   Give explicitly the name of the auxiliary transparent lemma.
+  Use this feature at your own risk; building computationally relevant terms
+  with tactics is fragile, and explicitly named and reused subterms
+  don't play well with asynchronous proofs.
 \end{Variants}
 
 \ErrMsg \errindex{Proof is not complete}
-- 
cgit v1.2.3


From 12f34b2ebfcbe958ba53b49399c3fcaf01f7a18c Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 11 Apr 2017 09:50:55 -0400
Subject: Generalize cache_term_by_tactic_then

This will allow a cache_term tactic that doesn't suffer from the
Not_found anomalies of abstract in typeclass resolution.
---
 tactics/tactics.ml  | 7 +++++--
 tactics/tactics.mli | 2 +-
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 19627eb530..20de56645f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4907,7 +4907,7 @@ let shrink_entry sign const =
   } in
   (const, args)
 
-let cache_term_by_tactic_then id gk ?(opaque=true) tac tacK =
+let cache_term_by_tactic_then id gk ?(opaque=true) ?(goal_type=None) tac tacK =
   let open Tacticals.New in
   let open Tacmach.New in
   let open Proofview.Notations in
@@ -4927,7 +4927,10 @@ let cache_term_by_tactic_then id gk ?(opaque=true) tac tacK =
 	else (Context.Named.add d s1,s2))
       global_sign (Context.Named.empty, empty_named_context_val) in
   let id = next_global_ident_away id (pf_ids_of_hyps gl) in
-  let concl = it_mkNamedProd_or_LetIn (Proofview.Goal.concl gl) sign in
+  let concl = match goal_type with
+              | None ->  Proofview.Goal.concl gl
+              | Some ty -> ty in
+  let concl = it_mkNamedProd_or_LetIn concl sign in
   let concl =
     try flush_and_check_evars !evdref concl
     with Uninstantiated_evar _ ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index d206011eed..082812c5a6 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -401,7 +401,7 @@ val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -
 
 val unify           : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic
 
-val cache_term_by_tactic_then : Id.t -> Decl_kinds.goal_kind -> ?opaque:bool -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic
+val cache_term_by_tactic_then : Id.t -> Decl_kinds.goal_kind -> ?opaque:bool -> ?goal_type:(constr option) -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic
 
 val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
 
-- 
cgit v1.2.3


From b348a11ccc4913598b72e4ecbb58811bcccd7bfc Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 11 Apr 2017 12:34:07 -0400
Subject: Make opaque optional only for tclABSTRACT

Also move named arguments to the beginning of the functions.  As per
https://github.com/coq/coq/pull/201#discussion_r110928302
---
 tactics/tactics.ml  | 8 ++++----
 tactics/tactics.mli | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 20de56645f..8f791cdcfe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4907,7 +4907,7 @@ let shrink_entry sign const =
   } in
   (const, args)
 
-let cache_term_by_tactic_then id gk ?(opaque=true) ?(goal_type=None) tac tacK =
+let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
   let open Tacticals.New in
   let open Tacmach.New in
   let open Proofview.Notations in
@@ -4985,8 +4985,8 @@ let cache_term_by_tactic_then id gk ?(opaque=true) ?(goal_type=None) tac tacK =
   Sigma.Unsafe.of_pair (tac, evd)
   end }
 
-let abstract_subproof id gk tac ?(opaque=true) =
-  cache_term_by_tactic_then id gk ~opaque:opaque tac (fun lem args -> exact_no_check (applist (lem, args)))
+let abstract_subproof ~opaque id gk tac =
+  cache_term_by_tactic_then ~opaque:opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args)))
 
 let anon_id = Id.of_string "anonymous"
 
@@ -5008,7 +5008,7 @@ let tclABSTRACT ?(opaque=true) name_op tac =
   let s, gk = if opaque
     then name_op_to_name name_op (Proof Theorem) "_subproof"
     else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in
-  abstract_subproof s gk tac ~opaque:opaque
+  abstract_subproof ~opaque:opaque s gk tac
 
 let unify ?(state=full_transparent_state) x y =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 082812c5a6..07a8035427 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -401,7 +401,7 @@ val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -
 
 val unify           : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic
 
-val cache_term_by_tactic_then : Id.t -> Decl_kinds.goal_kind -> ?opaque:bool -> ?goal_type:(constr option) -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic
+val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic
 
 val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
 
-- 
cgit v1.2.3


From 1e046726dc9352f7979ebdeba0d750e44016fea5 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 11 Apr 2017 12:48:23 -0400
Subject: transparent abstract: Respond to review comment

https://github.com/coq/coq/pull/201#discussion_r110952601
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8f791cdcfe..d02fe86653 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4986,7 +4986,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
   end }
 
 let abstract_subproof ~opaque id gk tac =
-  cache_term_by_tactic_then ~opaque:opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args)))
+  cache_term_by_tactic_then ~opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args)))
 
 let anon_id = Id.of_string "anonymous"
 
-- 
cgit v1.2.3


From e4262a89d7bc3d9b985d9a4a939f34176581abcb Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 11 Apr 2017 13:05:54 -0400
Subject: transparent abstract: Respond to review comment

https://github.com/coq/coq/pull/201#discussion_r110957570
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d02fe86653..4654817035 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5008,7 +5008,7 @@ let tclABSTRACT ?(opaque=true) name_op tac =
   let s, gk = if opaque
     then name_op_to_name name_op (Proof Theorem) "_subproof"
     else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in
-  abstract_subproof ~opaque:opaque s gk tac
+  abstract_subproof ~opaque s gk tac
 
 let unify ?(state=full_transparent_state) x y =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
-- 
cgit v1.2.3