From 8e45064f256dc89227a02ce337077efe86ea5fb9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Dec 2013 22:40:34 -0800 Subject: [PATCH] feat(library/tactic/apply_tactic): improved parametric apply_tactic Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 10 + src/library/tactic/apply_tactic.cpp | 327 +++++++++++++++---------- src/library/tactic/apply_tactic.h | 5 +- tests/lean/discharge.lean | 7 + tests/lean/discharge.lean.expected.out | 4 + tests/lean/disjcases.lean | 10 + tests/lean/disjcases.lean.expected.out | 7 + 7 files changed, 238 insertions(+), 132 deletions(-) create mode 100644 tests/lean/discharge.lean create mode 100644 tests/lean/discharge.lean.expected.out create mode 100644 tests/lean/disjcases.lean create mode 100644 tests/lean/disjcases.lean.expected.out diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 8e82dca7e..dc4e72441 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -17,6 +17,7 @@ Author: Leonardo de Moura #include #include #include +#include "util/flet.h" #include "util/luaref.h" #include "util/scoped_map.h" #include "util/exception.h" @@ -167,6 +168,11 @@ class parser::imp { pos_info m_last_cmd_pos; pos_info m_last_script_pos; tactic_hints m_tactic_hints; + // If true then return error when parsing identifiers and it is not local or global. + // We set this flag off when parsing tactics. The apply_tac may reference + // a hypothesis in the proof state. This hypothesis is not visible until we + // execute the tactic. + bool m_check_identifiers; script_state * m_script_state; @@ -875,6 +881,8 @@ class parser::imp { } else { throw parser_error(sstream() << "invalid object reference, object '" << id << "' is not an expression.", p); } + } else if (!m_check_identifiers) { + return mk_constant(id); } else { throw parser_error(sstream() << "unknown identifier '" << id << "'", p); } @@ -1389,6 +1397,7 @@ class parser::imp { }); } else if (curr_is_lparen()) { next(); + flet set(m_check_identifiers, false); expr pr = parse_expr(); check_rparen_next("invalid apply command, ')' expected"); return ::lean::apply_tactic(pr); @@ -2440,6 +2449,7 @@ public: m_elaborator(env), m_use_exceptions(use_exceptions), m_interactive(interactive) { + m_check_identifiers = true; m_script_state = S; if (m_script_state) { m_script_state->apply([&](lua_State * L) { diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index 410d4c470..a0d1bb7ed 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -6,167 +6,234 @@ Author: Leonardo de Moura */ #include #include +#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/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 proposition_arg; +// We use a pair to simulate this "union" type. +typedef list, optional>> arg_list; -static optional apply_tactic(ro_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))); - metavar_env new_menv = s.get_menv().copy(); - th_type_c = instantiate(th_type_c, mvars.size(), mvars.data(), new_menv); - 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) propositions that generate new subgoals. - typedef std::pair proposition_arg; - // We use a pair to simulate this "union" type. - typedef list, - optional>> 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_checker checker(env); - 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 = cons(mk_pair(some_expr(mvar_sol), optional()), l); - th_type_c = instantiate(abst_body(th_type_c), mvar_sol, new_menv); - } else { - expr arg_type = abst_domain(th_type_c); - 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); - } - l = cons(mk_pair(none_expr(), some(proposition_arg(new_gname, extra_hs))), l); - new_goals_buf.emplace_back(new_gname, goal(add_hypothesis.get_hypotheses(), arg_type)); - th_type_c = instantiate(abst_body(th_type_c), 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)); - l = cons(mk_pair(some_expr(new_m), optional()), l); - th_type_c = instantiate(abst_body(th_type_c), 1, &new_m, new_menv); - } - } +/** + \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); + buffer args; + args.push_back(th_fun); + for (auto const & p2 : alist) { + optional 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); } - 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) { - optional 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)); - } - 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, bool all) { - return mk_tactic01([=](ro_environment const & env, io_state const &, proof_state const & s) -> optional { - expr th_type = type_inferer(env)(th, context(), s.get_menv().copy()); - return apply_tactic(env, s, th, th_type, all); + std::reverse(args.begin() + 1, args.end()); + new_m.insert(gname, mk_app(args)); + return pb(new_m, a); }); } -tactic apply_tactic(name const & th_name, bool all) { +/** + \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 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 apply_tactic(ro_environment const & env, proof_state const & s, + expr th, optional 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(); + } + type_checker checker(env); + auto const & p = head(s.get_goals()); + name const & gname = p.first; + goal const & g = p.second; + metavar_env new_menv = s.get_menv().copy(); + expr th_type_c; + if (th_type) { + th_type_c = *th_type; + } else { + metavar_env tmp_menv; + buffer ucs; + th = apply_tactic_preprocessor_fn(env, tmp_menv, g.get_hypotheses())(th); + th_type_c = checker.check(th, context(), tmp_menv, ucs); + elaborator elb(env, tmp_menv, ucs.size(), ucs.data()); + try { + metavar_env new_tmp_menv = elb.next(); + th = new_tmp_menv->instantiate_metavars(th); + th_type_c = new_tmp_menv->instantiate_metavars(th_type_c); + } catch (exception & ex) { + return none_proof_state(); + } + move_metavars_fn move(new_menv); + th = move(th); + th_type_c = move(th_type_c); + } + expr conclusion = th_type_c; + buffer 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 subst = fo_unify(conclusion, g.get_conclusion()); + if (!subst) { + return none_proof_state(); + } + th_type_c = apply(*subst, th_type_c); + th = apply(*subst, th); + arg_list alist; + unsigned new_goal_idx = 1; + buffer> 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()), alist); + th_type_c = instantiate(abst_body(th_type_c), mvar_subst, new_menv); + } else { + expr arg_type = abst_domain(th_type_c); + 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_c = instantiate(abst_body(th_type_c), 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()), alist); + th_type_c = instantiate(abst_body(th_type_c), 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())); +} + +tactic apply_tactic(expr const & th) { + return mk_tactic01([=](ro_environment const & env, io_state const &, proof_state const & s) -> optional { + // 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 { + 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 { optional 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); + 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) { - int nargs = lua_gettop(L); - bool all = nargs >= 2 ? lua_toboolean(L, 2) : true; if (is_expr(L, 1)) - return push_tactic(L, apply_tactic(to_expr(L, 1), all)); + return push_tactic(L, apply_tactic(to_expr(L, 1))); else - return push_tactic(L, apply_tactic(to_name_ext(L, 1), all)); + return push_tactic(L, apply_tactic(to_name_ext(L, 1))); } void open_apply_tactic(lua_State * L) { diff --git a/src/library/tactic/apply_tactic.h b/src/library/tactic/apply_tactic.h index ac09325a4..aeead74d0 100644 --- a/src/library/tactic/apply_tactic.h +++ b/src/library/tactic/apply_tactic.h @@ -7,7 +7,8 @@ Author: Leonardo de Moura #pragma once #include "library/tactic/tactic.h" namespace lean { -tactic apply_tactic(expr const & th, bool all = true); -tactic apply_tactic(name const & th_name, bool all = true); +tactic apply_tactic(expr const & th); +tactic apply_tactic(expr const & th, expr const & th_type); +tactic apply_tactic(name const & th_name); void open_apply_tactic(lua_State * L); } diff --git a/tests/lean/discharge.lean b/tests/lean/discharge.lean new file mode 100644 index 000000000..878349912 --- /dev/null +++ b/tests/lean/discharge.lean @@ -0,0 +1,7 @@ +Check @Discharge +Theorem T (a b : Bool) : a => b => b => a. + apply Discharge. + apply Discharge. + apply Discharge. + assumption. + done. \ No newline at end of file diff --git a/tests/lean/discharge.lean.expected.out b/tests/lean/discharge.lean.expected.out new file mode 100644 index 000000000..c9da3cd33 --- /dev/null +++ b/tests/lean/discharge.lean.expected.out @@ -0,0 +1,4 @@ + Set: pp::colors + Set: pp::unicode +@Discharge : Π (a b : Bool), (a → b) → (a ⇒ b) + Proved: T diff --git a/tests/lean/disjcases.lean b/tests/lean/disjcases.lean new file mode 100644 index 000000000..a7a3084aa --- /dev/null +++ b/tests/lean/disjcases.lean @@ -0,0 +1,10 @@ +Variables a b c : Bool +Axiom H : a \/ b +Theorem T (a b : Bool) : a \/ b => b \/ a. + apply Discharge. + apply (DisjCases H). + apply Disj2. + assumption. + apply Disj1. + assumption. + done. \ No newline at end of file diff --git a/tests/lean/disjcases.lean.expected.out b/tests/lean/disjcases.lean.expected.out new file mode 100644 index 000000000..24be58d13 --- /dev/null +++ b/tests/lean/disjcases.lean.expected.out @@ -0,0 +1,7 @@ + Set: pp::colors + Set: pp::unicode + Assumed: a + Assumed: b + Assumed: c + Assumed: H + Proved: T