feat(library/tactic): add apply tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/builtin_tactic_cmds.cpp

@@ -9,14 +9,16 @@ Author: Leonardo de Moura
 
 namespace lean {
 static name g_bang("!");
+tactic parse_fail_tactic(parser &, pos_info const &) { return fail_tactic(); }
+tactic parse_id_tactic(parser &, pos_info const &) { return id_tactic(); }
+tactic parse_now_tactic(parser &, pos_info const &) { return now_tactic(); }
+tactic parse_print_tactic(parser & p, pos_info const & pos) {
+    return trace_state_tactic(p.get_stream_name(), pos);
+}
+tactic parse_assumption_tactic(parser &, pos_info const &) { return assumption_tactic(); }
+tactic parse_apply_tactic(parser & p, pos_info const &) { return p.parse_apply(); }
 
-tactic parse_fail_tactic(parser &) { return fail_tactic(); }
+tactic parse_unfold_tactic(parser & p, pos_info const &) {
-tactic parse_id_tactic(parser &) { return id_tactic(); }
-tactic parse_now_tactic(parser &) { return now_tactic(); }
-tactic parse_show_tactic(parser &) { return trace_state_tactic(); }
-tactic parse_assumption_tactic(parser &) { return assumption_tactic(); }
-
-tactic parse_unfold_tactic(parser & p) {
     auto pos = p.pos();
     expr id  = p.parse_expr();
     if (!is_constant(id))
@@ -24,7 +26,7 @@ tactic parse_unfold_tactic(parser & p) {
     return unfold_tactic(const_name(id));
 }
 
-tactic parse_repeat_tactic(parser & p) {
+tactic parse_repeat_tactic(parser & p, pos_info const &) {
     tactic t = p.parse_tactic();
     if (p.curr_is_numeral()) {
         unsigned n = p.parse_small_nat();
@@ -34,7 +36,7 @@ tactic parse_repeat_tactic(parser & p) {
     }
 }
 
-tactic parse_echo_tactic(parser & p) {
+tactic parse_echo_tactic(parser & p, pos_info const &) {
     if (!p.curr_is_string())
         throw parser_error("invalid 'echo' tactic, string expected", p.pos());
     tactic r = trace_tactic(p.get_str_val());
@@ -47,11 +49,12 @@ void add_tactic(tactic_cmd_table & t, tactic_cmd_info && info) { t.insert(info.g
 tactic_cmd_table get_builtin_tactic_cmds() {
     tactic_cmd_table t;
     add_tactic(t, tactic_cmd_info("fail", "always fail tactic", parse_fail_tactic));
-    add_tactic(t, tactic_cmd_info("show", "show goals tactic", parse_show_tactic));
+    add_tactic(t, tactic_cmd_info("print", "print current goals", parse_print_tactic));
     add_tactic(t, tactic_cmd_info("now",  "succeeds only if all goals have been solved", parse_now_tactic));
     add_tactic(t, tactic_cmd_info("echo", "trace tactic: display message", parse_echo_tactic));
     add_tactic(t, tactic_cmd_info("unfold", "unfold definition", parse_unfold_tactic));
     add_tactic(t, tactic_cmd_info("repeat", "repeat tactic", parse_repeat_tactic));
+    add_tactic(t, tactic_cmd_info("apply", "apply tactic", parse_apply_tactic));
     add_tactic(t, tactic_cmd_info("!", "repeat tactic", parse_repeat_tactic));
     add_tactic(t, tactic_cmd_info("id", "do nothing tactic", parse_id_tactic));
     add_tactic(t, tactic_cmd_info("assumption", "solve goal if there is an assumption that is identical to the conclusion",

src/frontends/lean/cmd_table.h

@@ -14,7 +14,7 @@ namespace lean {
 class parser;
 
 typedef std::function<environment(parser&)> command_fn;
-typedef std::function<tactic(parser&)> tactic_command_fn;
+typedef std::function<tactic(parser&, pos_info const &)> tactic_command_fn;
 
 template<typename F>
 struct cmd_info_tmpl {

src/frontends/lean/elaborator.cpp

@@ -615,10 +615,17 @@ public:
             if (optional<tactic> t = get_tactic_for(mvar)) {
                 proof_state_seq seq = (*t)(m_env, m_ios, ps);
                 if (auto r = seq.pull()) {
-                    if (auto pr = to_proof(r->first)) {
+                    try {
-                        subst = subst.assign(mlocal_name(mvar), *pr, justification());
+                        if (auto pr = to_proof(r->first)) {
-                    } else {
+                            subst = subst.assign(mlocal_name(mvar), *pr, justification());
-                        display_unsolved_proof_state(mvar, r->first, "unsolved subgoals");
+                        } else {
+                            display_unsolved_proof_state(mvar, r->first, "unsolved subgoals");
+                        }
+                    } catch (exception & ex) {
+                        regular out(m_env, m_ios);
+                        display_error_pos(out, m_pos_provider, mvar);
+                        out << " proof generation failed\n    >> ";
+                        display_error(out, nullptr, ex);
                     }
                 } else {
                     // tactic failed to produce any result

src/frontends/lean/local_decls.h

@@ -20,22 +20,25 @@ namespace lean {
 template<typename V>
 class local_decls {
     typedef rb_map<name, std::pair<V, unsigned>, name_quick_cmp> map;
-    typedef list<std::pair<map, unsigned>> scopes;
+    typedef list<std::tuple<map, unsigned, list<V>>> scopes;
     map       m_map;
     unsigned  m_counter;
     scopes    m_scopes;
+    list<V>   m_values;
 public:
     local_decls():m_counter(1) {}
     local_decls(local_decls const & d):m_map(d.m_map), m_counter(d.m_counter), m_scopes(d.m_scopes) {}
-    void insert(name const & k, V const & v) { m_map.insert(k, mk_pair(v, m_counter)); m_counter++; }
+    void insert(name const & k, V const & v) { m_map.insert(k, mk_pair(v, m_counter)); m_counter++; m_values = list<V>(v, m_values); }
     V const * find(name const & k) const { auto it = m_map.find(k); return it ? &(it->first) : nullptr; }
     unsigned find_idx(name const & k) const { auto it = m_map.find(k); return it ? it->second : 0; }
     bool contains(name const & k) const { return m_map.contains(k); }
-    void push() { m_scopes = scopes(mk_pair(m_map, m_counter), m_scopes); }
+    list<V> const & get_values() const { return m_values; }
+    void push() { m_scopes = scopes(std::make_tuple(m_map, m_counter, m_values), m_scopes); }
     void pop() {
         lean_assert(!is_nil(m_scopes));
-        m_map     = head(m_scopes).first;
+        m_map     = std::get<0>(head(m_scopes));
-        m_counter = head(m_scopes).second;
+        m_counter = std::get<1>(head(m_scopes));
+        m_values  = std::get<2>(head(m_scopes));
         m_scopes  = tail(m_scopes);
     }
     struct mk_scope {

src/frontends/lean/parser.cpp

@@ -26,6 +26,7 @@ Author: Leonardo de Moura
 #include "library/module.h"
 #include "library/scoped_ext.h"
 #include "library/error_handling/error_handling.h"
+#include "library/tactic/apply_tactic.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/notation_cmd.h"
 #include "frontends/lean/elaborator.h"
@@ -407,6 +408,8 @@ static name g_max("max");
 static name g_imax("imax");
 static name g_cup("\u2294");
 static name g_import("import");
+static name g_show("show");
+static name g_have("have");
 static unsigned g_level_add_prec = 10;
 static unsigned g_level_cup_prec = 5;
 
@@ -552,6 +555,11 @@ expr parser::elaborate(expr const & e) {
     return ::lean::elaborate(m_env, m_ios, e, m_hints, &pp);
 }
 
+expr parser::elaborate(expr const & e, name_generator const & ngen, list<parameter> const & ctx) {
+    parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
+    return ::lean::elaborate(m_env, m_ios, e, ngen, m_hints, substitution(), ctx, &pp);
+}
+
 expr parser::elaborate(environment const & env, expr const & e) {
     parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
     return ::lean::elaborate(env, m_ios, e, m_hints, &pp);
@@ -957,6 +965,41 @@ expr parser::abstract(unsigned num_params, parameter const * ps, expr const & e,
     return r;
 }
 
+tactic parser::parse_apply() {
+    auto p = pos();
+    expr e = parse_expr();
+    for_each(e, [&](expr const & e, unsigned) {
+            if (is_local(e)) {
+                auto it = get_local(mlocal_name(e));
+                lean_assert(it);
+                if (!it->m_bi.is_contextual())
+                    throw parser_error(sstream() << "invalid 'apply' tactic, it references non contextual local '"
+                                       << local_pp_name(e) << "'", p);
+            }
+            return has_local(e);
+        });
+    buffer<parameter> tmp;
+    for (parameter const & p : m_local_decls.get_values()) {
+        if (p.m_bi.is_contextual() && is_local(p.m_local))
+            tmp.push_back(p);
+    }
+    list<parameter> ctx = to_list(tmp.begin(), tmp.end());
+    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
+            name_generator ngen     = s.ngen();
+            auto const &   s_locals = s.get_init_locals();
+            expr           new_e    = elaborate(e, ngen.mk_child(), ctx);
+            proof_state    new_s(s, ngen);
+            buffer<expr> tmp;
+            for (auto const & p : ctx)
+                tmp.push_back(p.m_local);
+            std::reverse(tmp.begin(), tmp.end());
+            new_e = abstract_locals(new_e, tmp.size(), tmp.data());
+            for (auto const & l : s_locals)
+                new_e = instantiate(new_e, l);
+            return apply_tactic(new_e)(env, ios, new_s);
+        });
+}
+
 tactic parser::parse_tactic(unsigned /* rbp */) {
     if (curr_is_token(g_lparen) || curr_is_token(g_lbracket)) {
         bool paren = curr_is_token(g_lparen);
@@ -989,20 +1032,22 @@ tactic parser::parse_tactic(unsigned /* rbp */) {
             }
             return r;
         }
+    } else if (curr_is_token(g_have) || curr_is_token(g_show)) {
+        return parse_apply();
     } else {
         name id;
         auto p = pos();
         if (curr_is_identifier()) {
             id = get_name_val();
             next();
-        } else if (curr_is_keyword()) {
+        } else if (curr_is_keyword() || curr_is_command()) {
             id = get_token_info().value();
             next();
         } else {
             throw parser_error("invalid tactic, '(' or tactic command expected", p);
         }
         if (auto it = tactic_cmds().find(id)) {
-            return it->get_fn()(*this);
+            return it->get_fn()(*this, p);
         } else {
             throw parser_error(sstream() << "unknown tactic command '" << id << "'", p);
         }

src/frontends/lean/parser.h

@@ -227,6 +227,7 @@ public:
     expr pi_abstract(buffer<parameter> const & ps, expr const & e) { return pi_abstract(ps, e, pos_of(e)); }
 
     tactic parse_tactic(unsigned rbp = 0);
+    tactic parse_apply();
 
     struct local_scope { parser & m_p; environment m_env; local_scope(parser & p); ~local_scope(); };
     void add_local_level(name const & n, level const & l);
@@ -263,6 +264,7 @@ public:
     struct no_undef_id_error_scope { parser & m_p; bool m_old; no_undef_id_error_scope(parser &); ~no_undef_id_error_scope(); };
 
     expr elaborate(expr const & e);
+    expr elaborate(expr const & e, name_generator const & ngen, list<parameter> const & ctx);
     expr elaborate(environment const & env, expr const & e);
     std::pair<expr, expr> elaborate(name const & n, expr const & t, expr const & v);
 

src/kernel/abstract.cpp

@@ -35,11 +35,11 @@ expr abstract_locals(expr const & e, unsigned n, expr const * subst) {
     return replace(e, [=](expr const & m, unsigned offset) -> optional<expr> {
             if (!has_local(m))
                 return some_expr(m); // expression m does not contain local constants
-            if (closed(e)) {
+            if (is_local(m)) {
                 unsigned i = n;
                 while (i > 0) {
                     --i;
-                    if (subst[i] == m)
+                    if (mlocal_name(subst[i]) == mlocal_name(m))
                         return some_expr(copy_tag(m, mk_var(offset + n - i - 1)));
                 }
             }

src/library/tactic/CMakeLists.txt

@@ -1,6 +1,6 @@
-add_library(tactic goal.cpp cex_builder.cpp proof_builder.cpp proof_state.cpp tactic.cpp)
+add_library(tactic goal.cpp cex_builder.cpp proof_builder.cpp proof_state.cpp
+  tactic.cpp apply_tactic.cpp)
 
-#  apply_tactic.cpp
 # simplify_tactic.cpp)
 
 target_link_libraries(tactic ${LEAN_LIBS})

src/library/tactic/apply_tactic.cpp

@@ -1,257 +1,122 @@
 /*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
 #include <utility>
-#include <algorithm>
+#include "util/lazy_list_fn.h"
-#include "util/sstream.h"
+#include "kernel/for_each_fn.h"
-#include "kernel/environment.h"
 #include "kernel/instantiate.h"
-#include "kernel/type_checker.h"
 #include "kernel/abstract.h"
-#include "kernel/replace_visitor.h"
+#include "kernel/type_checker.h"
-#include "library/io_state_stream.h"
-#include "library/fo_unify.h"
-#include "library/placeholder.h"
 #include "library/kernel_bindings.h"
-#include "library/elaborator/elaborator.h"
+#include "library/unifier.h"
-#include "library/tactic/goal.h"
-#include "library/tactic/proof_builder.h"
-#include "library/tactic/proof_state.h"
-#include "library/tactic/tactic.h"
 #include "library/tactic/apply_tactic.h"
 
-#include "kernel/formatter.h"
-
 namespace lean {
-static name g_tmp_mvar_name = name::mk_internal_unique_name();
-// The proof is based on an application of a function that returns a proof.
-// There are two kinds of arguments:
-//    1) regular arguments computed using unification.
-//    2) propositions that generate new subgoals.
-typedef std::pair<name, hypotheses> proposition_arg;
-// We use a pair to simulate this "union" type.
-typedef list<std::pair<optional<expr>, optional<proposition_arg>>> arg_list;
-
 /**
-   \brief Return the proof builder for the apply_tactic.
+   \brief Traverse \c e and collect metavariable applications (?m l1 ... ln), and store in result.
-
+   The function only succeeds if all metavariable applications are "simple", i.e., the arguments
-   It solves the goal \c gname by applying \c th_fun to the arguments \c alist.
+   are distinct local constants.
 */
-proof_builder mk_apply_tac_proof_builder(proof_builder const & pb, name const & gname, expr const & th_fun, arg_list const & alist) {
+bool collect_simple_metas(expr const & e, buffer<expr> & result) {
-    return mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
+    bool failed = false;
-            proof_map new_m(m);
+    // collect metavariables
-            if (alist) {
+    for_each(e, [&](expr const & e, unsigned) {
-                buffer<expr> args;
+            if (is_meta(e)) {
-                args.push_back(th_fun);
+                if (!is_simple_meta(e)) {
-                for (auto const & p2 : alist) {
+                    failed = true;
-                    optional<expr> const & arg = p2.first;
+                } else {
-                    if (arg) {
+                    result.push_back(e);
-                        // TODO(Leo): decide if we instantiate the metavars in the end or not.
+                    return false; /* do not visit type */
-                        args.push_back(*arg);
+                }
-                    } else {
+            }
-                        proposition_arg const & parg = *(p2.second);
+            return !failed && has_metavar(e);
-                        name const & subgoal_name = parg.first;
+        });
-                        expr pr = find(m, subgoal_name);
+    return !failed;
-                        for (auto p : parg.second)
+}
-                            pr = Fun(p.first, p.second, pr);
+
-                        args.push_back(pr);
+tactic apply_tactic(expr const & e) {
-                        new_m.erase(subgoal_name);
+    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
+            precision prec = s.get_precision();
+            if ((prec != precision::Precise && prec != precision::Over) || empty(s.get_goals())) {
+                // it is pointless to apply this tactic, since it will produce UnderOver
+                return proof_state_seq();
+            }
+            goals const & gs    = s.get_goals();
+            name gname          = head(gs).first;
+            goal  g             = head(gs).second;
+            goals rest_gs       = tail(gs);
+            expr const & C      = g.get_conclusion();
+            name_generator ngen = s.ngen();
+            type_checker tc(env, ngen.mk_child());
+            expr new_e          = e;
+            expr new_e_type     = tc.infer(new_e);
+            buffer<expr> meta_buffer;
+            if (!collect_simple_metas(new_e, meta_buffer))
+                return proof_state_seq();
+            // add more metavariables while new_e_type is a Pi
+            while (is_pi(new_e_type)) {
+                expr meta  = g.mk_meta(ngen.next(), binding_domain(new_e_type));
+                meta_buffer.push_back(meta);
+                new_e      = mk_app(new_e, meta);
+                new_e_type = instantiate(binding_body(new_e_type), meta);
+            }
+            list<expr> metas = to_list(meta_buffer.begin(), meta_buffer.end());
+            // TODO(Leo): we should use unifier plugin
+            lazy_list<substitution> substs = unify(env, C, new_e_type, ngen.mk_child(), ios.get_options());
+            return map2<proof_state>(substs, [=](substitution const & subst) -> proof_state {
+                    // apply substitution to remaining goals
+                    name_generator new_ngen(ngen);
+                    type_checker tc(env, new_ngen.mk_child());
+                    goals new_gs = map(rest_gs, [&](named_goal const & ng) {
+                            return named_goal(ng.first, ng.second.instantiate_metavars(subst));
+                        });
+                    expr P            = subst.instantiate_metavars_wo_jst(new_e);
+                    goal tmp_g        = g.instantiate_metavars(subst);
+                    unsigned subgoal_idx = 1;
+                    buffer<std::pair<name, expr>> trace_buffer;
+                    // add unassigned metavariables as new goals
+                    buffer<named_goal> subgoals;
+                    for (expr const & meta : metas) {
+                        if (!subst.is_assigned(get_app_fn(meta))) {
+                            name new_gname(gname, subgoal_idx);
+                            expr new_C = subst.instantiate_metavars_wo_jst(tc.infer(meta));
+                            goal new_g(tmp_g.get_hypotheses(), new_C);
+                            subgoals.emplace_back(new_gname, new_g);
+                            trace_buffer.emplace_back(new_gname, meta);
+                            subgoal_idx++;
+                        }
                     }
-                }
+                    new_gs = to_list(subgoals.begin(), subgoals.end(), new_gs);
-                std::reverse(args.begin() + 1, args.end());
+                    list<std::pair<name, expr>> trace = to_list(trace_buffer.begin(), trace_buffer.end());
-                new_m.insert(gname, mk_app(args));
+                    proof_builder pb = s.get_pb();
-            } else {
+                    proof_builder new_pb([=](proof_map const & m, substitution const & pb_subst) {
-                new_m.insert(gname, th_fun);
+                            proof_map new_m(m);
-            }
+                            substitution new_subst;
-            return pb(new_m, a);
+                            for (auto const & p : trace) {
+                                expr pr   = find(new_m, p.first);
+                                expr meta = p.second;
+                                buffer<expr> meta_args;
+                                expr mvar = get_app_args(meta, meta_args);
+                                unsigned i = meta_args.size();
+                                while (i > 0) {
+                                    --i;
+                                    pr = Fun(meta_args[i], pr);
+                                }
+                                new_subst = new_subst.assign(mlocal_name(mvar), pr, justification());
+                                new_m.erase(p.first);
+                            }
+                            new_m.insert(gname, new_subst.instantiate_metavars_wo_jst(P));
+                            return pb(new_m, pb_subst);
+                        });
+                    return proof_state(s, new_gs, new_pb, new_ngen);
+                });
         });
 }
 
-/**
+int mk_apply_tactic(lua_State * L) { return push_tactic(L, apply_tactic(to_expr(L, 1))); }
-   \brief Functional object for replacing placeholders with
-   metavariables and attaching type to constants that refer
-   hypotheses in the given goal.
-*/
-class apply_tactic_preprocessor_fn : public replace_visitor {
-    ro_environment const & m_env;
-    metavar_env const &    m_menv;
-    hypotheses const &     m_hypotheses;
-protected:
-    expr visit_constant(expr const & e, context const & c) {
-        if (is_placeholder(e)) {
-            return m_menv->mk_metavar(c, const_type(e));
-        } else if (m_env->find_object(const_name(e))) {
-            return e;
-        } else {
-            for (auto const & p : m_hypotheses) {
-                if (p.first == const_name(e))
-                    return mk_constant(const_name(e), p.second);
-            }
-            throw exception(sstream() << "apply_tactic failed, unknown identifier '" << const_name(e) << "'");
-        }
-    }
-
-public:
-    apply_tactic_preprocessor_fn(ro_environment const & env, metavar_env const & menv, hypotheses const & hs):
-        m_env(env), m_menv(menv), m_hypotheses(hs) {}
-};
-
-/**
-   \brief Functional object for moving the metavariable occurring in an expression to
-   another metavar environment.
-*/
-class move_metavars_fn : public replace_visitor {
-    name_map<expr>         m_map;
-    metavar_env const &    m_menv;
-    expr visit_metavar(expr const & mvar, context const &) {
-        name const & mvar_name = metavar_name(mvar);
-        auto it = m_map.find(mvar_name);
-        if (it == m_map.end()) {
-            expr r = m_menv->mk_metavar();
-            m_map[mvar_name] = r;
-            return r;
-        } else {
-            return it->second;
-        }
-    }
-public:
-    move_metavars_fn(metavar_env const & menv):m_menv(menv) {}
-};
-
-static optional<proof_state> apply_tactic_core(ro_environment const & env, proof_state const & s,
-                                               expr th, expr th_type, metavar_env const & new_menv) {
-    type_checker checker(env);
-    auto const & p       = head(s.get_goals());
-    name const & gname   = p.first;
-    goal const & g       = p.second;
-    expr conclusion = th_type;
-    buffer<expr> mvars;
-    unsigned i = 0;
-    while (is_pi(conclusion)) {
-        expr mvar = new_menv->mk_metavar();
-        mvars.push_back(mvar);
-        conclusion = instantiate(abst_body(conclusion), mvar, new_menv);
-        i++;
-    }
-    optional<substitution> subst = fo_unify(conclusion, g.get_conclusion());
-    if (!subst) {
-        return none_proof_state();
-    }
-    th_type = apply(*subst, th_type);
-    th      = apply(*subst, th);
-    arg_list alist;
-    unsigned new_goal_idx = 1;
-    buffer<std::pair<name, goal>> new_goals_buf;
-    for (auto const & mvar : mvars) {
-        expr mvar_subst = apply(*subst, mvar);
-        if (mvar_subst != mvar) {
-            alist = cons(mk_pair(some_expr(mvar_subst), optional<proposition_arg>()), alist);
-            th_type = instantiate(abst_body(th_type), mvar_subst, new_menv);
-        } else {
-            expr arg_type = abst_domain(th_type);
-            if (checker.is_flex_proposition(arg_type, context(), new_menv)) {
-                name new_gname(gname, new_goal_idx);
-                new_goal_idx++;
-                hypotheses hs = g.get_hypotheses();
-                update_hypotheses_fn add_hypothesis(hs);
-                hypotheses extra_hs;
-                while (is_pi(arg_type)) {
-                    expr d = abst_domain(arg_type);
-                    name n = arg_to_hypothesis_name(abst_name(arg_type), d, env, context(), new_menv);
-                    n   = add_hypothesis(n, d);
-                    extra_hs.emplace_front(n, d);
-                    arg_type = instantiate(abst_body(arg_type), mk_constant(n, d), new_menv);
-                }
-                alist = cons(mk_pair(none_expr(), some(proposition_arg(new_gname, extra_hs))), alist);
-                new_goals_buf.emplace_back(new_gname, goal(add_hypothesis.get_hypotheses(), arg_type));
-                th_type = instantiate(abst_body(th_type), mk_constant(new_gname, arg_type), new_menv);
-            } else {
-                // we have to create a new metavar in menv
-                // since we do not have a substitution for mvar, and
-                // it is not a proposition
-                /// expr new_m = new_menv->mk_metavar(context(), some_expr(arg_type));
-                alist = cons(mk_pair(some_expr(mvar), optional<proposition_arg>()), alist);
-                th_type = instantiate(abst_body(th_type), mvar, new_menv);
-            }
-        }
-    }
-    proof_builder pb = s.get_proof_builder();
-    proof_builder new_pb = mk_apply_tac_proof_builder(pb, gname, th, alist);
-    goals new_gs = to_list(new_goals_buf.begin(), new_goals_buf.end(), tail(s.get_goals()));
-    return some(proof_state(precision::Over, new_gs, new_menv, new_pb, s.get_cex_builder()));
-}
-
-
-static optional<proof_state> apply_tactic(ro_environment const & env, proof_state const & s,
-                                          expr th, optional<expr> const & th_type) {
-    precision prec = s.get_precision();
-    if ((prec != precision::Precise && prec != precision::Over) || empty(s.get_goals())) {
-        // it is pointless to apply this tactic, since it will produce UnderOver
-        return none_proof_state();
-    }
-    if (th_type) {
-        metavar_env new_menv = s.get_menv().copy();
-        return apply_tactic_core(env, s, th, *th_type, new_menv);
-    } else {
-        metavar_env tmp_menv;
-        type_checker checker(env);
-        auto const & p = head(s.get_goals());
-        goal const & g = p.second;
-        buffer<unification_constraint> ucs;
-        th = apply_tactic_preprocessor_fn(env, tmp_menv, g.get_hypotheses())(th);
-        expr th_type_inferred = checker.check(th, context(), tmp_menv, ucs);
-        elaborator elb(env, tmp_menv, ucs.size(), ucs.data());
-        try {
-            while (true) {
-                metavar_env new_tmp_menv = elb.next();
-                metavar_env new_menv = s.get_menv().copy();
-                move_metavars_fn move(new_menv);
-                expr new_th               = move(new_tmp_menv->instantiate_metavars(th));
-                expr new_th_type_inferred = move(new_tmp_menv->instantiate_metavars(th_type_inferred));
-                auto r = apply_tactic_core(env, s, new_th, new_th_type_inferred, new_menv);
-                if (r)
-                    return r;
-            }
-        } catch (exception & ex) {
-            return none_proof_state();
-        }
-    }
-}
-
-tactic apply_tactic(expr const & th) {
-    return mk_tactic01([=](ro_environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
-            // th may contain placeholder
-            // TODO(Leo)
-            return apply_tactic(env, s, th, none_expr());
-        });
-}
-
-tactic apply_tactic(expr const & th, expr const & th_type) {
-    return mk_tactic01([=](ro_environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
-            return apply_tactic(env, s, th, some_expr(th_type));
-        });
-}
-
-tactic apply_tactic(name const & th_name) {
-    return mk_tactic01([=](ro_environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
-            optional<object> obj = env->find_object(th_name);
-            if (obj && (obj->is_theorem() || obj->is_axiom()))
-                return apply_tactic(env, s, mk_constant(th_name), some_expr(obj->get_type()));
-            else
-                return none_proof_state();
-        });
-}
-
-int mk_apply_tactic(lua_State * L) {
-    if (is_expr(L, 1))
-        return push_tactic(L, apply_tactic(to_expr(L, 1)));
-    else
-        return push_tactic(L, apply_tactic(to_name_ext(L, 1)));
-}
-
 void open_apply_tactic(lua_State * L) {
     SET_GLOBAL_FUN(mk_apply_tactic,     "apply_tac");
 }

src/library/tactic/apply_tactic.h

@@ -1,14 +1,13 @@
 /*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
 #pragma once
+#include "util/lua.h"
 #include "library/tactic/tactic.h"
 namespace lean {
-tactic apply_tactic(expr const & th);
+tactic apply_tactic(expr const & e);
-tactic apply_tactic(expr const & th, expr const & th_type);
-tactic apply_tactic(name const & th_name);
 void open_apply_tactic(lua_State * L);
 }

src/library/tactic/goal.cpp

@@ -82,7 +82,7 @@ expr goal::mk_meta(name const & n, expr const & type) const {
                 if (is_local(e)) {
                     bool found = false;
                     for (hypothesis const & h : m_hypotheses) {
-                        if (h.second && h.first == e) {
+                        if (mlocal_name(h.first) == mlocal_name(e)) {
                             found = true;
                             break;
                         }
@@ -112,6 +112,14 @@ expr goal::mk_meta(name const & n, expr const & type) const {
     return mk_app(mk_metavar(n, t), args);
 }
 
+goal goal::instantiate_metavars(substitution const & s) const {
+    hypotheses hs = map(m_hypotheses, [&](hypothesis const & h) {
+            return mk_pair(s.instantiate_metavars_wo_jst(h.first), h.second);
+        });
+    expr c = s.instantiate_metavars_wo_jst(m_conclusion);
+    return goal(hs, c);
+}
+
 static bool validate(expr const & r, hypotheses const & hs) {
     bool failed = false;
     for_each(r, [&](expr const & e, unsigned) {

src/library/tactic/goal.h

@@ -40,6 +40,7 @@ public:
         and each hypothesis only contains local constants that occur in the previous hypotheses.
     */
     bool validate() const;
+    goal instantiate_metavars(substitution const & s) const;
     format pp(environment const & env, formatter const & fmt, options const & opts) const;
 };
 

src/library/tactic/proof_state.cpp

@@ -146,11 +146,9 @@ io_state_stream const & operator<<(io_state_stream const & out, proof_state cons
 
 optional<expr> to_proof(proof_state const & s) {
     if (s.is_proof_final_state()) {
-        try {
+        substitution a;
-            substitution a;
+        proof_map  m;
-            proof_map  m;
+        return some_expr(s.get_pb()(m, a));
-            return some_expr(s.get_pb()(m, a));
-        } catch (...) {}
     }
     return none_expr();
 }

src/library/tactic/proof_state.h

@@ -15,7 +15,8 @@ Author: Leonardo de Moura
 #include "library/tactic/cex_builder.h"
 
 namespace lean {
-typedef list<std::pair<name, goal>> goals;
+typedef std::pair<name, goal> named_goal;
+typedef list<named_goal> goals;
 /** \brief Return the name of the i-th goal, return none if i == 0 or i > size(g) */
 optional<name> get_ith_goal_name(goals const & gs, unsigned i);
 
@@ -50,6 +51,8 @@ public:
         proof_state(s.m_precision, gs, pb, s.m_cex_builder, ngen, s.m_init_locals) {}
     proof_state(proof_state const & s, goals const & gs, proof_builder const & pb):proof_state(s, gs, pb, s.m_ngen) {}
     proof_state(proof_state const & s, goals const & gs):proof_state(s, gs, s.m_proof_builder) {}
+    proof_state(proof_state const & s, name_generator const & ngen):
+        proof_state(s.m_precision, s.m_goals, s.m_proof_builder, s.m_cex_builder, ngen, s.m_init_locals) {}
     precision get_precision() const { return m_precision; }
     goals const & get_goals() const { return m_goals; }
     proof_builder const & get_pb() const { return m_proof_builder; }

src/library/tactic/register_module.h

@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "library/tactic/proof_builder.h"
 #include "library/tactic/proof_state.h"
 #include "library/tactic/tactic.h"
-// #include "library/tactic/apply_tactic.h"
+#include "library/tactic/apply_tactic.h"
 // #include "library/tactic/simplify_tactic.h"
 
 namespace lean {
@@ -19,7 +19,7 @@ inline void open_tactic_module(lua_State * L) {
     open_proof_builder(L);
     open_proof_state(L);
     open_tactic(L);
-    // open_apply_tactic(L);
+    open_apply_tactic(L);
     // open_simplify_tactic(L);
 }
 inline void register_tactic_module() {

src/library/tactic/tactic.cpp

@@ -84,9 +84,10 @@ tactic trace_tactic(char const * msg) {
     return trace_tactic(std::string(msg));
 }
 
-tactic trace_state_tactic() {
+tactic trace_state_tactic(std::string const & fname, std::pair<unsigned, unsigned> const & pos) {
     return tactic1([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state {
-            diagnostic(env, ios) << s << endl;
+            diagnostic(env, ios) << fname << ":" << pos.first << ":" << pos.second << ": proof state\n"
+                                 << s << endl;
             ios.get_diagnostic_channel().get_stream().flush();
             return s;
         });
@@ -517,7 +518,6 @@ static int mk_now_tactic(lua_State * L)         {  return push_tactic(L, now_tac
 static int mk_fail_tactic(lua_State * L)        {  return push_tactic(L, fail_tactic()); }
 static int mk_trace_tactic(lua_State * L)       {  return push_tactic(L, trace_tactic(luaL_checkstring(L, 1))); }
 static int mk_assumption_tactic(lua_State * L)  {  return push_tactic(L, assumption_tactic()); }
-static int mk_trace_state_tactic(lua_State * L) {  return push_tactic(L, trace_state_tactic()); }
 static int mk_unfold_tactic(lua_State * L)      {
     int nargs = lua_gettop(L);
     if (nargs == 0)
@@ -567,7 +567,6 @@ void open_tactic(lua_State * L) {
     SET_GLOBAL_FUN(mk_id_tactic,          "id_tac");
     SET_GLOBAL_FUN(mk_now_tactic,         "now_tac");
     SET_GLOBAL_FUN(mk_fail_tactic,        "fail_tac");
-    SET_GLOBAL_FUN(mk_trace_state_tactic, "show_tac");
     SET_GLOBAL_FUN(mk_assumption_tactic,  "assumption_tac");
     SET_GLOBAL_FUN(mk_unfold_tactic,      "unfold_tac");
     SET_GLOBAL_FUN(mk_beta_tactic,        "beta_tac");

src/library/tactic/tactic.h

@@ -41,7 +41,7 @@ class sstream;
 tactic trace_tactic(sstream const & msg);
 tactic trace_tactic(std::string const & msg);
 /** \brief Return a tactic that just displays the input state in the diagnostic channel. */
-tactic trace_state_tactic();
+tactic trace_state_tactic(std::string const & fname, std::pair<unsigned, unsigned> const & pos);
 /** \brief Create a tactic that applies \c t, but suppressing diagnostic messages. */
 tactic suppress_trace(tactic const & t);
 /** \brief Return a tactic that performs \c t1 followed by \c t2. */

src/library/unifier.cpp

@@ -46,6 +46,11 @@ optional<expr> is_simple_meta(expr const & e, buffer<expr> & args) {
     return some_expr(m);
 }
 
+bool is_simple_meta(expr const & e) {
+    buffer<expr> args;
+    return (bool)is_simple_meta(e, args); // NOLINT
+}
+
 // Return true if all local constants in \c e are in locals
 bool context_check(expr const & e, buffer<expr> const & locals) {
     bool failed = false;

src/library/unifier.h

@@ -23,6 +23,8 @@ namespace lean {
 unsigned get_unifier_max_steps(options const & opts);
 bool get_unifier_use_exceptions(options const & opts);
 
+bool is_simple_meta(expr const & e);
+
 enum class unify_status { Solved, Failed, Unsupported };
 /**
     \brief Handle the easy-cases: first-order unification, higher-order patterns, identical terms, and terms without metavariables.

src/util/lazy_list_fn.h

@@ -122,6 +122,22 @@ lazy_list<T> map(lazy_list<T> const & l, F && f, char const * cname = "lazy list
         });
 }
 
+/**
+   \brief Create a lazy list by applying \c f to the elements of \c l.
+*/
+template<typename To, typename From, typename F>
+lazy_list<To> map2(lazy_list<From> const & l, F && f, char const * cname = "lazy list") {
+    return mk_lazy_list<To>([=]() {
+            typename lazy_list<From>::maybe_pair p = l.pull();
+            if (!p) {
+                return typename lazy_list<To>::maybe_pair();
+            } else {
+                check_system(cname);
+                return some(mk_pair(f(p->first), map2<To>(p->second, f, cname)));
+            }
+        });
+}
+
 /**
    \brief Create a lazy list that contains only the elements of \c l that satisfies \c pred.
 

tests/lean/run/tactic3.lean

@@ -1,6 +1,6 @@
 import logic
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : A
-:= by [echo "first try",  show, now  |
+:= by [echo "first try",  print, now  |
        echo "second try", fail       |
        echo "third try", exact]

tests/lean/run/tactic4.lean

@@ -3,4 +3,4 @@ import logic
 definition id {A : Type} (a : A) := a
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A
-:= by [unfold id, show, exact]
+:= by [unfold id, print, exact]

tests/lean/run/tactic5.lean

@@ -3,4 +3,4 @@ import logic
 definition id {A : Type} (a : A) := a
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A
-:= by [!(unfold id, show), exact]
+:= by [!(unfold id, print), exact]

tests/lean/run/tactic7.lean

@@ -0,0 +1,4 @@
+import logic
+
+theorem tst {A B : Bool} (H1 : A) (H2 : B) : A ∧ B ∧ A
+:= by (print, apply and_intro, print, exact, apply and_intro, print, !exact)

tests/lean/run/tactic8.lean

@@ -0,0 +1,7 @@
+import logic
+
+theorem tst {A B : Bool} (H1 : A) (H2 : B) : A ∧ B ∧ A
+:= by (apply and_intro,
+       show A, from H1,
+       show B ∧ A, from and_intro H2 H1)
+check @tst