feat(library/blast): add basic assumption action

src/library/blast/CMakeLists.txt

@@ -1,2 +1,2 @@
 add_library(blast OBJECT expr.cpp branch.cpp state.cpp blast.cpp
-  blast_tactic.cpp init_module.cpp simplifier.cpp)
+  blast_tactic.cpp init_module.cpp simplifier.cpp assumption.cpp)

src/library/blast/assumption.cpp

@@ -0,0 +1,23 @@
+/*
+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 "library/blast/blast.h"
+
+namespace lean {
+namespace blast {
+optional<expr> assumption_action() {
+    // TODO(Leo): this is a very naive implementation that just traverses the set of
+    // active hypothesis
+    branch const & b    = main_branch();
+    expr const & target = b.get_target();
+    auto hidx = b.find_active_hypothesis([&](unsigned, hypothesis const & h) {
+            return is_def_eq(h.get_type(), target);
+        });
+    if (!hidx)
+        return none_expr();
+    return some_expr(b.get(*hidx)->get_value());
+}
+}}

src/library/blast/assumption.h

@@ -0,0 +1,12 @@
+/*
+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 "kernel/expr.h"
+namespace lean {
+namespace blast {
+optional<expr> assumption_action();
+}}

src/library/blast/blast.cpp

@@ -21,6 +21,7 @@ Author: Leonardo de Moura
 #include "library/blast/expr.h"
 #include "library/blast/state.h"
 #include "library/blast/blast.h"
+#include "library/blast/assumption.h"
 #include "library/blast/blast_exception.h"
 
 #ifndef LEAN_DEFAULT_BLAST_MAX_DEPTH
@@ -434,6 +435,8 @@ class blastenv {
         if (activate_hypothesis()) {
             // TODO(Leo): we should probably eagerly simplify the activated hypothesis.
             return mk_pair(Continue, expr());
+        } else if (auto pr = assumption_action()) {
+            return mk_pair(ClosedBranch, *pr);
         } else {
             // TODO(Leo): add more actions...
             return mk_pair(NoAction, expr());

src/library/blast/branch.h

@@ -21,7 +21,7 @@ class branch {
     typedef hypothesis_idx_map<hypothesis_idx_set> forward_deps;
     typedef rb_map<double, unsigned, double_cmp>   todo_queue;
     friend class state;
-    unsigned           m_next;
+    unsigned           m_next{0};
     context            m_context;
     // We break the set of hypotheses in m_context in 3 sets that are not necessarily disjoint:
     //   - assumption
@@ -60,7 +60,7 @@ class branch {
     void update_indices(unsigned hidx);
 
 public:
-    branch():m_next(0) {}
+    branch() {}
 
     expr add_hypothesis(name const & n, expr const & type, expr const & value);
     expr add_hypothesis(expr const & type, expr const & value);
@@ -75,6 +75,12 @@ public:
         return get(href_index(h));
     }
     void for_each_hypothesis(std::function<void(unsigned, hypothesis const &)> const & fn) const { m_context.for_each(fn); }
+    optional<unsigned> find_active_hypothesis(std::function<bool(unsigned, hypothesis const &)> const & fn) const { // NOLINT
+        return m_active.find_if([&](unsigned hidx) {
+                return fn(hidx, *get(hidx));
+            });
+    }
+
     /** \brief Activate the next hypothesis in the TODO queue, return none if the TODO queue is empty. */
     optional<unsigned> activate_hypothesis();
 

tests/lean/run/blast1.lean

@@ -0,0 +1,2 @@
+example (a b : Prop) (Ha : a) (Hb : b) : a :=
+by blast