From 60c637fb9d8f822977b6a61402882068d1351bd0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Jul 2014 18:32:44 -0700 Subject: [PATCH] feat(library/tactic): add 'exact' tactic Signed-off-by: Leonardo de Moura --- library/standard/tactic.lean | 1 + src/library/tactic/apply_tactic.cpp | 14 +---------- src/library/tactic/expr_to_tactic.cpp | 3 +++ src/library/tactic/tactic.cpp | 35 +++++++++++++++++++++++++++ src/library/tactic/tactic.h | 5 ++++ tests/lean/run/tactic12.lean | 16 ++++++++++++ 6 files changed, 61 insertions(+), 13 deletions(-) create mode 100644 tests/lean/run/tactic12.lean diff --git a/library/standard/tactic.lean b/library/standard/tactic.lean index 88d40df87..a0d264e13 100644 --- a/library/standard/tactic.lean +++ b/library/standard/tactic.lean @@ -27,6 +27,7 @@ definition id : tactic := tactic_value definition beta : tactic := tactic_value definition apply {B : Type} (b : B) : tactic := tactic_value definition unfold {B : Type} (b : B) : tactic := tactic_value +definition exact {B : Type} (b : B) : tactic := tactic_value definition trace (s : string) : tactic := tactic_value infixl `;`:200 := and_then infixl `|`:100 := or_else diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index cee52e379..f3b3bccff 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -60,18 +60,6 @@ void collect_simple_meta(expr const & e, buffer & metas) { }); } -/** \brief Throw an exception is \c v contains local constants, \c e is only used for position information. */ -void check_has_no_local(expr const & v, expr const & e) { - if (has_local(v)) { - for_each(v, [&](expr const & l, unsigned) { - if (is_local(l)) - throw tactic_exception(e, sstream() << "apply tactic contains reference to local '" << local_pp_name(l) - << "' which is not marked as [fact], so it is not visible to tactics"); - return has_local(l); - }); - } -} - tactic apply_tactic(expr const & _e) { return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { goals const & gs = s.get_goals(); @@ -100,7 +88,7 @@ tactic apply_tactic(expr const & _e) { type_checker tc(env, new_ngen.mk_child()); expr new_e = subst.instantiate(e); expr new_p = g.abstract(new_e); - check_has_no_local(new_p, _e); + check_has_no_local(new_p, _e, "apply"); substitution new_subst = subst.assign(g.get_name(), new_p); buffer metas; collect_simple_meta(new_e, metas); diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index e815f33cb..fce79abd1 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -110,6 +110,9 @@ static register_tac reg_trace(name(g_tac, "trace"), [](type_checker & tc, expr c static register_tac reg_apply(name(g_tac, "apply"), [](type_checker &, expr const & e, pos_info_provider const *) { return apply_tactic(app_arg(e)); }); +static register_tac reg_exact(name(g_tac, "exact"), [](type_checker &, expr const & e, pos_info_provider const *) { + return exact_tactic(app_arg(e)); + }); static register_tac reg_unfold(name(g_tac, "unfold"), [](type_checker &, expr const & e, pos_info_provider const *) { expr id = get_app_fn(app_arg(e)); if (!is_constant(id)) diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index f01098b9f..51c4290bd 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -13,12 +13,27 @@ Author: Leonardo de Moura #include "util/lazy_list_fn.h" #include "util/list_fn.h" #include "kernel/instantiate.h" +#include "kernel/type_checker.h" +#include "kernel/for_each_fn.h" #include "kernel/replace_visitor.h" #include "library/kernel_bindings.h" #include "library/tactic/tactic.h" #include "library/io_state_stream.h" namespace lean { +/** \brief Throw an exception is \c v contains local constants, \c e is only used for position information. */ +void check_has_no_local(expr const & v, expr const & e, char const * tac_name) { + if (has_local(v)) { + for_each(v, [&](expr const & l, unsigned) { + if (is_local(l)) + throw tactic_exception(e, sstream() << "tactic '" << tac_name << "' contains reference to local '" << local_pp_name(l) + << "' which is not visible by this tactic " + << "possible causes: it was not marked as [fact]; it was destructued"); + return has_local(l); + }); + } +} + tactic_exception::tactic_exception(expr const & e, char const * msg):exception(msg), m_expr(e) {} tactic_exception::tactic_exception(expr const & e, sstream const & strm):exception(strm), m_expr(e) {} @@ -205,6 +220,26 @@ tactic assumption_tactic() { }); } +tactic exact_tactic(expr const & _e) { + return tactic01([=](environment const & env, io_state const &, proof_state const & s) { + type_checker tc(env); + substitution subst = s.get_subst(); + goals const & gs = s.get_goals(); + goal const & g = head(gs); + expr e = subst.instantiate(_e); + expr e_t = subst.instantiate(tc.infer(e)); + expr t = subst.instantiate(g.get_type()); + if (tc.is_def_eq(e_t, t) && !tc.next_cnstr()) { + expr new_p = g.abstract(e); + check_has_no_local(new_p, _e, "exact"); + substitution new_subst = subst.assign(g.get_name(), new_p); + return some(proof_state(s, tail(gs), new_subst)); + } else { + return none_proof_state(); + } + }); +} + tactic beta_tactic() { return tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { bool reduced = false; diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index 789ac11d2..2fb52a192 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -14,6 +14,9 @@ Author: Leonardo de Moura #include "library/tactic/proof_state.h" namespace lean { +/** \brief Throw an exception is \c v contains local constants, \c e is only used for position information. */ +void check_has_no_local(expr const & v, expr const & e, char const * tac_name); + class tactic_exception : public exception { expr m_expr; public: @@ -132,6 +135,8 @@ inline tactic when(proof_state_pred p, tactic const & t) { return cond(p, t, id_ */ tactic focus(tactic const & t, unsigned i); inline tactic focus(tactic const & t) { return focus(t, 1); } +/** \brief Solve first goal iff it is definitionally equal to \c e */ +tactic exact_tactic(expr const & e); /** \brief Return a tactic that unfolds the definition named \c n. */ tactic unfold_tactic(name const & n); /** \brief Return a tactic that unfolds all (non-opaque) definitions. */ diff --git a/tests/lean/run/tactic12.lean b/tests/lean/run/tactic12.lean new file mode 100644 index 000000000..37db1fc8b --- /dev/null +++ b/tests/lean/run/tactic12.lean @@ -0,0 +1,16 @@ +import standard +using tactic + +theorem tst (a b : Bool) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b +:= by apply and_intro; + apply not_intro; + exact + (assume Ha, or_elim H + (assume Hna, absurd Ha Hna) + (assume Hnb, absurd Hb Hnb)); + assumption + + + + +