From 4cf5c77575a63e4b89b884046d938269b98bb779 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 31 Dec 2015 12:35:16 -0800 Subject: [PATCH] feat(library/blast/strategies): add strategy for applying recursors --- src/library/blast/strategies/CMakeLists.txt | 2 +- src/library/blast/strategies/portfolio.cpp | 7 + src/library/blast/strategies/rec_strategy.cpp | 165 ++++++++++++++++++ src/library/blast/strategies/rec_strategy.h | 49 ++++++ 4 files changed, 222 insertions(+), 1 deletion(-) create mode 100644 src/library/blast/strategies/rec_strategy.cpp create mode 100644 src/library/blast/strategies/rec_strategy.h diff --git a/src/library/blast/strategies/CMakeLists.txt b/src/library/blast/strategies/CMakeLists.txt index a13c876da..f608f18de 100644 --- a/src/library/blast/strategies/CMakeLists.txt +++ b/src/library/blast/strategies/CMakeLists.txt @@ -1,2 +1,2 @@ add_library(blast_strategies OBJECT simple_strategy.cpp iterative_deepening.cpp - preprocess_strategy.cpp action_strategy.cpp portfolio.cpp) + preprocess_strategy.cpp action_strategy.cpp rec_strategy.cpp portfolio.cpp) diff --git a/src/library/blast/strategies/portfolio.cpp b/src/library/blast/strategies/portfolio.cpp index e44adc7c7..e4c47118c 100644 --- a/src/library/blast/strategies/portfolio.cpp +++ b/src/library/blast/strategies/portfolio.cpp @@ -16,6 +16,7 @@ Author: Leonardo de Moura #include "library/blast/strategies/simple_strategy.h" #include "library/blast/strategies/preprocess_strategy.h" #include "library/blast/strategies/action_strategy.h" +#include "library/blast/strategies/rec_strategy.h" namespace lean { namespace blast { @@ -58,6 +59,10 @@ static optional apply_ematch_simp() { ematch_simp_action)(); } +static optional apply_ematch_simp_rec() { + return rec_and_then(apply_ematch_simp)(); +} + static optional apply_constructor() { return mk_action_strategy("constructor", []() { return constructor_action(); })(); @@ -105,6 +110,8 @@ optional apply_strategy() { return apply_ematch(); } else if (s_name == "ematch_simp") { return apply_ematch_simp(); + } else if (s_name == "ematch_simp_rec") { + return apply_ematch_simp_rec(); } else if (s_name == "constructor") { return apply_constructor(); } else if (s_name == "unit") { diff --git a/src/library/blast/strategies/rec_strategy.cpp b/src/library/blast/strategies/rec_strategy.cpp new file mode 100644 index 000000000..54e84dc7c --- /dev/null +++ b/src/library/blast/strategies/rec_strategy.cpp @@ -0,0 +1,165 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/inductive/inductive.h" +#include "library/user_recursors.h" +#include "library/blast/blast.h" +#include "library/blast/trace.h" +#include "library/blast/choice_point.h" +#include "library/blast/actions/intros_action.h" +#include "library/blast/actions/recursor_action.h" +#include "library/blast/strategies/rec_strategy.h" + +namespace lean { +namespace blast { +static action_result try_hypothesis(hypothesis_idx hidx) { + state & s = curr_state(); + hypothesis const & h = s.get_hypothesis_decl(hidx); + expr const & type = h.get_type(); + expr const & I = get_app_fn(type); + lean_assert(is_constant(I)); + name const & I_name = const_name(I); + if (inductive::is_inductive_decl(env(), I_name)) { + return recursor_action(hidx, inductive::get_elim_name(I_name)); + } + list Rs = get_recursors_for(env(), const_name(I)); + if (Rs) { + return recursor_action(hidx, head(Rs)); + } + return action_result::failed(); +} + +class rec_choice_point_cell : public choice_point_cell { + state m_state; + list m_hs; + unsigned m_choice_idx; +public: + rec_choice_point_cell(state const & s, list const & hs, unsigned choice_idx): + m_state(s), m_hs(hs), m_choice_idx(choice_idx) {} + + virtual action_result next() { + while (!empty(m_hs)) { + curr_state() = m_state; + hypothesis_idx hidx = head(m_hs); + m_hs = tail(m_hs); + action_result r = try_hypothesis(hidx); + if (!failed(r)) { + lean_trace_search(tout() << "next of choice #" << m_choice_idx + << ", recurse " << ppb(mk_href(hidx)) << "\n";); + return r; + } + } + return action_result::failed(); + } +}; + +action_result rec_action(rec_candidate_selector const & selector) { + hypothesis_idx_buffer hidxs; + selector(hidxs); + if (hidxs.empty()) + return action_result::failed(); + if (hidxs.size() == 1) + return try_hypothesis(hidxs[0]); + state s = curr_state(); + list hidx_list = to_list(hidxs); + while (!empty(hidx_list)) { + hypothesis_idx hidx = head(hidx_list); + action_result r = try_hypothesis(hidx); + hidx_list = tail(hidx_list); + if (!failed(r)) { + if (!empty(hidx_list)) { + // create choice point + unsigned cidx = mk_choice_point_idx(); + push_choice_point(choice_point(new rec_choice_point_cell(s, hidx_list, cidx))); + lean_trace_search(tout() << "recurse " << ppb(mk_href(hidx)) << " (choice #" << cidx << ")\n";); + } else { + lean_trace_search(tout() << "recurse " << ppb(mk_href(hidx)) << "\n";); + } + return r; + } + curr_state() = s; + } + return action_result::failed(); +} + +class rec_strategy_fn : public strategy_fn { + strategy m_S; + rec_candidate_selector m_selector; + unsigned m_init_depth; + unsigned m_max_depth; + + virtual bool show_failure() const override { return false; } + virtual char const * get_name() const override { return "recursor"; } + + virtual action_result hypothesis_pre_activation(hypothesis_idx) override { + return action_result::new_branch(); + } + + virtual action_result hypothesis_post_activation(hypothesis_idx) override { + return action_result::new_branch(); + } + + virtual action_result next_action() override { + if (curr_state().get_proof_depth() < m_max_depth) { + Try(intros_action()); + Try(activate_hypothesis()); + Try(rec_action(m_selector)); + } + if (optional pf = m_S()) { + return action_result::solved(*pf); + } + return action_result::failed(); + } + +public: + rec_strategy_fn(strategy const & S, rec_candidate_selector const & sel): + m_S(S), m_selector(sel), m_init_depth(curr_state().get_proof_depth()), + // TODO(Leo): use iterative deepening + // TODO(Leo): add option: max number of rounds (aka max depth) + // TODO(Leo): add option: max number of steps + m_max_depth(m_init_depth + 1) {} +}; + +strategy rec_and_then(strategy const & S, rec_candidate_selector const & selector) { + return [=]() { return rec_strategy_fn(S, selector)(); }; // NOLINT +} + +static void default_selector(hypothesis_idx_buffer & r) { + // TODO(Leo): add options to control selection + state & s = curr_state(); + s.for_each_hypothesis([&](hypothesis_idx hidx, hypothesis const & h) { + expr const & type = h.get_type(); + if (!is_app(type) && !is_constant(type)) + return; + if (!h.is_assumption() && !is_prop(type)) + return; + if (is_relation_app(type)) + return; // we don't apply recursors to equivalence relations: =, ~, <->, etc. + if (get_type_context().is_class(type)) + return; // ignore type classes + expr const & I = get_app_fn(type); + if (!is_constant(I)) + return; + name const & I_name = const_name(I); + if (inductive::is_inductive_decl(env(), I_name) && *inductive::get_num_intro_rules(env(), I_name) > 1) { + // builtin recursive datatype with more than one constructor + r.push_back(hidx); + return; + } + list Rs = get_recursors_for(env(), I_name); + if (Rs) { + // has user defined recursor + r.push_back(hidx); + return; + } + }); + s.sort_hypotheses(r); +} + +strategy rec_and_then(strategy const & S) { + return rec_and_then(S, default_selector); +} +}} diff --git a/src/library/blast/strategies/rec_strategy.h b/src/library/blast/strategies/rec_strategy.h new file mode 100644 index 000000000..ed8c403a5 --- /dev/null +++ b/src/library/blast/strategies/rec_strategy.h @@ -0,0 +1,49 @@ +/* +Copyright (c) 2015 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/blast/strategy.h" + +namespace lean { +namespace blast { +/* +Auxiliary strategy for applying recursors automatically. +The idea is to simulate the case-analysis used in many theorems +in the standard library. + +Example: + +theorem last_concat [simp] {x : T} : ∀ {l : list T} (h : concat x l ≠ []), last (concat x l) h = x +| [] h := rfl +| [a] h := rfl +| (a₁::a₂::l) h := + begin + change last (a₁::a₂::concat x l) !cons_ne_nil = x, + rewrite last_cons_cons, + change last (concat x (a₂::l)) !concat_ne_nil = x, + apply last_concat + end + + +Options: +1) ignore non-recursive (true) +2) ignore type classes (true) +3) ignore structures (true) +4) maximum number of rounds 3 + +Each is an iterative deepening procedure. +*/ + +/* Procedure for retrieving hypotheses from the current state. + The rec_and_then strategy will apply the recursor action on the candidates. + Actually, it creates a choice point for trying each candidate. */ +typedef std::function rec_candidate_selector; + +strategy rec_and_then(strategy const & S, rec_candidate_selector const & selector); + +/* Use default selector */ +strategy rec_and_then(strategy const & S); +}}