feat(library/tactic): add 'rename' hypothesis tactic

src/emacs/lean-syntax.el

@@ -118,7 +118,8 @@
      (,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
      ;; tactics
      (,(rx word-start
-           (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "back" "beta" "done" "exact" "repeat")
+           (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "rename"
+               "back" "beta" "done" "exact" "repeat")
            word-end)
       . 'font-lock-constant-face)
      ;; Types

src/frontends/lean/builtin_tactics.cpp

@@ -20,9 +20,16 @@ static expr parse_apply(parser & p, unsigned, expr const *, pos_info const & pos
     return p.save_pos(mk_apply_tactic_macro(e), pos);
 }
 
+static expr parse_rename(parser & p, unsigned, expr const *, pos_info const & pos) {
+    name from = p.check_id_next("invalid 'rename' tactic, identifier expected");
+    name to   = p.check_id_next("invalid 'rename' tactic, identifier expected");
+    return p.save_pos(mk_rename_tactic_macro(from, to), pos);
+}
+
 void init_nud_tactic_table(parse_table & r) {
     expr x0 = mk_var(0);
-    r = r.add({transition("apply", mk_ext_action(parse_apply))}, x0);
+    r = r.add({transition("apply",  mk_ext_action(parse_apply))}, x0);
+    r = r.add({transition("rename", mk_ext_action(parse_rename))}, x0);
 }
 
 void initialize_builtin_tactics() {

src/frontends/lean/token_table.cpp

@@ -76,7 +76,7 @@ void init_token_table(token_table & t) {
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {"local", 0},
-         {"apply", 0}, {nullptr, 0}};
+         {"apply", 0}, {"rename", 0}, {nullptr, 0}};
 
     char const * commands[] =
         {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "coercion",

src/library/tactic/expr_to_tactic.cpp

@@ -137,11 +137,17 @@ bool is_tactic_macro(expr const & e) {
 }
 
 static name * g_apply_tactic_name = nullptr;
+static name * g_rename_tactic_name = nullptr;
 
 expr mk_apply_tactic_macro(expr const & e) {
     return mk_tactic_macro(*g_apply_tactic_name, e);
 }
 
+expr mk_rename_tactic_macro(name const & from, name const & to) {
+    expr args[2] = { Const(from), Const(to) };
+    return mk_tactic_macro(*g_rename_tactic_name, 2, args);
+}
+
 expr_to_tactic_fn const & get_tactic_macro_fn(expr const & e) {
     lean_assert(is_tactic_macro(e));
     return static_cast<tactic_macro_definition_cell const*>(macro_def(e).raw())->get_fn();
@@ -307,6 +313,7 @@ void initialize_expr_to_tactic() {
                                 });
 
     g_apply_tactic_name = new name(*g_tactic_name, "apply");
+    g_rename_tactic_name = new name(*g_tactic_name, "rename");
 
     name builtin_tac_name(*g_tactic_name, "builtin");
     name exact_tac_name(*g_tactic_name, "exact");
@@ -376,6 +383,13 @@ void initialize_expr_to_tactic() {
                       check_macro_args(e, 1, "invalid 'apply' tactic, it must have one argument");
                       return apply_tactic(fn, macro_arg(e, 0));
                   });
+    register_tacm(*g_rename_tactic_name,
+                  [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                      check_macro_args(e, 2, "invalid 'rename' tactic, it must have two arguments");
+                      if (!is_constant(macro_arg(e, 0)) || !is_constant(macro_arg(e, 1)))
+                          throw expr_to_tactic_exception(e, "invalid 'rename' tactic, arguments must be identifiers");
+                      return rename_tactic(const_name(macro_arg(e, 0)), const_name(macro_arg(e, 1)));
+                  });
     register_tac(exact_tac_name,
                  [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
                      // TODO(Leo): use elaborate_fn
@@ -417,6 +431,7 @@ void finalize_expr_to_tactic() {
     delete g_id_tac_fn;
     delete g_exact_tac_fn;
     delete g_apply_tactic_name;
+    delete g_rename_tactic_name;
     delete g_tactic_macros;
     delete g_map;
     delete g_tactic_name;

src/library/tactic/expr_to_tactic.h

@@ -52,6 +52,7 @@ expr mk_tactic_macro(name const & kind, unsigned num_args, expr const * args);
 expr mk_tactic_macro(name const & kind, expr const & e);
 bool is_tactic_macro(expr const & e);
 expr mk_apply_tactic_macro(expr const & e);
+expr mk_rename_tactic_macro(name const & from, name const & to);
 
 /** \brief Exception used to report a problem when an expression is being converted into a tactic. */
 class expr_to_tactic_exception : public tactic_exception {

src/library/tactic/tactic.cpp

@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/type_checker.h"
 #include "kernel/for_each_fn.h"
+#include "kernel/replace_fn.h"
 #include "kernel/replace_visitor.h"
 #include "library/kernel_bindings.h"
 #include "library/tactic/tactic.h"
@@ -211,6 +212,39 @@ tactic discard(tactic const & t, unsigned k) {
         });
 }
 
+tactic rename_tactic(name const & from, name const & to) {
+    return tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
+            goals const & gs = s.get_goals();
+            if (empty(gs))
+                return none_proof_state();
+            goal const & g        = head(gs);
+            goals const & rest_gs = tail(gs);
+            buffer<expr> locals;
+            get_app_args(g.get_meta(), locals);
+            unsigned i = locals.size();
+            optional<expr> from_local;
+            while (i > 0) {
+                --i;
+                expr const & local = locals[i];
+                if (local_pp_name(local) == from) {
+                    from_local = local;
+                    break;
+                }
+            }
+            if (!from_local)
+                return none_proof_state();
+            expr to_local = mk_local(mlocal_name(*from_local), to, mlocal_type(*from_local), local_info(*from_local));
+            auto fn = [&](expr const & e) {
+                if (is_local(e) && mlocal_name(e) == mlocal_name(*from_local))
+                    return some_expr(to_local);
+                else
+                    return none_expr();
+            };
+            goal new_g(replace(g.get_meta(), fn), replace(g.get_type(), fn));
+            return some(proof_state(s, goals(new_g, rest_gs)));
+        });
+}
+
 tactic assumption_tactic() {
     return tactic01([](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
             substitution subst = s.get_subst();

src/library/tactic/tactic.h

@@ -127,6 +127,9 @@ tactic take(tactic const & t, unsigned k);
 */
 tactic discard(tactic const & t, unsigned k);
 
+/** \brief Return a tactic that renames hypothesis \c from into \c to in the current goal. */
+tactic rename_tactic(name const & from, name const & to);
+
 typedef std::function<bool(environment const & env, io_state const & ios, proof_state const & s)> proof_state_pred; // NOLINT
 /**
     \brief Return a tactic that applies the predicate \c p to the input state.

tests/lean/run/rename_tac.lean

@@ -0,0 +1,10 @@
+import tools.tactic
+open tactic
+
+theorem foo (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c :=
+begin
+  apply eq.trans,
+  apply Hbc,
+  rename Hab Foo,
+  apply Foo
+end