feat(library/blast/strategies): add "ematch" strategy for testing ematching

src/library/blast/strategies/debug_action_strategy.cpp

@@ -61,6 +61,21 @@ public:
         m_action(a) {}
 };
 
+class xdebug_action_strategy_fn : public debug_action_strategy_core_fn {
+    std::function<action_result(hypothesis_idx)> m_pre;
+    std::function<action_result(hypothesis_idx)> m_post;
+    std::function<action_result()>               m_next;
+
+    virtual action_result pre(hypothesis_idx hidx) { return m_pre(hidx); }
+    virtual action_result post(hypothesis_idx hidx) { return m_post(hidx); }
+    virtual action_result next() { return m_next(); }
+public:
+    xdebug_action_strategy_fn(std::function<action_result(hypothesis_idx)> const & pre,
+                              std::function<action_result(hypothesis_idx)> const & post,
+                              std::function<action_result()> const & next):
+        m_pre(pre), m_post(post), m_next(next) {}
+};
+
 strategy mk_debug_action_strategy(std::function<action_result()> const & a) {
     return [=]() { return debug_action_strategy_fn(a)(); }; // NOLINT
 }
@@ -72,4 +87,10 @@ strategy mk_debug_pre_action_strategy(std::function<action_result(hypothesis_idx
 strategy mk_debug_post_action_strategy(std::function<action_result(hypothesis_idx)> const & a) {
     return [=]() { return debug_post_action_strategy_fn(a)(); }; // NOLINT
 }
+
+strategy mk_debug_action_strategy(std::function<action_result(hypothesis_idx)> const & pre,
+                                  std::function<action_result(hypothesis_idx)> const & post,
+                                  std::function<action_result()> const & next) {
+    return [=]() { return xdebug_action_strategy_fn(pre, post, next)(); }; // NOLINT
+}
 }}

src/library/blast/strategies/debug_action_strategy.h

@@ -13,4 +13,7 @@ namespace blast {
 strategy mk_debug_action_strategy(std::function<action_result()> const & a);
 strategy mk_debug_pre_action_strategy(std::function<action_result(hypothesis_idx)> const & a);
 strategy mk_debug_post_action_strategy(std::function<action_result(hypothesis_idx)> const & a);
+strategy mk_debug_action_strategy(std::function<action_result(hypothesis_idx)> const & pre,
+                                  std::function<action_result(hypothesis_idx)> const & post,
+                                  std::function<action_result()> const & next);
 }}

src/library/blast/strategies/portfolio.cpp

@@ -7,6 +7,8 @@ Author: Leonardo de Moura
 #include <string>
 #include "library/blast/actions/assert_cc_action.h"
 #include "library/blast/simplifier/simplifier_strategies.h"
+#include "library/blast/unit/unit_actions.h"
+#include "library/blast/forward/ematch.h"
 #include "library/blast/strategies/simple_strategy.h"
 #include "library/blast/strategies/preprocess_strategy.h"
 #include "library/blast/strategies/debug_action_strategy.h"
@@ -18,10 +20,12 @@ static optional<expr> apply_preprocess() {
 }
 
 static optional<expr> apply_simp() {
+    flet<bool> set(get_config().m_simp, true);
     return mk_simplify_using_hypotheses_strategy()();
 }
 
 static optional<expr> apply_simp_nohyps() {
+    flet<bool> set(get_config().m_simp, true);
     return mk_simplify_all_strategy()();
 }
 
@@ -30,9 +34,17 @@ static optional<expr> apply_simple() {
 }
 
 static optional<expr> apply_cc() {
+    flet<bool> set(get_config().m_cc, true);
     return mk_debug_pre_action_strategy(assert_cc_action)();
 }
 
+static optional<expr> apply_ematch() {
+    flet<bool> set(get_config().m_ematch, true);
+    return mk_debug_action_strategy([](hypothesis_idx hidx) { Try(unit_propagate(hidx)); TrySolve(assert_cc_action(hidx)); return action_result::new_branch(); },
+                                    unit_propagate,
+                                    ematch_action)();
+}
+
 optional<expr> apply_strategy() {
     std::string s_name(get_config().m_strategy);
     if (s_name == "preprocess") {
@@ -45,6 +57,8 @@ optional<expr> apply_strategy() {
         return apply_simple();
     } else if (s_name == "cc") {
         return apply_cc();
+    } else if (s_name == "ematch") {
+        return apply_ematch();
     } else {
         // TODO(Leo): add more builtin strategies
         return apply_simple();

tests/lean/run/blast_congr_bug.lean

@@ -4,17 +4,13 @@ attribute P_sub [instance]
 constant q : P → Prop
 
 section
-set_option blast.simp true
-set_option blast.cc   false
-
 example (h₁ h₂ : P) : q h₁ = q h₂ :=
-by blast
+by simp
 end
 
 
 section
-set_option blast.simp false
-set_option blast.cc   true
+set_option blast.strategy "cc"
 
 example (h₁ h₂ : P) : q h₁ = q h₂ :=
 by blast

tests/lean/run/blast_ematch1.lean

@@ -6,10 +6,7 @@ constant g : nat → nat
 definition lemma1 [forward] : ∀ x, (:g (f x):) = x :=
 sorry
 
-set_option blast.init_depth 10
-set_option blast.inc_depth 1000
-set_option blast.subst false
-set_option blast.ematch true
+set_option blast.strategy "ematch"
 
 example (a b c : nat) : a = f b → a = f c → g a ≠ b → false :=
 by blast

tests/lean/run/blast_ematch10.lean

@@ -1,6 +1,5 @@
 attribute iff [reducible]
-set_option blast.subst false
-set_option blast.simp  false
+set_option blast.strategy "ematch"
 
 definition lemma1 (p : nat → Prop) (a b c : nat) : p a → a = b → p b :=
 by blast

tests/lean/run/blast_ematch2.lean

@@ -6,7 +6,7 @@ constant g : nat → nat
 definition lemma1 [forward] : ∀ x, g (f x) = x :=
 sorry
 
-set_option blast.ematch true
+set_option blast.strategy "ematch"
 
 example (a b : nat) : f a = f b → a = b :=
 by blast

tests/lean/run/blast_ematch3.lean

@@ -10,9 +10,7 @@ include s
 attribute add.comm [forward]
 attribute add.assoc [forward]
 
-set_option blast.simp   false
-set_option blast.subst  false
-set_option blast.ematch true
+set_option blast.strategy "ematch"
 
 theorem add_comm_three  (a b c : A) : a + b + c = c + b + a :=
 by blast
@@ -29,9 +27,7 @@ attribute mul.assoc [forward]
 attribute mul.left_inv [forward]
 attribute one_mul [forward]
 
-set_option blast.simp   false
-set_option blast.subst  false
-set_option blast.ematch true
+set_option blast.strategy "ematch"
 
 theorem inv_mul_cancel_left (a b : A) : a⁻¹ * (a * b) = b :=
 by blast

tests/lean/run/blast_ematch4.lean

@@ -3,9 +3,7 @@ open algebra nat
 
 section
 open nat
-set_option blast.simp   false
-set_option blast.subst  false
-set_option blast.ematch true
+set_option blast.strategy "ematch"
 
 attribute add.comm  [forward]
 attribute add.assoc [forward]

tests/lean/run/blast_ematch5.lean

@@ -3,13 +3,7 @@ constant subt : nat → nat → Prop
 lemma subt_trans [forward] {a b c : nat} : subt a b → subt b c → subt a c :=
 sorry
 
-set_option blast.init_depth 20
-set_option blast.inc_depth  100
-set_option blast.ematch   true
-set_option blast.simp     false
--- TODO(Leo): check if unit propagation is still buggy
--- If I remove the following option, blast fails
-set_option blast.backward true -- false
+set_option blast.strategy "ematch"
 
 example (a b c d : nat) : subt a b → subt b c → subt c d → subt a d :=
 by blast

tests/lean/run/blast_ematch6.lean

@@ -7,9 +7,7 @@ section
 variable [s : group A]
 include s
 
-set_option blast.simp   false
-set_option blast.subst  false
-set_option blast.ematch true
+set_option blast.strategy "ematch"
 
 attribute mul_one      [forward]
 attribute mul.assoc    [forward]

tests/lean/run/blast_ematch7.lean

@@ -4,9 +4,8 @@ open algebra
 variables {A : Type} [s : ring A] (a b : A)
 include s
 
-set_option blast.subst  false
-set_option blast.simp   false
-set_option blast.ematch true
+set_option blast.strategy "ematch"
+
 attribute zero_mul [forward]
 
 example : a = 0 → a * b = 0 :=
@@ -14,11 +13,6 @@ by blast
 
 open int
 
--- Remark: int is a non-recursive datatype. So, the recursor action will
--- destruct it. This is a dumb move, and we need to prove the same theorem 4 times because of that.
--- It also demonstrates we need better heuristics for the recursor action and/or annotations.
-set_option blast.recursor false
-
 definition ex1 (a b : int) : a = 0 → a * b = 0 :=
 by blast
 

tests/lean/run/blast_ematch8.lean

@@ -5,9 +5,7 @@ variables {A : Type}
 variables [s : group A]
 include s
 namespace foo
-set_option blast.ematch true
-set_option blast.subst  false
-set_option blast.simp   false
+set_option blast.strategy "ematch"
 attribute inv_inv mul.left_inv mul.assoc one_mul mul_one [forward]
 
 theorem mul.right_inv (a : A) : a * a⁻¹ = 1 :=

tests/lean/run/blast_ematch9.lean

@@ -2,7 +2,7 @@ constant P : nat → Prop
 definition h [reducible] (n : nat) := n
 definition foo [forward] : ∀ x, P (h x) := sorry
 
-set_option blast.ematch true
+set_option blast.strategy "ematch"
 
 example (n : nat) : P (h n) :=
 by blast