feat(library/blast): add "subst" action

src/library/blast/CMakeLists.txt

@@ -1,4 +1,4 @@
 add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp
   init_module.cpp simplifier.cpp simple_actions.cpp intros.cpp proof_expr.cpp
   options.cpp choice_point.cpp simple_strategy.cpp backward.cpp util.cpp
-  gexpr.cpp revert.cpp)
+  gexpr.cpp revert.cpp subst.cpp)

src/library/blast/intros.cpp

@@ -16,7 +16,7 @@ struct intros_proof_step_cell : public proof_step_cell {
     list<expr> m_new_hs;
     virtual ~intros_proof_step_cell() {}
     virtual action_result resolve(expr const & pr) const {
-        expr new_pr = mk_proof_lambda(curr_state(), m_new_hs, unfold_hypotheses_ge(curr_state(), pr));
+        expr new_pr = mk_proof_lambda(curr_state(), m_new_hs, pr);
         return action_result::solved(new_pr);
     }
 

src/library/blast/revert.cpp

@@ -23,7 +23,7 @@ struct revert_proof_step_cell : public proof_step_cell {
     virtual bool is_silent() const override { return true; }
 };
 
-unsigned revert(buffer<hypothesis_idx> & hidxs, hypothesis_idx_set & hidxs_set) {
+unsigned revert_action(buffer<hypothesis_idx> & hidxs, hypothesis_idx_set & hidxs_set) {
     lean_assert(hidxs.size() == hidxs_set.size());
     state & s = curr_state();
     unsigned hidxs_size = hidxs.size();
@@ -41,8 +41,8 @@ unsigned revert(buffer<hypothesis_idx> & hidxs, hypothesis_idx_set & hidxs_set)
     return hidxs.size();
 }
 
-unsigned revert(buffer<hypothesis_idx> & hidxs) {
+unsigned revert_action(buffer<hypothesis_idx> & hidxs) {
     hypothesis_idx_set hidxs_set(hidxs);
-    return revert(hidxs, hidxs_set);
+    return revert_action(hidxs, hidxs_set);
 }
 }}

src/library/blast/revert.h

@@ -11,5 +11,9 @@ namespace lean {
 namespace blast {
 /** \brief Revert the given hypotheses and their dependencies.
     Return the total number of hypotheses reverted. */
-unsigned revert(buffer<hypothesis_idx> & hidxs);
+unsigned revert_action(buffer<hypothesis_idx> & hidxs);
+
+/** \brief Lower-level version of previous procedure.
+    \pre hidxs and hidxs_set contain the same elements. */
+unsigned revert_action(buffer<hypothesis_idx> & hidxs, hypothesis_idx_set & hidxs_set);
 }}

src/library/blast/simple_strategy.cpp

@@ -8,7 +8,9 @@ Author: Leonardo de Moura
 #include "library/blast/options.h"
 #include "library/blast/choice_point.h"
 #include "library/blast/simple_actions.h"
+#include "library/blast/proof_expr.h"
 #include "library/blast/intros.h"
+#include "library/blast/subst.h"
 #include "library/blast/backward.h"
 
 namespace lean {
@@ -59,6 +61,9 @@ class simple_strategy {
                 display_action("assumption-contradiction");
                 return action_result::solved(*pr);
             }
+            if (subst_action(*hidx)) {
+                display_action("subst");
+            }
             return action_result::new_branch();
         }
 
@@ -84,7 +89,7 @@ class simple_strategy {
     action_result next_branch(expr pr) {
         while (curr_state().has_proof_steps()) {
             proof_step s     = curr_state().top_proof_step();
-            action_result r  = s.resolve(pr);
+            action_result r  = s.resolve(unfold_hypotheses_ge(curr_state(), pr));
             switch (r.get_kind()) {
             case action_result::Failed:
                 display_msg(">>> next-branch FAILED <<<");

src/library/blast/state.h

@@ -263,6 +263,10 @@ public:
 
     /** \brief Return the set of hypotheses that (directly) depend on the given one */
     hypothesis_idx_set get_forward_deps(hypothesis_idx hidx) const;
+    template<typename F>
+    void for_each_forward_dep(hypothesis_idx hidx, F && f) const {
+        get_forward_deps(hidx).for_each(f);
+    }
 
     /************************
        Abstracting hypotheses

src/library/blast/subst.cpp

@@ -0,0 +1,117 @@
+/*
+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/abstract.h"
+#include "kernel/instantiate.h"
+#include "library/blast/revert.h"
+#include "library/blast/intros.h"
+#include "library/blast/blast.h"
+
+namespace lean {
+namespace blast {
+struct subst_proof_step_cell : public proof_step_cell {
+    expr  m_target;
+    expr  m_eq_href;
+    expr  m_rhs;
+    bool  m_dep;
+    subst_proof_step_cell(expr const & t, expr const & e, expr const & r, bool d):
+        m_target(t), m_eq_href(e), m_rhs(r), m_dep(d) {}
+    virtual ~subst_proof_step_cell() {}
+
+    virtual action_result resolve(expr const & pr) const {
+        try {
+            state & s = curr_state();
+            app_builder & b = get_app_builder();
+            if (m_dep) {
+                buffer<expr> hs;
+                hs.push_back(m_rhs);
+                hs.push_back(m_eq_href);
+                expr motive = s.mk_lambda(hs, m_target);
+                return action_result::solved(b.mk_eq_drec(motive, pr, m_eq_href));
+            } else {
+                expr motive = s.mk_lambda(m_rhs, m_target);
+                return action_result::solved(b.mk_eq_rec(motive, pr, m_eq_href));
+            }
+        } catch (app_builder &) {
+            return action_result::failed();
+        }
+    }
+};
+
+bool subst_core(hypothesis_idx hidx) {
+    state & s       = curr_state();
+    state saved     = s;
+    app_builder & b = get_app_builder();
+    hypothesis const * h = s.get_hypothesis_decl(hidx);
+    lean_assert(h);
+    expr type = h->get_type();
+    expr lhs, rhs;
+    lean_verify(is_eq(type, lhs, rhs));
+    lean_assert(is_href(rhs));
+    try {
+        hypothesis_idx_buffer to_revert;
+        s.for_each_forward_dep(href_index(rhs),
+                               [&](hypothesis_idx d) {
+                                   if (d != hidx) to_revert.push_back(d);
+                               });
+        s.for_each_forward_dep(hidx,
+                               [&](hypothesis_idx d) { to_revert.push_back(d); });
+        unsigned num = revert_action(to_revert);
+        expr target  = s.get_target();
+        expr new_target = abstract(target, h->get_self());
+        bool dep        = !closed(new_target);
+        if (dep)
+            new_target = instantiate(new_target, b.mk_eq_refl(lhs));
+        new_target = instantiate(abstract(new_target, rhs), lhs);
+        s.push_proof_step(new subst_proof_step_cell(target, h->get_self(), rhs, dep));
+        s.set_target(new_target);
+        lean_verify(intros_action(num));
+        lean_verify(s.del_hypothesis(hidx));
+        lean_verify(s.del_hypothesis(href_index(rhs)));
+        return true;
+    } catch (app_builder_exception &) {
+        s = saved;
+        return false;
+    }
+}
+
+bool subst_action(hypothesis_idx hidx) {
+    state & s       = curr_state();
+    app_builder & b = get_app_builder();
+    hypothesis const * h = s.get_hypothesis_decl(hidx);
+    lean_assert(h);
+    expr type = h->get_type();
+    expr lhs, rhs;
+    if (!is_eq(type, lhs, rhs))
+        return false;
+    if (is_href(rhs)) {
+        return subst_core(hidx);
+    } else if (is_href(lhs)) {
+        if (!s.get_forward_deps(href_index(lhs)).empty()) {
+            // TODO(Leo): we don't handle this case yet.
+            // Other hypotheses depend on this equality.
+            return false;
+        }
+        state saved   = s;
+        try {
+            expr new_eq   = b.mk_eq(rhs, lhs);
+            expr new_pr   = b.mk_eq_symm(h->get_self());
+            expr new_href = s.mk_hypothesis(new_eq, new_pr);
+            if (subst_core(href_index(new_href))) {
+                return true;
+            } else {
+                s = saved;
+                return false;
+            }
+        } catch (app_builder_exception &) {
+            s = saved;
+            return false;
+        }
+    } else {
+        return false;
+    }
+}
+}}

src/library/blast/subst.h

@@ -0,0 +1,14 @@
+/*
+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/hypothesis.h"
+namespace lean {
+namespace blast {
+/** \brief If the given hypothesis is of the form (H : t = x) or (H : x = s), then
+    eliminate x (and H). Return true if success. */
+bool subst_action(hypothesis_idx hidx);
+}}