feat(library/blast/strategies): add strategy for applying recursors

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)

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<expr> apply_ematch_simp() {
                               ematch_simp_action)();
 }
 
+static optional<expr> apply_ematch_simp_rec() {
+    return rec_and_then(apply_ematch_simp)();
+}
+
 static optional<expr> apply_constructor() {
     return mk_action_strategy("constructor",
                               []() { return constructor_action(); })();
@@ -105,6 +110,8 @@ optional<expr> 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") {

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<name> 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<hypothesis_idx> m_hs;
+    unsigned             m_choice_idx;
+public:
+    rec_choice_point_cell(state const & s, list<hypothesis_idx> 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<hypothesis_idx> 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<expr> 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<name> 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);
+}
+}}

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<void(hypothesis_idx_buffer &)> 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);
+}}