lean2/src/library/tactic/apply_tactic.cpp

259 lines
10 KiB
C++
Raw Normal View History

/*
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 "util/sstream.h"
#include "kernel/environment.h"
#include "kernel/instantiate.h"
#include "kernel/type_checker.h"
#include "kernel/abstract.h"
#include "kernel/replace_visitor.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/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.
It solves the goal \c gname by applying \c th_fun to the arguments \c alist.
*/
proof_builder mk_apply_tac_proof_builder(proof_builder const & pb, name const & gname, expr const & th_fun, arg_list const & alist) {
return mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
proof_map new_m(m);
if (alist) {
buffer<expr> args;
args.push_back(th_fun);
for (auto const & p2 : alist) {
optional<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 {
proposition_arg const & parg = *(p2.second);
name const & subgoal_name = parg.first;
expr pr = find(m, subgoal_name);
for (auto p : parg.second)
pr = Fun(p.first, p.second, pr);
args.push_back(pr);
new_m.erase(subgoal_name);
}
}
std::reverse(args.begin() + 1, args.end());
new_m.insert(gname, mk_app(args));
} else {
new_m.insert(gname, th_fun);
}
return pb(new_m, a);
});
}
/**
\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");
}
}