feat(library/tactic): add apply_tactic

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

src/kernel/instantiate.cpp

@@ -10,9 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/metavar.h"
 
 namespace lean {
-expr instantiate_with_closed(expr const & a, unsigned n, expr const * s) {
+expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s) {
-    lean_assert(std::all_of(s, s+n, closed));
-
     auto f = [=](expr const & m, unsigned offset) -> expr {
         if (is_var(m)) {
             unsigned vidx = var_idx(m);
@@ -35,6 +33,12 @@ expr instantiate_with_closed(expr const & a, unsigned n, expr const * s) {
     };
     return replace_fn<decltype(f)>(f)(a);
 }
+
+expr instantiate_with_closed(expr const & a, unsigned n, expr const * s) {
+    lean_assert(std::all_of(s, s+n, closed));
+    return instantiate_with_closed_relaxed(a, n, s);
+}
+
 expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst) {
     auto f = [=](expr const & m, unsigned offset) -> expr {
         if (is_var(m)) {

src/kernel/instantiate.h

@@ -18,6 +18,12 @@ inline expr instantiate_with_closed(expr const & e, std::initializer_list<expr>
     return instantiate_with_closed(e, l.size(), l.begin());
 }
 inline expr instantiate_with_closed(expr const & e, expr const & s) { return instantiate_with_closed(e, 1, &s); }
+/**
+   \brief Similar to instantiate_with_closed, but does not use an assertion for
+   testing whether arguments are close or not.
+   This version is useful, for example, when we want to treat metavariables as closed terms.
+*/
+expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s);
 
 /**
    \brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e.

src/library/tactic/CMakeLists.txt

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

src/library/tactic/apply_tactic.cpp

@@ -0,0 +1,154 @@
+/*
+Copyright (c) 2013 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 "kernel/environment.h"
+#include "kernel/instantiate.h"
+#include "library/fo_unify.h"
+#include "library/kernel_bindings.h"
+#include "library/type_inferer.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"
+
+namespace lean {
+static name g_tmp_mvar_name = name::mk_internal_unique_name();
+
+static optional<proof_state> apply_tactic(environment const & env, proof_state const & s,
+                                          expr const & th, expr const & th_type, bool all) {
+    precision prec = s.get_precision();
+    if (prec != precision::Precise && prec != precision::Over) {
+        // it is pointless to apply this tactic, since it will produce UnderOver
+        return none_proof_state();
+    }
+    unsigned num = 0;
+    expr th_type_c = th_type;
+    while (is_pi(th_type_c)) {
+        num++;
+        th_type_c = abst_body(th_type_c);
+    }
+    buffer<expr> mvars;
+    for (unsigned i = 0; i < num; i++)
+        mvars.push_back(mk_metavar(name(g_tmp_mvar_name, i)));
+    th_type_c = instantiate_with_closed_relaxed(th_type_c, mvars.size(), mvars.data());
+    bool found = false;
+    buffer<std::pair<name, goal>> new_goals_buf;
+    // The proof is based on an application of th.
+    // There are two kinds of arguments:
+    //    1) regular arguments computed using unification.
+    //    2) propostions that generate new subgoals.
+    // We use a pair to simulate this "union" type.
+    typedef list<std::pair<expr, name>> arg_list;
+    // We may solve more than one goal.
+    // We store the solved goals using a list of pairs
+    // name, args. Where the 'name' is the name of the solved goal.
+    type_inferer inferer(env);
+    metavar_env new_menv = s.get_menv();
+    list<std::pair<name, arg_list>> proof_info;
+    for (auto const & p : s.get_goals()) {
+        check_interrupted();
+        if (all || !found) {
+            name const & gname = p.first;
+            goal const & g     = p.second;
+            expr const & c     = g.get_conclusion();
+            optional<substitution> subst = fo_unify(th_type_c, c);
+            if (subst) {
+                found = true;
+                th_type_c = th_type;
+                arg_list l;
+                unsigned new_goal_idx = 1;
+                for (auto const & mvar : mvars) {
+                    expr mvar_sol = apply(*subst, mvar);
+                    if (mvar_sol != mvar) {
+                        l.emplace_front(mvar_sol, name());
+                        th_type_c = instantiate(abst_body(th_type_c), mvar_sol);
+                    } else {
+                        if (inferer.is_proposition(abst_domain(th_type_c))) {
+                            name new_gname(gname, new_goal_idx);
+                            new_goal_idx++;
+                            l.emplace_front(expr(), new_gname);
+                            new_goals_buf.emplace_back(new_gname, update(g, abst_domain(th_type_c)));
+                            th_type_c = instantiate(abst_body(th_type_c), mk_constant(new_gname, abst_domain(th_type_c)));
+                        } 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(), abst_domain(th_type_c));
+                            l.emplace_front(new_m, name());
+                            // we use instantiate_with_closed_relaxed because we do not want
+                            // to introduce a lift operator in the new_m
+                            th_type_c = instantiate_with_closed_relaxed(abst_body(th_type_c), 1, &new_m);
+                        }
+                    }
+                }
+                proof_info.emplace_front(gname, l);
+            } else {
+                new_goals_buf.push_back(p);
+            }
+        } else {
+            new_goals_buf.push_back(p);
+        }
+    }
+    if (found) {
+        proof_builder pb     = s.get_proof_builder();
+        proof_builder new_pb = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
+                proof_map new_m(m);
+                for (auto const & p1 : proof_info) {
+                    name const & gname = p1.first;
+                    arg_list const & l = p1.second;
+                    buffer<expr> args;
+                    args.push_back(th);
+                    for (auto const & p2 : l) {
+                        expr const & arg = p2.first;
+                        if (arg) {
+                            // TODO(Leo): decide if we instantiate the metavars in the end or not.
+                            args.push_back(arg);
+                        } else {
+                            name const & subgoal_name = p2.second;
+                            args.push_back(find(m, subgoal_name));
+                            new_m.erase(subgoal_name);
+                        }
+                    }
+                    std::reverse(args.begin() + 1, args.end());
+                    new_m.insert(gname, mk_app(args));
+                }
+                return pb(new_m, a);
+            });
+        goals new_gs = to_list(new_goals_buf.begin(), new_goals_buf.end());
+        return some(proof_state(precision::Over, new_gs, new_menv, new_pb, s.get_cex_builder()));
+    } else {
+        return none_proof_state();
+    }
+}
+
+tactic apply_tactic(expr const & th, expr const & th_type, bool all) {
+    return mk_tactic01([=](environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
+            return apply_tactic(env, s, th, th_type, all);
+        });
+}
+
+tactic apply_tactic(name const & th_name, bool all) {
+    return mk_tactic01([=](environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
+            object const & obj = env.find_object(th_name);
+            if (obj && (obj.is_theorem() || obj.is_axiom()))
+                return apply_tactic(env, s, mk_constant(th_name), obj.get_type(), all);
+            else
+                return none_proof_state();
+        });
+}
+
+int mk_apply_tactic(lua_State * L) {
+    int nargs = lua_gettop(L);
+    return push_tactic(L, apply_tactic(to_name_ext(L, 1), nargs >= 2 ? lua_toboolean(L, 2) : true));
+}
+
+void open_apply_tactic(lua_State * L) {
+    SET_GLOBAL_FUN(mk_apply_tactic,     "apply_tactic");
+}
+}

src/library/tactic/apply_tactic.h

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

src/library/tactic/register_module.h

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "library/tactic/proof_state.h"
 #include "library/tactic/tactic.h"
 #include "library/tactic/boolean.h"
+#include "library/tactic/apply_tactic.h"
 
 namespace lean {
 inline void open_tactic_module(lua_State * L) {
@@ -21,6 +22,7 @@ inline void open_tactic_module(lua_State * L) {
     open_proof_state(L);
     open_tactic(L);
     open_boolean(L);
+    open_apply_tactic(L);
 }
 inline void register_tactic_module() {
     script_state::register_module(open_tactic_module);

tests/lean/apply_tac1.lean

@@ -0,0 +1,18 @@
+Variable f : Int -> Int -> Bool
+Variable P : Int -> Int -> Bool
+Axiom Ax1 (x y : Int) (H : P x y) : (f x y)
+Theorem T1 (a : Int) : (P a a) => (f a a).
+      apply imp_tactic
+      apply (** apply_tactic("Ax1") **)
+      apply assumption_tactic
+      done
+Variable b : Int
+Axiom Ax2 (x : Int) : (f x b)
+(**
+simple_tac = REPEAT(ORELSE(imp_tactic, assumption_tactic, apply_tactic("Ax2"), apply_tactic("Ax1")))
+**)
+Theorem T2 (a : Int) : (P a a) => (f a a).
+     apply simple_tac
+     done
+
+Show Environment 1.

tests/lean/apply_tac1.lean.expected.out

@@ -0,0 +1,10 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: f
+  Assumed: P
+  Assumed: Ax1
+  Proved: T1
+  Assumed: b
+  Assumed: Ax2
+  Proved: T2
+Theorem T2 (a : ℤ) : (P a a) ⇒ (f a a) := Discharge (λ H : P a a, Ax1 a a H)