From 29d472788faddac7e0581a4d4e95a2fa0ded5ee7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 13 Nov 2015 16:26:28 -0800
Subject: [PATCH] feat(library/blast/subst): avoid unnecessary proof step

---
 src/library/blast/hypothesis.h |  2 ++
 src/library/blast/subst.cpp    | 18 +++++++++++++-----
 tests/lean/run/blast7.lean     |  7 +++++++
 3 files changed, 22 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/blast7.lean

diff --git a/src/library/blast/hypothesis.h b/src/library/blast/hypothesis.h
index 03867390d..336569c84 100644
--- a/src/library/blast/hypothesis.h
+++ b/src/library/blast/hypothesis.h
@@ -65,6 +65,8 @@ public:
             m_buffer.push_back(h);
         }
     }
+    unsigned size() const { return m_buffer.size(); }
+    bool empty() const { return m_buffer.empty(); }
     hypothesis_idx_buffer const & as_buffer() const {
         return m_buffer;
     }
diff --git a/src/library/blast/subst.cpp b/src/library/blast/subst.cpp
index f829f8b14..c7b794466 100644
--- a/src/library/blast/subst.cpp
+++ b/src/library/blast/subst.cpp
@@ -61,12 +61,20 @@ bool subst_core(hypothesis_idx hidx) {
         expr target  = s.get_target();
         expr new_target = abstract(target, h->get_self());
         bool dep        = !closed(new_target);
-        if (dep)
+        bool skip       = to_revert.empty();
+        if (dep) {
+            skip       = false;
             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));
+        }
+        new_target = abstract(new_target, rhs);
+        if (!closed(new_target))
+            skip       = false;
+        if (!skip) {
+            new_target = instantiate(new_target, 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;
diff --git a/tests/lean/run/blast7.lean b/tests/lean/run/blast7.lean
new file mode 100644
index 000000000..c39193387
--- /dev/null
+++ b/tests/lean/run/blast7.lean
@@ -0,0 +1,7 @@
+set_option blast.init_depth 10
+
+lemma lemma1 (p : Prop) (a b : nat) : a = b → p → p :=
+by blast
+
+reveal lemma1
+print lemma1