refactor(library/blast): avoid auxiliary local when creating hypothesis for intros

src/library/blast/assumption.cpp

@@ -18,6 +18,12 @@ optional<expr> assumption_action() {
         });
     if (!hidx)
         return none_expr();
-    return some_expr(s.get(*hidx)->get_value());
+    // TODO(Leo): cleanup
+    hypothesis const * h = s.get(*hidx);
+    if (h->get_value()) {
+        return some_expr(*h->get_value());
+    } else {
+        return some_expr(mk_href(*hidx));
+    }
 }
 }}

src/library/blast/blast.cpp

@@ -498,14 +498,14 @@ class blastenv {
         state &  m_state;
 
         virtual expr visit_local(expr const & e) {
+            // TODO(Leo): cleanup
             if (is_href(e)) {
                 hypothesis const * h = m_state.get(e);
-                lean_assert(h);
-                expr v = h->get_value();
-                return visit(v);
-            } else {
-                return replace_visitor::visit_local(e);
+                if (auto r = h->get_value()) {
+                    return visit(*r);
+                }
             }
+            return replace_visitor::visit_local(e);
         }
 
         virtual expr visit_meta(expr const & e) {

src/library/blast/hypothesis.h

@@ -28,7 +28,7 @@ class hypothesis {
     unsigned           m_dep_depth; // dependency depth
     hypothesis_idx_set m_deps;      // hypotheses used by the type and/or value of this hypothesis.
     expr               m_type;
-    expr               m_value;     // justification for this object.
+    optional<expr>     m_value;     // justification for this object.
     // Remark: if blast::is_local(m_value) is true, then the hypothesis is an assumption
 public:
     hypothesis():m_active(false), m_dep_depth(0) {}
@@ -37,9 +37,9 @@ public:
     unsigned get_dep_depth() const { return m_dep_depth; }
     hypothesis_idx_set const & get_backward_deps() const { return m_deps; }
     expr const & get_type() const { return m_type; }
-    expr const & get_value() const { return m_value; }
+    optional<expr> const & get_value() const { return m_value; }
     /** \brief Return true iff this hypothesis depends on \c h. */
     bool depends_on(expr const & h) const { return m_deps.contains(href_index(h)); }
-    bool is_assumption() const { return is_local_non_href(m_value); }
+    bool is_assumption() const { return !m_value || is_local_non_href(*m_value); }
 };
 }}

src/library/blast/intros.cpp

@@ -12,16 +12,13 @@ namespace lean {
 namespace blast {
 class intros_proof_step_cell : public proof_step_cell {
     list<expr> m_new_hs;
-    list<expr> m_new_locals;
 public:
-    intros_proof_step_cell(list<expr> const & new_hs, list<expr> const & new_locals):
-        m_new_hs(new_hs), m_new_locals(new_locals) {}
+    intros_proof_step_cell(list<expr> const & new_hs):
+        m_new_hs(new_hs) {}
     virtual ~intros_proof_step_cell() {}
 
     virtual optional<expr> resolve(state & s, expr const & pr) {
-        buffer<expr> locals;
-        to_buffer(m_new_locals, locals);
-        expr new_pr = Fun(locals, s.expand_hrefs(pr, m_new_hs));
+        expr new_pr = s.mk_lambda(m_new_hs, pr);
         return some_expr(new_pr);
     }
 };
@@ -32,15 +29,12 @@ bool intros_action() {
     if (!is_pi(target))
         return false;
     buffer<expr> new_hs;
-    buffer<expr> new_locals;
     while (is_pi(target)) {
-        expr local = mk_fresh_local(binding_domain(target));
-        expr href  = s.add_hypothesis(binding_name(target), binding_domain(target), local);
+        expr href  = s.add_hypothesis(binding_name(target), binding_domain(target));
         new_hs.push_back(href);
-        new_locals.push_back(local);
         target     = whnf(instantiate(binding_body(target), href));
     }
-    s.push_proof_step(proof_step(new intros_proof_step_cell(to_list(new_hs), to_list(new_locals))));
+    s.push_proof_step(proof_step(new intros_proof_step_cell(to_list(new_hs))));
     s.set_target(target);
     return true;
 }

src/library/blast/state.cpp

@@ -328,7 +328,7 @@ bool state::check_hypothesis(expr const & e, unsigned hidx, hypothesis const & h
 
 bool state::check_hypothesis(unsigned hidx, hypothesis const & h) const {
     lean_assert(check_hypothesis(h.get_type(), hidx, h));
-    lean_assert(h.is_assumption() || check_hypothesis(h.get_value(), hidx, h));
+    lean_assert(h.is_assumption() || check_hypothesis(*h.get_value(), hidx, h));
     return true;
 }
 
@@ -417,8 +417,8 @@ void state::add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user) {
 
 void state::add_deps(hypothesis & h_user, unsigned hidx_user) {
     add_deps(h_user.m_type, h_user, hidx_user);
-    if (!is_local_non_href(h_user.m_value)) {
-        add_deps(h_user.m_value, h_user, hidx_user);
+    if (!h_user.is_assumption()) {
+        add_deps(*h_user.m_value, h_user, hidx_user);
     }
 }
 
@@ -427,7 +427,7 @@ double state::compute_weight(unsigned hidx, expr const & /* type */) {
     return 1.0 / (static_cast<double>(hidx) + 1.0);
 }
 
-expr state::add_hypothesis(unsigned new_hidx, name const & n, expr const & type, expr const & value) {
+expr state::add_hypothesis(unsigned new_hidx, name const & n, expr const & type, optional<expr> const & value) {
     hypothesis new_h;
     new_h.m_name          = n;
     new_h.m_type          = type;
@@ -442,12 +442,21 @@ expr state::add_hypothesis(unsigned new_hidx, name const & n, expr const & type,
 }
 
 expr state::add_hypothesis(name const & n, expr const & type, expr const & value) {
-    return add_hypothesis(mk_href_idx(), n, type, value);
+    return add_hypothesis(mk_href_idx(), n, type, some_expr(value));
 }
 
 expr state::add_hypothesis(expr const & type, expr const & value) {
     unsigned hidx = mk_href_idx();
-    return add_hypothesis(hidx, name(*g_prefix, hidx), type, value);
+    return add_hypothesis(hidx, name(*g_prefix, hidx), type, some_expr(value));
+}
+
+expr state::add_hypothesis(name const & n, expr const & type) {
+    return add_hypothesis(mk_href_idx(), n, type, none_expr());
+}
+
+expr state::add_hypothesis(expr const & type) {
+    unsigned hidx = mk_href_idx();
+    return add_hypothesis(hidx, name(*g_prefix, hidx), type, none_expr());
 }
 
 void state::update_indices(unsigned /* hidx */) {
@@ -503,10 +512,12 @@ struct expand_hrefs_fn : public replace_visitor {
 
     virtual expr visit_local(expr const & e) {
         if (is_href(e) && std::find(m_hrefs.begin(), m_hrefs.end(), e) != m_hrefs.end()) {
-            return visit(m_state.get(e)->get_value());
-        } else {
-            return replace_visitor::visit_local(e);
+            hypothesis const * h = m_state.get(e);
+            if (h->get_value()) {
+                return visit(*h->get_value());
+            }
         }
+        return replace_visitor::visit_local(e);
     }
 };
 

src/library/blast/state.h

@@ -126,8 +126,7 @@ class state {
         We will update indices and data-structures (e.g., congruence closure). */
     void update_indices(unsigned hidx);
 
-    expr add_hypothesis(unsigned new_hidx, name const & n, expr const & type, expr const & value);
-
+    expr add_hypothesis(unsigned new_hidx, name const & n, expr const & type, optional<expr> const & value);
 
     void add_fixed_by(unsigned hidx, unsigned midx);
     unsigned add_metavar_decl(metavar_decl const & decl);
@@ -202,6 +201,8 @@ public:
 
     expr add_hypothesis(name const & n, expr const & type, expr const & value);
     expr add_hypothesis(expr const & type, expr const & value);
+    expr add_hypothesis(name const & n, expr const & type);
+    expr add_hypothesis(expr const & type);
 
     /** \brief Return true iff the hypothesis with index \c hidx_user depends on the hypothesis with index
         \c hidx_provider. */
@@ -283,7 +284,7 @@ public:
     unsigned get_depth() const { return m_depth; }
 
     expr mk_lambda(unsigned num, expr const * hrefs, expr const & b) const {
-        return mk_binding(false, num, hrefs, b);
+        return mk_binding(true, num, hrefs, b);
     }
     expr mk_pi(unsigned num, expr const * hrefs, expr const & b) const {
         return mk_binding(false, num, hrefs, b);

tests/lean/run/blast2.lean

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