diff --git a/src/library/basic_thms.cpp b/src/library/basic_thms.cpp index 60c22fa05..1a1861a43 100644 --- a/src/library/basic_thms.cpp +++ b/src/library/basic_thms.cpp @@ -9,8 +9,6 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "library/basic_thms.h" -#include "kernel/kernel_exception.h" - namespace lean { MK_CONSTANT(trivial, name("Trivial")); diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index a01edc633..8d51acd51 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -12,6 +12,8 @@ Author: Leonardo de Moura #include "util/sstream.h" #include "util/interrupt.h" #include "util/lazy_list_fn.h" +#include "kernel/replace_visitor.h" +#include "kernel/instantiate.h" #include "library/kernel_bindings.h" #include "library/tactic/tactic.h" @@ -180,7 +182,7 @@ tactic suppress_trace(tactic const & t) { tactic assumption_tactic() { return mk_tactic01([](environment const &, io_state const &, proof_state const & s) -> optional { list> proofs; - goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal { + goals new_gs = map_goals(s, [&](name const & gname, goal const & g) -> goal { expr const & c = g.get_conclusion(); expr pr; for (auto const & p : g.get_hypotheses()) { @@ -191,7 +193,7 @@ tactic assumption_tactic() { } } if (pr) { - proofs.emplace_front(ng, pr); + proofs.emplace_front(gname, pr); return goal(); } else { return g; @@ -200,7 +202,7 @@ tactic assumption_tactic() { if (empty(proofs)) return none_proof_state(); proof_builder new_pb = add_proofs(s.get_proof_builder(), proofs); - return some(proof_state(s, new_goals, new_pb)); + return some(proof_state(s, new_gs, new_pb)); }); } @@ -348,6 +350,60 @@ tactic focus(tactic const & t, int i) { }); } +class unfold_fn : public replace_visitor { +protected: + name const & m_name; + expr const & m_def; + bool m_unfolded; + + virtual expr visit_constant(expr const & c, context const &) { + if (const_name(c) == m_name) { + m_unfolded = true; + return m_def; + } else { + return c; + } + } + + virtual expr visit_app(expr const & e, context const & ctx) { + expr const & f = arg(e, 0); + if (is_constant(f) && const_name(f) == m_name) { + buffer new_args; + for (unsigned i = 0; i < num_args(e); i++) + new_args.push_back(visit(arg(e, i), ctx)); + if (is_lambda(new_args[0])) + return apply_beta(new_args[0], new_args.size() - 1, new_args.data() + 1); + else + return mk_app(new_args); + } else { + return replace_visitor::visit_app(e, ctx); + } + } + +public: + unfold_fn(name const & n, expr const & d):m_name(n), m_def(d), m_unfolded(false) {} + bool unfolded() const { return m_unfolded; } +}; + +tactic unfold_tactic(name const & n) { + return mk_tactic01([=](environment const & env, io_state const &, proof_state const & s) -> optional { + object const & obj = env.find_object(n); + if (!obj || !obj.is_definition()) + return none_proof_state(); // tactic failed + unfold_fn fn(n, obj.get_value()); + goals new_gs = map_goals(s, [&](name const &, goal const & g) -> goal { + hypotheses new_hs = map(g.get_hypotheses(), [&](hypothesis const & h) { return hypothesis(h.first, fn(h.second)); }); + expr new_c = fn(g.get_conclusion()); + return goal(new_hs, new_c); + }); + if (fn.unfolded()) { + return proof_state(s, new_gs); + } else { + return none_proof_state(); + } + }); +} + DECL_UDATA(proof_state_seq) static const struct luaL_Reg proof_state_seq_m[] = { @@ -622,6 +678,7 @@ static int mk_fail_tactic(lua_State * L) { return push_tactic(L, fail_ta 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) { return push_tactic(L, unfold_tactic(to_name_ext(L, 1))); } static const struct luaL_Reg tactic_m[] = { {"__gc", tactic_gc}, // never throws @@ -673,6 +730,7 @@ void open_tactic(lua_State * L) { SET_GLOBAL_FUN(mk_trace_state_tactic, "show_tactic"); SET_GLOBAL_FUN(mk_assumption_tactic, "assumption_tactic"); SET_GLOBAL_FUN(mk_assumption_tactic, "assump_tactic"); + SET_GLOBAL_FUN(mk_unfold_tactic, "unfold_tactic"); SET_GLOBAL_FUN(mk_lua_tactic01, "tactic"); // HOL-like tactic names diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index ced7e84c6..0dae51e25 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -287,6 +287,10 @@ tactic focus(tactic const & t, name const & gname); */ tactic focus(tactic const & t, int i); inline tactic focus(tactic const & t) { return focus(t, 1); } +/** + \brief Return a tactic that unfolds the definition named \c n. +*/ +tactic unfold_tactic(name const & n); UDATA_DEFS_CORE(proof_state_seq) UDATA_DEFS(tactic); diff --git a/tests/lean/tactic9.lean b/tests/lean/tactic9.lean new file mode 100644 index 000000000..9d18c4643 --- /dev/null +++ b/tests/lean/tactic9.lean @@ -0,0 +1,11 @@ +Definition f(a : Bool) : Bool := not a. + +Theorem T (a b : Bool) : a \/ b => (f b) => a := _. + apply imp_tactic + apply imp_tactic + apply disj_hyp_tactic + apply (** unfold_tactic("f") **) + apply assumption_tactic + apply absurd_tactic + done +Show Environment 1. \ No newline at end of file diff --git a/tests/lean/tactic9.lean.expected.out b/tests/lean/tactic9.lean.expected.out new file mode 100644 index 000000000..8c911a4b5 --- /dev/null +++ b/tests/lean/tactic9.lean.expected.out @@ -0,0 +1,6 @@ + Set: pp::colors + Set: pp::unicode + Defined: f + Proved: T +Theorem T (a b : Bool) : a ∨ b ⇒ (f b) ⇒ a := + Discharge (λ H : a ∨ b, Discharge (λ H::1 : f b, DisjCases H (λ H : a, H) (λ H : b, AbsurdImpAny b a H H::1)))