feat(library/blast/simplifier/simplifier_actions): add simplify_hypothesis_action

src/library/blast/recursor_action.cpp

@@ -42,8 +42,8 @@ optional<name> is_recursor_action_target(hypothesis_idx hidx) {
         return optional<name>();
     if (is_relation_app(type))
         return optional<name>(); // we don't apply recursors to equivalence relations: =, ~, <->, etc.
-    if (!h.is_assumption())
+    if (!h.is_assumption() && !is_prop(type))
-        return optional<name>(); // we only consider assumptions
+        return optional<name>(); // we only consider assumptions or propositions
     if (get_type_context().is_class(type)) {
         // we don't eliminate type classes instances
         // TODO(Leo): we may revise that in the future... some type classes instances may be worth eliminating (e.g., decidable).

src/library/blast/simple_strategy.cpp

@@ -34,6 +34,7 @@ class simple_strategy : public strategy {
         trace_action("activate");
 
         Try(assumption_contradiction_actions(*hidx));
+        Try(simplify_hypothesis_action(*hidx));
         TrySolve(assert_cc_action(*hidx));
         Try(subst_action(*hidx));
         Try(no_confusion_action(*hidx));

src/library/blast/simplifier/simplifier_actions.cpp

@@ -91,4 +91,34 @@ action_result simplify_target_action() {
     trace_action("simplify");
     return action_result::new_branch();
 }
+
+action_result simplify_hypothesis_action(hypothesis_idx hidx) {
+    if (!get_config().m_simp)
+        return action_result::failed();
+    state & s            = curr_state();
+    if (s.has_target_forward_deps(hidx)) {
+        // We currently do not try to simplify a hypothesis if other
+        // hypotheses or target depends on it.
+        return action_result::failed();
+    }
+    hypothesis const & h = s.get_hypothesis_decl(hidx);
+    if (!is_prop(h.get_type())) {
+        // We currently only simplify propositions.
+        return action_result::failed();
+    }
+    auto & ext           = get_extension();
+    auto r = simplify(get_iff_name(), h.get_type(), ext.get_simp_rule_sets());
+    if (r.get_new() == h.get_type())
+        return action_result::failed(); // did nothing
+    expr new_h_proof;
+    if (r.has_proof()) {
+        new_h_proof = get_app_builder().mk_app(get_iff_mp_name(), r.get_proof(), h.get_self());
+    } else {
+        // they are definitionally equal
+        new_h_proof = h.get_self();
+    }
+    s.mk_hypothesis(r.get_new(), new_h_proof);
+    s.del_hypothesis(hidx);
+    return action_result::new_branch();
+}
 }}

src/library/blast/simplifier/simplifier_actions.h

@@ -9,8 +9,7 @@ Author: Leonardo de Moura
 #include "library/blast/action_result.h"
 namespace lean {
 namespace blast {
-optional<hypothesis_idx> simplify_hypothesis_action(hypothesis_idx hidx);
+action_result simplify_hypothesis_action(hypothesis_idx hidx);
-bool add_simp_rule_action(hypothesis_idx hidx);
 action_result simplify_target_action();
 
 void initialize_simplifier_actions();

tests/lean/run/blast_simp1.lean

@@ -0,0 +1,17 @@
+example (a b c : Prop) : a ∧ b ∧ c ↔ c ∧ b ∧ a :=
+by blast
+
+example (a b c : Prop) : a ∧ false ∧ c ↔ false :=
+by blast
+
+example (a b c : Prop) : a ∨ false ∨ b ↔ b ∨ a :=
+by blast
+
+example (a b c : Prop) : ¬ true ∨ false ∨ b ↔ b :=
+by blast
+
+example (a b c : Prop) : if true then a else b ↔ if false then b else a :=
+by blast
+
+example (a b : Prop) : a ∧ not a ↔ false :=
+by blast

tests/lean/run/blast_simp2.lean

@@ -0,0 +1,6 @@
+set_option blast.recursor false
+
+definition tst1 (a b : Prop) : a ∧ b ∧ true → b ∧ a :=
+by blast
+
+print tst1