feat(library/init/meta): add add_aux_decl and abstract tactics

library/init/meta/async_tactic.lean

@@ -24,15 +24,6 @@ s ← read, return $ task.delay $ λ _,
     undefined_core $ to_string $ fmt () ++ format.line ++ to_fmt s'
   end
 
-private meta def get_undeclared_const (env : environment) (base : name) : ℕ → name | i :=
-let n := base <.> ("_aux_" ++ to_string i) in
-if ¬env^.contains n then n
-else get_undeclared_const (i+1)
-
-meta def new_aux_decl_name : tactic name := do
-env ← get_env, n ← decl_name,
-return $ get_undeclared_const env n 1
-
 meta def prove_goal_async (tac : tactic unit) : tactic unit := do
 ctx ← local_context, revert_lst ctx,
 tgt ← target, tgt ← instantiate_mvars tgt,

library/init/meta/interactive.lean

@@ -341,6 +341,9 @@ tactic.try
 meta def solve1 : itactic → tactic unit :=
 tactic.solve1
 
+meta def abstract (id : opt_ident) (tac : itactic) : tactic unit :=
+tactic.abstract tac id
+
 /--
 This tactic applies to any goal. `assert h : T` adds a new hypothesis of name `h` and type `T` to the current goal and opens a new subgoal with target `T`.
 The new subgoal becomes the main goal.

library/init/meta/tactic.lean

@@ -195,8 +195,8 @@ meta instance {α : Type u} [has_to_tactic_format α] : has_to_tactic_format (li
 
 meta def pair_to_tactic_format_aux {α : Type u} {β : Type v} [has_to_tactic_format α] [has_to_tactic_format β] :
          α × β → tactic format
-| (a, b) := do 
-  fa ← pp a, fb ← pp b, 
+| (a, b) := do
+  fa ← pp a, fb ← pp b,
   return $ to_fmt "(" ++ fa ++ ", " ++ fb ++ ")"
 
 meta instance (α : Type u) (β : Type v) [has_to_tactic_format α] [has_to_tactic_format β] :
@@ -206,7 +206,7 @@ meta def option_to_tactic_format {α : Type u} [has_to_tactic_format α] : optio
 | (some a) := do fa ← pp a, return (to_fmt "(some " ++ fa ++ ")")
 | none     := return "none"
 
-meta instance {α : Type u} [has_to_tactic_format α] : has_to_tactic_format (option α) := 
+meta instance {α : Type u} [has_to_tactic_format α] : has_to_tactic_format (option α) :=
 ⟨option_to_tactic_format⟩
 
 meta instance has_to_format_to_has_to_tactic_format (α : Type) [has_to_format α] : has_to_tactic_format α :=
@@ -402,6 +402,17 @@ meta constant add_decl : declaration → tactic unit
 /- (doc_string env d k) return the doc string for d (if available) -/
 meta constant doc_string : name → tactic string
 meta constant add_doc_string : name → string → tactic unit
+/--
+Create an auxiliary definition with name `c` where `type` and `value` may contain local constants and
+meta-variables. This function collects all dependencies (universe parameters, universe metavariables,
+local constants (aka hypotheses) and metavariables).
+It updates the environment in the tactic_state, and returns an expression of the form
+
+          (c.{l_1 ... l_n} a_1 ... a_m)
+
+where l_i's and a_j's are the collected dependencies.
+-/
+meta constant add_aux_decl (c : name) (type : expr) (val : expr) (is_lemma : bool) : tactic expr
 meta constant module_doc_strings : tactic (list (option name × string))
 /- (set_basic_attribute_core attr_name c_name persistent prio) set attribute attr_name for constant c_name with the given priority.
    If the priority is none, then use default -/
@@ -833,6 +844,35 @@ meta def refine (e : pexpr) : tactic unit :=
 do tgt : expr ← target,
    to_expr `(%%e : %%tgt) >>= exact
 
+private meta def get_undeclared_const (env : environment) (base : name) : ℕ → name | i :=
+let n := base <.> ("_aux_" ++ to_string i) in
+if ¬env^.contains n then n
+else get_undeclared_const (i+1)
+
+meta def new_aux_decl_name : tactic name := do
+env ← get_env, n ← decl_name,
+return $ get_undeclared_const env n 1
+
+private meta def mk_aux_decl_name : option name → tactic name
+| none          := new_aux_decl_name
+| (some suffix) := do p ← decl_name, return $ p ++ suffix
+
+meta def abstract (tac : tactic unit) (suffix : option name := none) : tactic unit :=
+do fail_if_no_goals,
+   gs ← get_goals,
+   type ← target,
+   is_lemma ← is_prop type,
+   m ← mk_meta_var type,
+   set_goals [m],
+   tac,
+   n ← num_goals,
+   when (n ≠ 0) (fail "abstract tactic failed, there are unsolved goals"),
+   set_goals gs,
+   val ← instantiate_mvars m,
+   c   ← mk_aux_decl_name suffix,
+   e   ← add_aux_decl c type val is_lemma,
+   exact e
+
 /- (solve_aux type tac) synthesize an element of 'type' using tactic 'tac' -/
 meta def solve_aux {α : Type} (type : expr) (tac : tactic α) : tactic (α × expr) :=
 do m ← mk_meta_var type,

src/emacs/lean-syntax.el

@@ -11,7 +11,7 @@
   '("import" "prelude" "protected" "private" "noncomputable" "definition" "meta" "renaming"
     "hiding" "exposing" "parameter" "parameters" "begin" "conjecture" "constant" "constants"
     "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises" "theory"
-    "print" "theorem" "proposition" "example" "abstract"
+    "print" "theorem" "proposition" "example"
     "open" "as" "export" "override" "axiom" "axioms" "inductive" "with" "without"
     "structure" "record" "universe" "universes"
     "alias" "help" "precedence" "reserve" "declare_trace" "add_key_equivalence"

src/library/tactic/tactic_state.cpp

@@ -18,6 +18,7 @@ Author: Leonardo de Moura
 #include "library/module.h"
 #include "library/documentation.h"
 #include "library/scoped_ext.h"
+#include "library/aux_definition.h"
 #include "library/unfold_macros.h"
 #include "library/vm/vm_environment.h"
 #include "library/vm/vm_exceptional.h"
@@ -778,6 +779,21 @@ format tactic_state::pp() const {
     }
 }
 
+vm_obj tactic_add_aux_decl(vm_obj const & n, vm_obj const & type, vm_obj const & val, vm_obj const & lemma, vm_obj const & _s) {
+    tactic_state const & s   = to_tactic_state(_s);
+    optional<metavar_decl> g = s.get_main_goal_decl();
+    if (!g) return mk_no_goals_exception(s);
+    try {
+        pair<environment, expr> r =
+            to_bool(lemma) ?
+              mk_aux_lemma(s.env(), s.mctx(), g->get_context(), to_name(n), to_expr(type), to_expr(val))
+            : mk_aux_definition(s.env(), s.mctx(), g->get_context(), to_name(n), to_expr(type), to_expr(val));
+        return mk_tactic_success(to_obj(r.second), set_env(s, r.first));
+    } catch (exception & ex) {
+        return mk_tactic_exception(ex, s);
+    }
+}
+
 void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic_state", "env"}),            tactic_state_env);
     DECLARE_VM_BUILTIN(name({"tactic_state", "format_expr"}),    tactic_state_format_expr);
@@ -816,6 +832,7 @@ void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic", "module_doc_strings"}),   tactic_module_doc_strings);
     DECLARE_VM_BUILTIN(name({"tactic", "open_namespaces"}),      tactic_open_namespaces);
     DECLARE_VM_BUILTIN(name({"tactic", "decl_name"}),            tactic_decl_name);
+    DECLARE_VM_BUILTIN(name({"tactic", "add_aux_decl"}),         tactic_add_aux_decl);
     g_pp_instantiate_goal_mvars = new name{"pp", "instantiate_goal_mvars"};
     register_bool_option(*g_pp_instantiate_goal_mvars, LEAN_DEFAULT_PP_INSTANTIATE_GOAL_MVARS,
                          "(pretty printer) instantiate assigned metavariables before pretty printing goals");

tests/lean/run/abstract_tac.lean

@@ -0,0 +1,9 @@
+def ex (a b c : nat) : a = b → c = b → a = c ∧ b = c :=
+begin
+  intros,
+  split,
+  abstract { transitivity, trace "hello", trace_state, assumption, symmetry, assumption },
+  abstract { symmetry, assumption }
+end
+
+print ex