feat(library/blast): add simplify_target action

src/library/blast/CMakeLists.txt

@@ -1,4 +1,5 @@
 add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp
   init_module.cpp simplifier.cpp simple_actions.cpp intros_action.cpp proof_expr.cpp
   options.cpp choice_point.cpp simple_strategy.cpp backward_action.cpp util.cpp
-  gexpr.cpp revert_action.cpp subst_action.cpp no_confusion_action.cpp)
+  gexpr.cpp revert_action.cpp subst_action.cpp no_confusion_action.cpp
+  simplify_actions.cpp)

src/library/blast/action_result.h

@@ -29,7 +29,9 @@ public:
     static action_result failed() { return action_result(false); }
     static action_result new_branch() { return action_result(true); }
     static action_result solved(expr const & pr) { return action_result(pr); }
+    optional<expr> to_opt_expr() const { return m_kind == Solved ? some_expr(m_proof) : none_expr(); }
 };
 
 inline bool failed(action_result const & r) { return r.get_kind() == action_result::Failed; }
+inline bool solved(action_result const & r) { return r.get_kind() == action_result::Solved; }
 }}

src/library/blast/simple_strategy.cpp

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "library/blast/subst_action.h"
 #include "library/blast/backward_action.h"
 #include "library/blast/no_confusion_action.h"
+#include "library/blast/simplify_actions.h"
 
 namespace lean {
 namespace blast {
@@ -52,6 +53,45 @@ class simple_strategy {
         return curr_state().activate_hypothesis();
     }
 
+    /* \brief Preprocess state
+       It keeps applying intros, activating and finally simplify target.
+       Return an expression if the goal has been proved during preprocessing step. */
+    optional<expr> preprocess_core() {
+        display_msg("* Preprocess");
+        while (true) {
+            if (intros_action())
+                continue;
+            if (auto hidx = activate_hypothesis()) {
+                if (auto pr = assumption_contradiction_actions(*hidx)) {
+                    return pr;
+                }
+                if (subst_action(*hidx))
+                    continue;
+                action_result r = no_confusion_action(*hidx);
+                if (solved(r))
+                    return r.to_opt_expr();
+                continue;
+            }
+            break;
+        }
+        if (auto pr = assumption_action())
+            return pr;
+        return simplify_target_action().to_opt_expr();
+    }
+
+    optional<expr> preprocess() {
+        if (auto pr = preprocess_core()) {
+            auto r = next_branch(*pr);
+            if (!solved(r)) {
+                throw exception("invalid blast preprocessing action, preprocessing actions should not create branches");
+            } else {
+                return r.to_opt_expr();
+            }
+        } else {
+            return none_expr();
+        }
+    }
+
     action_result next_action() {
         if (intros_action()) {
             display_action("intros");
@@ -160,7 +200,12 @@ class simple_strategy {
     }
 
     optional<expr> search() {
+        clear_choice_points();
         curr_state().set_simp_rule_sets(get_simp_rule_sets(env()));
+        if (auto pr = preprocess())
+            return pr;
+        if (get_num_choice_points() > 0)
+            throw exception("invalid blast preprocessing action, preprocessing actions should not create choice points");
         state s    = curr_state();
         unsigned d = m_config.m_init_depth;
         while (true) {

src/library/blast/simplify_actions.cpp

@@ -0,0 +1,52 @@
+/*
+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/constants.h"
+#include "library/blast/simple_actions.h"
+#include "library/blast/blast.h"
+#include "library/blast/simplifier.h"
+
+namespace lean {
+namespace blast {
+static bool use_iff(expr const & target) {
+    return is_standard(env()) && is_prop(target);
+}
+
+class simplify_target_proof_step_cell : public proof_step_cell {
+    bool m_iff;
+    expr m_eq_pr;
+public:
+    simplify_target_proof_step_cell(bool iff, expr const & eq_pr):
+        m_iff(iff), m_eq_pr(eq_pr) {}
+
+    virtual ~simplify_target_proof_step_cell() {}
+
+    virtual action_result resolve(expr const & pr) const {
+        try {
+            app_builder & b = get_app_builder();
+            if (m_iff)
+                return action_result::solved(b.mk_app(get_iff_mpr_name(), m_eq_pr, pr));
+            else
+                return action_result::solved(b.mk_app(get_eq_mpr_name(), m_eq_pr, pr));
+        } catch (app_builder_exception &) {
+            return action_result::failed();
+        }
+    }
+};
+
+action_result simplify_target_action() {
+    state & s   = curr_state();
+    expr target = s.get_target();
+    bool iff    = use_iff(target);
+    name rname  = iff ? get_iff_name() : get_eq_name();
+    auto r = simplify(rname, target, s.get_simp_rule_sets());
+    if (r.is_none())
+        return action_result::failed(); // did nothing
+    s.push_proof_step(new simplify_target_proof_step_cell(iff, r.get_proof()));
+    s.set_target(r.get_new());
+    return action_result::new_branch();
+}
+}}

src/library/blast/simplify_actions.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 {
+optional<hypothesis_idx> simplify_hypothesis_action(hypothesis_idx hidx);
+bool add_simp_rule_action(hypothesis_idx hidx);
+action_result simplify_target_action();
+}}

tests/lean/run/blast11.lean

@@ -0,0 +1,12 @@
+import data.nat
+open algebra nat
+
+definition lemma1 (a b : nat) : a + b + 0 = b + a :=
+by blast
+
+print lemma1
+
+definition lemma2 (a b c : nat) : a + b + 0 + c + a + a + b = 0 + 0 + c + a + b + a + a + b :=
+by blast
+
+print lemma2