feat(library/blast): add strategies "grind" and "core_grind"

library/init/logic.lean

@@ -243,6 +243,7 @@ notation a ∧ b  := and a b
 variables {a b c d : Prop}
 
 attribute and.rec [elim]
+attribute and.intro [intro]
 
 theorem and.elim (H₁ : a ∧ b) (H₂ : a → b → c) : c :=
 and.rec H₂ H₁

src/library/blast/grinder/grinder_actions.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "library/blast/blast.h"
+#include "library/blast/trace.h"
 #include "library/blast/actions/recursor_action.h"
 #include "library/blast/backward/backward_action.h"
 #include "library/blast/grinder/intro_elim_lemmas.h"
@@ -18,7 +19,9 @@ struct grinder_branch_extension : public branch_extension {
     name_map<name>  m_elim_lemmas;
 
     grinder_branch_extension() {}
-    grinder_branch_extension(grinder_branch_extension const &) {}
+    grinder_branch_extension(grinder_branch_extension const & e):
+        m_intro_lemmas(e.m_intro_lemmas),
+        m_elim_lemmas(e.m_elim_lemmas) {}
     virtual ~grinder_branch_extension() {}
     virtual branch_extension * clone() override { return new grinder_branch_extension(*this); }
     virtual void initialized() override {

src/library/blast/grinder/grinder_strategy.cpp

@@ -42,9 +42,16 @@ action_result grinder_strategy_core_fn::next_action() {
 }
 
 strategy grind_and_then(strategy const & S) {
-    return [=]() { return grinder_strategy_fn([](hypothesis_idx) { return action_result::failed(); },       // NOLINT
+    return [=]() { // NOLINT
-                                              [](hypothesis_idx) { return action_result::failed(); },       // NOLINT
+        curr_state().deactivate_all();
-                                              [=]() { TryStrategy(S); return action_result::failed(); })(); // NOLINT
+        return grinder_strategy_fn([](hypothesis_idx) { return action_result::failed(); }, // NOLINT
+                                   [](hypothesis_idx) { return action_result::failed(); }, // NOLINT
+                                   [=]() { // NOLINT
+                                       if (optional<expr> pf = S()) {
+                                           return action_result::solved(*pf);
+                                       }
+                                       return action_result::failed();
+                                   })();
     };
 }
 }}

src/library/blast/grinder/grinder_strategy.h

@@ -37,5 +37,5 @@ public:
         m_pre(pre), m_post(post), m_next(next) {}
 };
 
-strategy grind_and_then(strategy & S);
+strategy grind_and_then(strategy const & S);
 }}

src/library/blast/state.cpp

@@ -595,6 +595,11 @@ double state::compute_weight(unsigned hidx, expr const & /* type */) {
     return 1.0 / (static_cast<double>(hidx) + 1.0);
 }
 
+void state::add_todo_queue(hypothesis_idx hidx) {
+    double w = compute_weight(hidx, get_hypothesis_decl(hidx).get_type());
+    m_branch.m_todo_queue.insert(w, hidx);
+}
+
 expr state::mk_hypothesis(unsigned new_hidx, name const & n, expr const & type, optional<expr> const & value) {
     hypothesis new_h;
     expr r                = mk_href(new_hidx);
@@ -607,8 +612,7 @@ expr state::mk_hypothesis(unsigned new_hidx, name const & n, expr const & type,
     m_branch.m_hyp_decls.insert(new_hidx, new_h);
     if (new_h.is_assumption())
         m_branch.m_assumption.insert(new_hidx);
-    double w = compute_weight(new_hidx, type);
+    add_todo_queue(new_hidx);
-    m_branch.m_todo_queue.insert(w, new_hidx);
     return r;
 }
 
@@ -780,6 +784,21 @@ branch_extension & state::get_extension(unsigned extid) {
     }
 }
 
+void state::deactivate_all() {
+    m_branch.m_head_to_hyps = head_map<hypothesis_idx>();
+    unsigned n = get_extension_manager().get_num_extensions();
+    for (unsigned i = 0; i < n; i++) {
+        if (m_branch.m_extensions[i]) {
+            m_branch.m_extensions[i]->dec_ref();
+            m_branch.m_extensions[i] = nullptr;
+        }
+    }
+    m_branch.m_active.for_each([&](hypothesis_idx hidx) {
+            add_todo_queue(hidx);
+        });
+    m_branch.m_active = hypothesis_idx_set();
+}
+
 void state::update_indices(hypothesis_idx hidx) {
     hypothesis const & h = get_hypothesis_decl(hidx);
     /* update m_head_to_hyps */

src/library/blast/state.h

@@ -183,6 +183,8 @@ class state {
     void add_deps(hypothesis & h_user, hypothesis_idx hidx_user);
     void del_forward_dep(unsigned hidx_user, unsigned hidx_provider);
 
+    void add_todo_queue(hypothesis_idx hidx);
+
     expr mk_hypothesis(hypothesis_idx new_hidx, name const & n, expr const & type, optional<expr> const & value);
 
     unsigned add_metavar_decl(metavar_decl const & decl);
@@ -297,6 +299,9 @@ public:
     optional<hypothesis_idx> select_hypothesis_to_activate();
     void activate_hypothesis(hypothesis_idx hidx);
 
+    /** \brief Deactivate all active hypotheses */
+    void deactivate_all();
+
     /** \brief Store in \c r the hypotheses in this branch sorted by dependency depth */
     void get_sorted_hypotheses(hypothesis_idx_buffer & r) const;
     /** \brief Sort hypotheses in r */

src/library/blast/strategies/portfolio.cpp

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "library/blast/forward/ematch.h"
 #include "library/blast/backward/backward_action.h"
 #include "library/blast/backward/backward_strategy.h"
+#include "library/blast/grinder/grinder_strategy.h"
 #include "library/blast/strategies/simple_strategy.h"
 #include "library/blast/strategies/preprocess_strategy.h"
 #include "library/blast/strategies/debug_action_strategy.h"
@@ -62,6 +63,14 @@ static optional<expr> apply_unit() {
                                     []() { return action_result::failed(); })();
 }
 
+static optional<expr> apply_grind() {
+    return preprocess_and_then(grind_and_then([]() { return none_expr(); }))();
+}
+
+static optional<expr> apply_core_grind() {
+    return grind_and_then([]() { return none_expr(); })();
+}
+
 optional<expr> apply_strategy() {
     std::string s_name(get_config().m_strategy);
     if (s_name == "preprocess") {
@@ -77,6 +86,10 @@ optional<expr> apply_strategy() {
         return apply_simple();
     } else if (s_name == "cc") {
         return apply_cc();
+    } else if (s_name == "grind") {
+        return apply_grind();
+    } else if (s_name == "core_grind") {
+        return apply_core_grind();
     } else if (s_name == "ematch") {
         return apply_ematch();
     } else if (s_name == "constructor") {

tests/lean/run/blast_grind1.lean

@@ -0,0 +1,33 @@
+set_option blast.strategy "core_grind"
+
+example (a b c : nat) : a = b ∨ a = c → b = c → b = a :=
+by blast
+
+example (f : nat → nat) (a b c : nat) : f a = f b ∨ f a = f c → f b = f c → f b = f a :=
+by blast
+
+definition ex1 (a : nat) : a = 0 → (λ x, x + a) = (λ x, x + 0) :=
+by blast
+
+print ex1
+
+attribute Exists.intro [intro]
+
+example (p q : nat → Prop) : (∃ x, p x ∧ q x) → (∃ x, q x) ∧ (∃ x, p x) :=
+by blast
+
+set_option blast.strategy "grind"
+
+example (a b c : nat) : a = b ∨ a = c → b = c → b = a :=
+by blast
+
+example (f : nat → nat) (a b c : nat) : f a = f b ∨ f a = f c → f b = f c → f b = f a :=
+by blast
+
+example (a : nat) : a = 0 → (λ x, x + a) = (λ x, x + 0) :=
+by blast
+
+attribute Exists.intro [intro]
+
+example (p q : nat → Prop) : (∃ x, p x ∧ q x) → (∃ x, q x) ∧ (∃ x, p x) :=
+by blast