feat(library/blast/strategies/portfolio): add more strategies for debugging purposes

src/library/blast/strategies/portfolio.cpp

@@ -10,6 +10,8 @@ Author: Leonardo de Moura
 #include "library/blast/simplifier/simplifier_strategies.h"
 #include "library/blast/unit/unit_actions.h"
 #include "library/blast/forward/ematch.h"
+#include "library/blast/backward/backward_action.h"
+#include "library/blast/backward/backward_strategy.h"
 #include "library/blast/strategies/simple_strategy.h"
 #include "library/blast/strategies/preprocess_strategy.h"
 #include "library/blast/strategies/debug_action_strategy.h"
@@ -46,6 +48,14 @@ static optional<expr> apply_ematch() {
                                     ematch_action)();
 }
 
+static optional<expr> apply_constructor() {
+    return mk_debug_action_strategy([]() { return constructor_action(); })();
+}
+
+static optional<expr> apply_backward() {
+    return preprocess_and_then(mk_backward_strategy())();
+}
+
 static optional<expr> apply_unit() {
     return mk_debug_action_strategy(unit_preprocess,
                                     unit_propagate,
@@ -69,8 +79,12 @@ optional<expr> apply_strategy() {
         return apply_cc();
     } else if (s_name == "ematch") {
         return apply_ematch();
+    } else if (s_name == "constructor") {
+        return apply_constructor();
     } else if (s_name == "unit") {
         return apply_unit();
+    } else if (s_name == "backward") {
+        return apply_backward();
     } else {
         throw exception(sstream() << "unknown blast strategy '" << s_name << "'");
     }

tests/lean/run/blast10.lean

@@ -1,6 +1,6 @@
 import data.list
 
-set_option blast.trace true
+set_option blast.strategy "unit"
 
 definition lemma1 : true :=
 by blast

tests/lean/run/blast11.lean

@@ -2,11 +2,11 @@ import data.nat
 open algebra nat
 
 definition lemma1 (a b : nat) : a + b + 0 = b + a :=
-by blast
+by simp
 
 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
+by simp
 
 print lemma2

tests/lean/run/blast12.lean

@@ -1,5 +1,5 @@
 import data.nat
-open algebra nat
+open nat
 
 example (a b : nat) : 0 + a + b + 1 = 1 + a + b :=
-by blast
+by simp

tests/lean/run/blast13.lean

@@ -1,5 +1,6 @@
 import data.list
 open perm
+set_option blast.strategy "cc"
 
 example (p : Prop) (l : list nat) : ¬ l ~ l → p :=
 by blast

tests/lean/run/blast17.lean

@@ -1,2 +1,4 @@
+set_option blast.strategy "preprocess"
+
 example (p q r : Prop) (a b : nat) : true → a = a → q → q → p → p :=
 by blast

tests/lean/run/blast18.lean

@@ -1,4 +1,5 @@
 -- Backward chaining with tagged rules
+set_option blast.strategy "backward"
 constants {P Q R S T U : Prop} (Hpq : P → Q) (Hqr : Q → R) (Hrs : R → S) (Hst : S → T)
 constants (Huq : U → Q) (Hur : U → R) (Hus : U → S) (Hut : U → T)
 attribute Hpq [backward]

tests/lean/run/blast19.lean

@@ -1,4 +1,5 @@
 -- Backward chaining with hypotheses
+set_option blast.strategy "backward"
 constants {P Q R S T U : Prop}
 constants (Huq : U → Q) (Hur : U → R) (Hus : U → S) (Hut : U → T)
 attribute Huq [backward]

tests/lean/run/blast21.lean

@@ -1,4 +1,5 @@
 namespace ex
+set_option blast.strategy "backward"
 
 constant typ : Type₁
 

tests/lean/run/blast3.lean

@@ -1,6 +1,5 @@
 -- TODO(Leo): use better strategy
-set_option blast.strategy "simple"
-set_option blast.cc false
+set_option blast.strategy "constructor"
 
 example (a b c : Prop) : b → c → b ∧ c :=
 by blast