From b5db77961dc2297254aa8e0c447462882d309349 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 14 Nov 2015 15:02:14 -0800 Subject: [PATCH] feat(library/blast): add "trivial" action --- src/library/blast/blast.cpp | 12 ++++++++++++ src/library/blast/blast.h | 3 +++ src/library/blast/simple_actions.cpp | 25 +++++++++++++++++++++++++ src/library/blast/simple_actions.h | 2 ++ src/library/blast/simple_strategy.cpp | 5 +++++ tests/lean/run/blast10.lean | 14 ++++++++++++++ 6 files changed, 61 insertions(+) create mode 100644 tests/lean/run/blast10.lean diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index 20cfdbec0..8c8a97eb9 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "library/normalize.h" #include "library/class.h" #include "library/type_context.h" +#include "library/relation_manager.h" #include "library/congr_lemma_manager.h" #include "library/projection.h" #include "library/tactic/goal.h" @@ -47,6 +48,7 @@ class blastenv { name_predicate m_class_pred; name_predicate m_instance_pred; name_map m_projection_info; + is_relation_pred m_is_relation_pred; state m_curr_state; // current state tmp_type_context_pool m_tmp_ctx_pool; tmp_type_context_ptr m_tmp_ctx; // for app_builder and congr_lemma_manager @@ -402,6 +404,7 @@ public: m_not_reducible_pred(mk_not_reducible_pred(env)), m_class_pred(mk_class_pred(env)), m_instance_pred(mk_instance_pred(env)), + m_is_relation_pred(mk_is_relation_pred(env)), m_tmp_ctx(mk_tmp_type_context()), m_app_builder(*m_tmp_ctx), m_fun_info_manager(*m_tmp_ctx), @@ -506,6 +509,10 @@ public: m_norm_cache.insert(mk_pair(e, r)); return r; } + + bool is_relation(expr const & e, name & rop, expr & lhs, expr & rhs) { + return m_is_relation_pred(e, rop, lhs, rhs); + } }; LEAN_THREAD_PTR(blastenv, g_blastenv); @@ -551,6 +558,11 @@ projection_info const * get_projection_info(name const & n) { return g_blastenv->get_projection_info(n); } +bool is_relation(expr const & e, name & rop, expr & lhs, expr & rhs) { + lean_assert(g_blastenv); + return g_blastenv->is_relation(e, rop, lhs, rhs); +} + expr whnf(expr const & e) { lean_assert(g_blastenv); return g_blastenv->whnf(e); diff --git a/src/library/blast/blast.h b/src/library/blast/blast.h index e7040e4e9..d1a85b2e5 100644 --- a/src/library/blast/blast.h +++ b/src/library/blast/blast.h @@ -34,6 +34,9 @@ expr mk_fresh_local(expr const & type, binder_info const & bi = binder_info()); bool is_reducible(name const & n); /** \brief Return a nonnull projection_info object if \c n is the name of a projection in env() */ projection_info const * get_projection_info(name const & n); +/** \brief Return true iff \c e is a relation application, + and store the relation name, lhs and rhs in the output arguments. */ +bool is_relation(expr const & e, name & rop, expr & lhs, expr & rhs); /** \brief Put the given expression in weak-head-normal-form with respect to the current state being processed by the blast tactic. */ expr whnf(expr const & e); diff --git a/src/library/blast/simple_actions.cpp b/src/library/blast/simple_actions.cpp index 53c29ba58..e0367a523 100644 --- a/src/library/blast/simple_actions.cpp +++ b/src/library/blast/simple_actions.cpp @@ -55,4 +55,29 @@ optional assumption_contradiction_actions(hypothesis_idx hidx) { } return none_expr(); } + +optional trivial_action() { + try { + state s = curr_state(); + expr target = s.get_target(); + /* ignore if target contains meta-variables */ + if (has_expr_metavar(target)) + return none_expr(); + + /* true */ + if (target == mk_true()) { + return some_expr(mk_true_intro()); + } + + /* a ~ a */ + name rop; expr lhs, rhs; + if (is_relation(target, rop, lhs, rhs) && is_def_eq(lhs, rhs)) { + return some_expr(get_app_builder().mk_refl(rop, lhs)); + } + + return none_expr(); + } catch (app_builder_exception &) { + return none_expr(); + } +} }} diff --git a/src/library/blast/simple_actions.h b/src/library/blast/simple_actions.h index 3f9145728..b7368208c 100644 --- a/src/library/blast/simple_actions.h +++ b/src/library/blast/simple_actions.h @@ -12,4 +12,6 @@ optional assumption_action(); /** \brief Apply assumption and contradiction actions using the given hypothesis. \remark This action is supposed to be applied when a hypothesis is activated. */ optional assumption_contradiction_actions(hypothesis_idx hidx); +/** \brief Solve trivial targets (e.g., true, a = a, a <-> a, etc). */ +optional trivial_action(); }} diff --git a/src/library/blast/simple_strategy.cpp b/src/library/blast/simple_strategy.cpp index d01735fea..1860bee71 100644 --- a/src/library/blast/simple_strategy.cpp +++ b/src/library/blast/simple_strategy.cpp @@ -76,6 +76,11 @@ class simple_strategy { return action_result::new_branch(); } + if (auto pr = trivial_action()) { + display_action("trivial"); + return action_result::solved(*pr); + } + if (auto pr = assumption_action()) { // Remark: this action is only relevant // when the target has been modified. diff --git a/tests/lean/run/blast10.lean b/tests/lean/run/blast10.lean new file mode 100644 index 000000000..97fab2648 --- /dev/null +++ b/tests/lean/run/blast10.lean @@ -0,0 +1,14 @@ +import data.list + +set_option blast.trace true + +definition lemma1 : true := +by blast + +open perm + +definition lemma2 (l : list nat) : l ~ l := +by blast + +print lemma1 +print lemma2