feat(frontends/lean): add 'simp' as shortcut for 'with_options [blast.strategy "simp"] blast'

library/init/tactic.lean

@@ -109,6 +109,9 @@ definition blast (ls : opt_identifier_list) (ds : opt_identifier_list) : tactic
 -- with_options_tac is just a marker for the builtin 'with_options' notation
 definition with_options_tac (o : expr) (t : tactic) : tactic := builtin
 
+definition simp        : tactic := #tactic with_options [blast.strategy "simp"] blast
+definition simp_nohyps : tactic := #tactic with_options [blast.strategy "simp_nohyps"] blast
+
 definition cases (h : expr) (ids : opt_identifier_list) : tactic := builtin
 
 definition induction (h : expr) (rec : using_expr) (ids : opt_identifier_list) : tactic := builtin

src/frontends/lean/builtin_exprs.cpp

@@ -320,6 +320,10 @@ static expr parse_begin_end_plus(parser & p, unsigned, expr const *, pos_info co
     return parse_begin_end_core(p, pos, get_end_tk(), true);
 }
 
+static expr parse_tactic_expr(parser & p, unsigned, expr const *, pos_info const &) {
+    return p.parse_tactic();
+}
+
 static expr parse_proof_qed_core(parser & p, pos_info const & pos) {
     expr r = p.parse_expr();
     p.check_token_next(get_qed_tk(), "invalid proof-qed, 'qed' expected");
@@ -770,6 +774,7 @@ parse_table init_nud_table() {
     r = r.add({transition("let", mk_ext_action(parse_let_expr))}, x0);
     r = r.add({transition("calc", mk_ext_action(parse_calc_expr))}, x0);
     r = r.add({transition("#", mk_ext_action(parse_override_notation))}, x0);
+    r = r.add({transition("#tactic", mk_ext_action(parse_tactic_expr))}, x0);
     r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0);
     r = r.add({transition("@@", mk_ext_action(parse_partial_explicit_expr))}, x0);
     r = r.add({transition("!", mk_ext_action(parse_consume_args_expr))}, x0);

src/frontends/lean/token_table.cpp

@@ -96,8 +96,8 @@ void init_token_table(token_table & t) {
          {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
          {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0},  {"with", 0}, {"...", 0}, {",", 0},
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"xrewrite", 0}, {"krewrite", 0},
-         {"esimp", 0}, {"fold", 0}, {"unfold", 0}, {"with_options", 0}, {"simp", 0},
-         {"generalize", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0},
+         {"esimp", 0}, {"fold", 0}, {"unfold", 0}, {"with_options", 0},
+         {"generalize", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"#tactic", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"begin+", g_max_prec}, {"abstract", g_max_prec},
          {"proof", g_max_prec}, {"qed", 0}, {"@@", g_max_prec}, {"@", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec},

src/library/blast/strategy.cpp

@@ -71,6 +71,8 @@ optional<expr> strategy_fn::search() {
             if (failed(r)) {
                 // all choice points failed...
                 trace(">>> proof not found, no choice points left <<<");
+                if (get_config().m_show_failure)
+                    display_curr_state();
                 return none_expr();
             }
             trace("* next choice point");

tests/lean/run/blast_simp_st1.lean

@@ -0,0 +1,23 @@
+import data.nat
+open algebra nat
+
+section
+open nat
+set_option blast.strategy "preprocess" -- make sure simplifier is not used by default
+
+attribute add.comm      [simp]
+attribute add.assoc     [simp]
+attribute add.left_comm [simp]
+
+example (a b c : nat) : a + b + b + c = c + b + a + b :=
+by simp
+
+example (a b c : nat) : a = b → a + c = c + b :=
+by simp
+
+definition f : nat → nat := sorry
+
+example (a b c : nat) : f a = f b → f a + c = c + f b :=
+by simp
+
+end