From 7d0100a3400b70c19422c5ef920acef2ef38293a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Oct 2014 15:26:16 -0700 Subject: [PATCH] feat(library/tactic): add 'intros' tactic --- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/builtin_tactics.cpp | 10 ++++ src/frontends/lean/token_table.cpp | 2 +- src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/expr_to_tactic.cpp | 32 ++++++++++- src/library/tactic/expr_to_tactic.h | 2 + src/library/tactic/intros_tactic.cpp | 76 ++++++++++++++++++++++++++ src/library/tactic/intros_tactic.h | 11 ++++ src/library/tactic/proof_state.h | 2 + tests/lean/run/intros.lean | 33 +++++++++++ 10 files changed, 167 insertions(+), 5 deletions(-) create mode 100644 src/library/tactic/intros_tactic.cpp create mode 100644 src/library/tactic/intros_tactic.h create mode 100644 tests/lean/run/intros.lean diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 1bcf3287b..a0014c67a 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -118,7 +118,7 @@ (,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face) ;; tactics (,(rx word-start - (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "rename" + (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "rename" "intros" "back" "beta" "done" "exact" "repeat") word-end) . 'font-lock-constant-face) diff --git a/src/frontends/lean/builtin_tactics.cpp b/src/frontends/lean/builtin_tactics.cpp index d6f8cd2c9..837c40d96 100644 --- a/src/frontends/lean/builtin_tactics.cpp +++ b/src/frontends/lean/builtin_tactics.cpp @@ -26,10 +26,20 @@ static expr parse_rename(parser & p, unsigned, expr const *, pos_info const & po return p.save_pos(mk_rename_tactic_macro(from, to), pos); } +static expr parse_intros(parser & p, unsigned, expr const *, pos_info const & pos) { + buffer ns; + while (p.curr_is_identifier()) { + ns.push_back(p.get_name_val()); + p.next(); + } + return p.save_pos(mk_intros_tactic_macro(ns), pos); +} + void init_nud_tactic_table(parse_table & r) { expr x0 = mk_var(0); r = r.add({transition("apply", mk_ext_action(parse_apply))}, x0); r = r.add({transition("rename", mk_ext_action(parse_rename))}, x0); + r = r.add({transition("intros", mk_ext_action(parse_intros))}, x0); } void initialize_builtin_tactics() { diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 2265d3eef..7b1e278e5 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -76,7 +76,7 @@ void init_token_table(token_table & t) { {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {"local", 0}, - {"apply", 0}, {"rename", 0}, {nullptr, 0}}; + {"apply", 0}, {"rename", 0}, {"intros", 0}, {nullptr, 0}}; char const * commands[] = {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "coercion", diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index fdc14f749..6db389f6d 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,4 +1,4 @@ add_library(tactic goal.cpp proof_state.cpp tactic.cpp apply_tactic.cpp -expr_to_tactic.cpp init_module.cpp) +intros_tactic.cpp expr_to_tactic.cpp init_module.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 020175759..4d50f3f88 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -16,6 +16,7 @@ Author: Leonardo de Moura #include "library/kernel_serializer.h" #include "library/tactic/expr_to_tactic.h" #include "library/tactic/apply_tactic.h" +#include "library/tactic/intros_tactic.h" namespace lean { static expr * g_exact_tac_fn = nullptr; @@ -80,6 +81,13 @@ public: m_name(n), m_fn(fn) {} name const & get_tatic_kind() const { return m_name; } expr_to_tactic_fn const & get_fn() const { return m_fn; } + virtual bool operator==(macro_definition_cell const & other) const { + if (tactic_macro_definition_cell const * other_ptr = dynamic_cast(&other)) { + return m_name == other_ptr->m_name; + } else { + return false; + } + } virtual name get_name() const { return get_tactic_name(); } virtual format pp(formatter const &) const { return format(m_name); } virtual void display(std::ostream & out) const { out << m_name; } @@ -138,6 +146,7 @@ bool is_tactic_macro(expr const & e) { static name * g_apply_tactic_name = nullptr; static name * g_rename_tactic_name = nullptr; +static name * g_intros_tactic_name = nullptr; expr mk_apply_tactic_macro(expr const & e) { return mk_tactic_macro(*g_apply_tactic_name, e); @@ -148,6 +157,14 @@ expr mk_rename_tactic_macro(name const & from, name const & to) { return mk_tactic_macro(*g_rename_tactic_name, 2, args); } +expr mk_intros_tactic_macro(buffer const & ns) { + buffer args; + for (name const & n : ns) { + args.push_back(Const(n)); + } + return mk_tactic_macro(*g_intros_tactic_name, args.size(), args.data()); +} + expr_to_tactic_fn const & get_tactic_macro_fn(expr const & e) { lean_assert(is_tactic_macro(e)); return static_cast(macro_def(e).raw())->get_fn(); @@ -220,7 +237,6 @@ static name_generator next_name_generator() { } tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) { - // std::cout << "expr_to_tactic: " << e << "\n"; flet let(g_unfold_tactic_macros, false); type_checker tc(env, next_name_generator()); return expr_to_tactic(tc, fn, e, p); @@ -315,6 +331,7 @@ void initialize_expr_to_tactic() { g_apply_tactic_name = new name(*g_tactic_name, "apply"); g_rename_tactic_name = new name(*g_tactic_name, "rename"); + g_intros_tactic_name = new name(*g_tactic_name, "intros"); name builtin_tac_name(*g_tactic_name, "builtin"); name exact_tac_name(*g_tactic_name, "exact"); @@ -380,7 +397,6 @@ void initialize_expr_to_tactic() { }); register_tacm(*g_apply_tactic_name, [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - // std::cout << "gen apply: " << e << "\n"; check_macro_args(e, 1, "invalid 'apply' tactic, it must have one argument"); return apply_tactic(fn, macro_arg(e, 0)); }); @@ -391,6 +407,17 @@ void initialize_expr_to_tactic() { throw expr_to_tactic_exception(e, "invalid 'rename' tactic, arguments must be identifiers"); return rename_tactic(const_name(macro_arg(e, 0)), const_name(macro_arg(e, 1))); }); + register_tacm(*g_intros_tactic_name, + [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { + buffer ns; + for (unsigned i = 0; i < macro_num_args(e); i++) { + expr const & arg = macro_arg(e, i); + if (!is_constant(arg)) + throw expr_to_tactic_exception(e, "invalid 'intros' tactic, arguments must be identifiers"); + ns.push_back(const_name(arg)); + } + return intros_tactic(to_list(ns.begin(), ns.end())); + }); register_tac(exact_tac_name, [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { // TODO(Leo): use elaborate_fn @@ -433,6 +460,7 @@ void finalize_expr_to_tactic() { delete g_exact_tac_fn; delete g_apply_tactic_name; delete g_rename_tactic_name; + delete g_intros_tactic_name; delete g_tactic_macros; delete g_map; delete g_tactic_name; diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index 683dc150d..f8bf97c2a 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/src/library/tactic/expr_to_tactic.h @@ -51,8 +51,10 @@ expr const & get_determ_tac_fn(); expr mk_tactic_macro(name const & kind, unsigned num_args, expr const * args); expr mk_tactic_macro(name const & kind, expr const & e); bool is_tactic_macro(expr const & e); + expr mk_apply_tactic_macro(expr const & e); expr mk_rename_tactic_macro(name const & from, name const & to); +expr mk_intros_tactic_macro(buffer const & ns); /** \brief Exception used to report a problem when an expression is being converted into a tactic. */ class expr_to_tactic_exception : public tactic_exception { diff --git a/src/library/tactic/intros_tactic.cpp b/src/library/tactic/intros_tactic.cpp new file mode 100644 index 000000000..bd0aa1f2f --- /dev/null +++ b/src/library/tactic/intros_tactic.cpp @@ -0,0 +1,76 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/instantiate.h" +#include "library/reducible.h" +#include "library/tactic/tactic.h" + +namespace lean { +/** \brief Return a "user" name that is not used by any local constant in the given goal */ +static name get_unused_name(goal const & g, name const & prefix, unsigned & idx) { + buffer locals; + get_app_rev_args(g.get_meta(), locals); + while (true) { + bool used = false; + name curr = prefix.append_after(idx); + idx++; + for (expr const & local : locals) { + if (is_local(local) && local_pp_name(local) == curr) { + used = true; + break; + } + } + if (!used) + return curr; + } +} + +tactic intros_tactic(list _ns, bool relax_main_opaque) { + auto fn = [=](environment const & env, io_state const &, proof_state const & s) { + list ns = _ns; + goals const & gs = s.get_goals(); + if (empty(gs)) + return optional(); + goal const & g = head(gs); + name_generator ngen = s.get_ngen(); + auto tc = mk_type_checker(env, ngen.mk_child(), relax_main_opaque); + expr t = g.get_type(); + expr m = g.get_meta(); + bool gen_names = empty(ns); + unsigned nidx = 1; + try { + while (true) { + if (!gen_names && is_nil(ns)) + break; + if (!is_pi(t)) { + if (!is_nil(ns)) { + t = tc->ensure_pi(t).first; + } else { + expr new_t = tc->whnf(t).first; + if (!is_pi(new_t)) + break; + } + } + name new_name; + if (!is_nil(ns)) { + new_name = head(ns); + ns = tail(ns); + } else { + new_name = get_unused_name(g, name("H"), nidx); + } + expr new_local = mk_local(ngen.next(), new_name, binding_domain(t), binding_info(t)); + t = instantiate(binding_body(t), new_local); + m = mk_app(m, new_local); + } + goal new_g(m, t); + return some(proof_state(s, goals(new_g, tail(gs)), ngen)); + } catch (exception &) { + return optional(); + } + }; + return tactic01(fn); +} +} diff --git a/src/library/tactic/intros_tactic.h b/src/library/tactic/intros_tactic.h new file mode 100644 index 000000000..8e549a2af --- /dev/null +++ b/src/library/tactic/intros_tactic.h @@ -0,0 +1,11 @@ +/* +Copyright (c) 2014 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 intros_tactic(list ns, bool relax_main_opaque = true); +} diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 6d8410b93..477a424a7 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -24,6 +24,8 @@ public: proof_state(goals const & gs, substitution const & s, name_generator const & ngen, constraints const & postponed); proof_state(proof_state const & s, goals const & gs, substitution const & subst): proof_state(gs, subst, s.m_ngen, s.m_postponed) {} + proof_state(proof_state const & s, goals const & gs, name_generator const & ngen): + proof_state(gs, s.m_subst, ngen, s.m_postponed) {} proof_state(proof_state const & s, goals const & gs): proof_state(s, gs, s.m_subst) {} proof_state(proof_state const & s, name_generator const & ngen): diff --git a/tests/lean/run/intros.lean b/tests/lean/run/intros.lean new file mode 100644 index 000000000..d4fa0a1b1 --- /dev/null +++ b/tests/lean/run/intros.lean @@ -0,0 +1,33 @@ +import logic tools.tactic +open tactic + +theorem tst1 (a b : Prop) : a → b → b := +by intros Ha; intros Hb; apply Hb + +theorem tst2 (a b : Prop) : a → b → a ∧ b := +by intros Ha; intros Hb; apply and.intro; apply Hb; apply Ha + +theorem tst3 (a b : Prop) : a → b → a ∧ b := +begin + intros Ha, + intros Hb, + apply and.intro, + apply Hb, + apply Ha +end + +theorem tst4 (a b : Prop) : a → b → a ∧ b := +begin + intros Ha Hb, + apply and.intro, + apply Hb, + apply Ha +end + +theorem tst5 (a b : Prop) : a → b → a ∧ b := +begin + intros, + apply and.intro, + eassumption, + eassumption +end