feat(library/tactic): add 'fapply' tactic, closes #356

library/tools/tactic.lean

@@ -49,6 +49,7 @@ builtin : expr
 
 opaque definition apply      (e : expr)   : tactic := builtin
 opaque definition rapply     (e : expr)   : tactic := builtin
+opaque definition fapply     (e : expr)   : tactic := builtin
 opaque definition rename     (a b : expr) : tactic := builtin
 opaque definition intro      (e : expr)   : tactic := builtin
 opaque definition generalize (e : expr)   : tactic := builtin

src/emacs/lean-syntax.el

@@ -122,7 +122,7 @@
      ;; tactics
      ("cases[ \t\n]+[^ \t\n]+[ \t\n]+\\(with\\)" (1 'font-lock-constant-face))
      (,(rx (not (any "\.")) word-start
-           (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply" "apply" "rename" "intro" "intros"
+           (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply" "apply" "fapply" "rename" "intro" "intros"
                "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "repeat"
                "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases")
            word-end)

src/library/tactic/apply_tactic.cpp

@@ -51,7 +51,7 @@ static void remove_redundant_metas(buffer<expr> & metas) {
     metas.shrink(k);
 }
 
-enum subgoals_action_kind { IgnoreSubgoals, AddRevSubgoals, AddSubgoals };
+enum subgoals_action_kind { IgnoreSubgoals, AddRevSubgoals, AddSubgoals, AddAllSubgoals };
 
 static proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s,
                                          expr const & _e, buffer<constraint> & cs,
@@ -114,8 +114,9 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
                     for (unsigned i = 0; i < metas.size(); i++)
                         new_gs = cons(goal(metas[i], new_subst.instantiate_all(tc->infer(metas[i]).first)), new_gs);
                 } else {
-                    lean_assert(subgoals_action == AddSubgoals);
+                    lean_assert(subgoals_action == AddSubgoals || subgoals_action == AddAllSubgoals);
-                    remove_redundant_metas(metas);
+                    if (subgoals_action == AddSubgoals)
+                        remove_redundant_metas(metas);
                     unsigned i = metas.size();
                     while (i > 0) {
                         --i;
@@ -149,7 +150,7 @@ tactic eassumption_tactic() {
         });
 }
 
-tactic apply_tactic(elaborate_fn const & elab, expr const & e, bool rev) {
+tactic apply_tactic_core(elaborate_fn const & elab, expr const & e, subgoals_action_kind k) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
             goals const & gs = s.get_goals();
             if (empty(gs))
@@ -163,10 +164,22 @@ tactic apply_tactic(elaborate_fn const & elab, expr const & e, bool rev) {
             to_buffer(ecs.second, cs);
             to_buffer(s.get_postponed(), cs);
             proof_state new_s(s, ngen, constraints());
-            return apply_tactic_core(env, ios, new_s, new_e, cs, true, rev ? AddRevSubgoals : AddSubgoals);
+            return apply_tactic_core(env, ios, new_s, new_e, cs, true, k);
         });
 }
 
+tactic apply_tactic(elaborate_fn const & elab, expr const & e) {
+    return apply_tactic_core(elab, e, AddSubgoals);
+}
+
+tactic fapply_tactic(elaborate_fn const & elab, expr const & e) {
+    return apply_tactic_core(elab, e, AddAllSubgoals);
+}
+
+tactic rapply_tactic(elaborate_fn const & elab, expr const & e) {
+    return apply_tactic_core(elab, e, AddRevSubgoals);
+}
+
 int mk_eassumption_tactic(lua_State * L) { return push_tactic(L, eassumption_tactic()); }
 void open_apply_tactic(lua_State * L) {
     SET_GLOBAL_FUN(mk_eassumption_tactic, "eassumption_tac");
@@ -176,13 +189,19 @@ void initialize_apply_tactic() {
     register_tac(name({"tactic", "apply"}),
                  [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      check_tactic_expr(app_arg(e), "invalid 'apply' tactic, invalid argument");
-                     return apply_tactic(fn, get_tactic_expr_expr(app_arg(e)), false);
+                     return apply_tactic(fn, get_tactic_expr_expr(app_arg(e)));
                  });
 
     register_tac(name({"tactic", "rapply"}),
                  [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
-                     check_tactic_expr(app_arg(e), "invalid 'apply' tactic, invalid argument");
+                     check_tactic_expr(app_arg(e), "invalid 'rapply' tactic, invalid argument");
-                     return apply_tactic(fn, get_tactic_expr_expr(app_arg(e)), true);
+                     return rapply_tactic(fn, get_tactic_expr_expr(app_arg(e)));
+                 });
+
+    register_tac(name({"tactic", "fapply"}),
+                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                     check_tactic_expr(app_arg(e), "invalid 'fapply' tactic, invalid argument");
+                     return fapply_tactic(fn, get_tactic_expr_expr(app_arg(e)));
                  });
 
     register_simple_tac(name({"tactic", "eassumption"}),

src/library/tactic/apply_tactic.h

@@ -8,7 +8,9 @@ Author: Leonardo de Moura
 #include "util/lua.h"
 #include "library/tactic/elaborate.h"
 namespace lean {
-tactic apply_tactic(elaborate_fn const & fn, expr const & e, bool rev_goals = false);
+tactic apply_tactic(elaborate_fn const & fn, expr const & e);
+tactic rapply_tactic(elaborate_fn const & fn, expr const & e);
+tactic fapply_tactic(elaborate_fn const & fn, expr const & e);
 tactic eassumption_tactic();
 void open_apply_tactic(lua_State * L);
 void initialize_apply_tactic();

tests/lean/run/fapply.lean

@@ -0,0 +1,8 @@
+import logic
+
+example : ∃ a : num, a = a :=
+begin
+  fapply exists_intro,
+  exact 0,
+  apply rfl,
+end