feat(frontends/lean): automatically open 'tactic' namespace (if it is not already open) in 'by' and 'begin-end' expressions

src/frontends/lean/builtin_cmds.cpp

@@ -347,10 +347,12 @@ environment open_export_cmd(parser & p, bool open) {
                             env = add_abbrev(p, env, as+id, ns+id);
                     }
                 } else {
-                    throw parser_error("invalid 'open/export' command option, identifier, 'hiding' or 'renaming' expected", p.pos());
+                    throw parser_error("invalid 'open/export' command option, "
+                                       "identifier, 'hiding' or 'renaming' expected", p.pos());
                 }
                 if (found_explicit && !exceptions.empty())
-                    throw parser_error("invalid 'open/export' command option, mixing explicit and implicit 'open/export' options", p.pos());
+                    throw parser_error("invalid 'open/export' command option, "
+                                       "mixing explicit and implicit 'open/export' options", p.pos());
                 p.check_token_next(get_rparen_tk(), "invalid 'open/export' command option, ')' expected");
             }
             if (!found_explicit) {

src/frontends/lean/builtin_exprs.cpp

@@ -9,9 +9,12 @@ Author: Leonardo de Moura
 #include "library/annotation.h"
 #include "library/placeholder.h"
 #include "library/explicit.h"
+#include "library/aliases.h"
+#include "library/scoped_ext.h"
 #include "library/tactic/tactic.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "library/tactic/exact_tactic.h"
+#include "library/tactic/util.h"
 #include "library/typed_expr.h"
 #include "library/choice.h"
 #include "library/let.h"
@@ -113,9 +116,20 @@ static expr parse_placeholder(parser & p, unsigned, expr const *, pos_info const
     return p.save_pos(mk_explicit_expr_placeholder(), pos);
 }
 
+static environment open_tactic_namespace(parser & p) {
+    if (!is_tactic_namespace_open(p.env())) {
+        environment env = using_namespace(p.env(), p.ios(), "tactic");
+        env = add_aliases(env, name("tactic"), name());
+        return env;
+    } else {
+        return p.env();
+    }
+}
+
 static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
     parser::no_undef_id_error_scope scope(p);
-    expr t = p.parse_expr();
+    environment env = open_tactic_namespace(p);
+    expr t = p.parse_scoped_expr(0, nullptr, env);
     return p.mk_by(t, pos);
 }
 
@@ -126,6 +140,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) {
     buffer<expr> tacs;
     bool first = true;
     parser::no_undef_id_error_scope scope(p);
+    environment env = open_tactic_namespace(p);
     while (!p.curr_is_token(get_end_tk())) {
         if (first)
             first = false;
@@ -137,7 +152,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) {
                           p.curr_is_token(get_assume_tk()) || p.curr_is_token(get_take_tk()) ||
                           p.curr_is_token(get_fun_tk()));
         auto pos = p.pos();
-        expr tac = p.parse_expr();
+        expr tac = p.parse_scoped_expr(0, nullptr, env);
         if (use_exact)
             tac = p.mk_app(get_exact_tac_fn(), tac, pos);
         if (pre_tac)

src/library/tactic/CMakeLists.txt

@@ -1,5 +1,6 @@
 add_library(tactic goal.cpp proof_state.cpp tactic.cpp elaborate.cpp
 apply_tactic.cpp intros_tactic.cpp rename_tactic.cpp trace_tactic.cpp
-exact_tactic.cpp unfold_tactic.cpp expr_to_tactic.cpp init_module.cpp)
+exact_tactic.cpp unfold_tactic.cpp expr_to_tactic.cpp util.cpp
+init_module.cpp)
 
 target_link_libraries(tactic ${LEAN_LIBS})

tests/lean/run/tactic1.lean

@@ -1,5 +1,4 @@
 import logic
-open tactic
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : A
 := by assumption

tests/lean/run/tactic10.lean

@@ -1,5 +1,4 @@
 import logic
-open tactic
 
 theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a
 := by rapply iff.intro;

tests/lean/run/tactic11.lean

@@ -1,5 +1,4 @@
 import logic
-open tactic
 
 theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a
 := have H1 [visible] : a → b, -- We need to mark H1 as fact, otherwise it is not visible by tactics

tests/lean/run/tactic16.lean

@@ -1,5 +1,4 @@
 import logic data.string
-open tactic
 
 constant A : Type.{1}
 constant f : A → A → A

tests/lean/run/tactic23.lean

@@ -1,5 +1,4 @@
 import logic
-open tactic
 
 inductive nat : Type :=
 zero : nat,
@@ -24,7 +23,7 @@ coercion num_to_nat
 check 2 + 3
 
 -- Define an assump as an alias for the eassumption tactic
-definition assump : tactic := eassumption
+definition assump : tactic := tactic.eassumption
 
 theorem T1 {p : nat → Prop} {a : nat } (H : p (a+2)) : ∃ x, p (succ x)
 := by apply exists_intro; assump