From 029ef57abda4e91ebf81904fc9ede670e5392479 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Dec 2013 03:22:12 -0800 Subject: [PATCH] feat(library/tactic): add apply_tactic Signed-off-by: Leonardo de Moura --- src/kernel/instantiate.cpp | 10 +- src/kernel/instantiate.h | 6 + src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/apply_tactic.cpp | 154 ++++++++++++++++++++++++ src/library/tactic/apply_tactic.h | 13 ++ src/library/tactic/register_module.h | 2 + tests/lean/apply_tac1.lean | 18 +++ tests/lean/apply_tac1.lean.expected.out | 10 ++ 8 files changed, 211 insertions(+), 4 deletions(-) create mode 100644 src/library/tactic/apply_tactic.cpp create mode 100644 src/library/tactic/apply_tactic.h create mode 100644 tests/lean/apply_tac1.lean create mode 100644 tests/lean/apply_tac1.lean.expected.out diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index 343590f01d..1f17ca4d32 100644 --- a/src/kernel/instantiate.cpp +++ b/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) { - lean_assert(std::all_of(s, s+n, closed)); - +expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s) { 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(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)) { diff --git a/src/kernel/instantiate.h b/src/kernel/instantiate.h index eaebc9de50..ef5d1748c2 100644 --- a/src/kernel/instantiate.h +++ b/src/kernel/instantiate.h @@ -18,6 +18,12 @@ inline expr instantiate_with_closed(expr const & e, std::initializer_list 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. diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index ff3f1d26e9..07b267a738 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/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}) diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp new file mode 100644 index 0000000000..39cc3a18c4 --- /dev/null +++ b/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 +#include +#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 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 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> 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> 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> 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 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 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 { + 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 { + 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"); +} +} diff --git a/src/library/tactic/apply_tactic.h b/src/library/tactic/apply_tactic.h new file mode 100644 index 0000000000..3d8f99387a --- /dev/null +++ b/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); +} diff --git a/src/library/tactic/register_module.h b/src/library/tactic/register_module.h index 2240314dd2..4d913b9300 100644 --- a/src/library/tactic/register_module.h +++ b/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); diff --git a/tests/lean/apply_tac1.lean b/tests/lean/apply_tac1.lean new file mode 100644 index 0000000000..c79a9908be --- /dev/null +++ b/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. \ No newline at end of file diff --git a/tests/lean/apply_tac1.lean.expected.out b/tests/lean/apply_tac1.lean.expected.out new file mode 100644 index 0000000000..56ce2649db --- /dev/null +++ b/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)