feat(library/tactic): add all_goals tactic

closes #501

hott/init/tactic.hlean

@@ -10,7 +10,6 @@ expression. We should view 'tactic' as automation that when execute
 produces a term.  tactic.builtin is just a "dummy" for creating the
 definitions that are actually implemented in C++
 -/
-
 prelude
 import init.datatypes init.reserved_notation init.num
 
@@ -33,6 +32,7 @@ opaque definition at_most     (t : tactic) (k : num)  : tactic := builtin
 opaque definition discard     (t : tactic) (k : num)  : tactic := builtin
 opaque definition focus_at    (t : tactic) (i : num)  : tactic := builtin
 opaque definition try_for     (t : tactic) (ms : num) : tactic := builtin
+opaque definition all_goals   (t : tactic) : tactic := builtin
 opaque definition now         : tactic := builtin
 opaque definition assumption  : tactic := builtin
 opaque definition eassumption : tactic := builtin

library/init/tactic.lean

@@ -32,6 +32,7 @@ opaque definition at_most     (t : tactic) (k : num)  : tactic := builtin
 opaque definition discard     (t : tactic) (k : num)  : tactic := builtin
 opaque definition focus_at    (t : tactic) (i : num)  : tactic := builtin
 opaque definition try_for     (t : tactic) (ms : num) : tactic := builtin
+opaque definition all_goals   (t : tactic) : tactic := builtin
 opaque definition now         : tactic := builtin
 opaque definition assumption  : tactic := builtin
 opaque definition eassumption : tactic := builtin

src/emacs/lean-syntax.el

@@ -130,7 +130,7 @@
      (,(rx (not (any "\.")) word-start
            (group
             (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply"
-                "apply" "fapply" "rename" "intro" "intros"
+                "apply" "fapply" "rename" "intro" "intros" "all_goals"
                 "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "repeat"
                 "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" "esimp" "unfold" "change"))
            word-end)

src/library/constants.cpp

@@ -59,6 +59,7 @@ name const * g_string = nullptr;
 name const * g_string_empty = nullptr;
 name const * g_string_str = nullptr;
 name const * g_tactic = nullptr;
+name const * g_tactic_all_goals = nullptr;
 name const * g_tactic_apply = nullptr;
 name const * g_tactic_assert_hypothesis = nullptr;
 name const * g_tactic_fapply = nullptr;
@@ -171,6 +172,7 @@ void initialize_constants() {
     g_string_empty = new name{"string", "empty"};
     g_string_str = new name{"string", "str"};
     g_tactic = new name{"tactic"};
+    g_tactic_all_goals = new name{"tactic", "all_goals"};
     g_tactic_apply = new name{"tactic", "apply"};
     g_tactic_assert_hypothesis = new name{"tactic", "assert_hypothesis"};
     g_tactic_fapply = new name{"tactic", "fapply"};
@@ -284,6 +286,7 @@ void finalize_constants() {
     delete g_string_empty;
     delete g_string_str;
     delete g_tactic;
+    delete g_tactic_all_goals;
     delete g_tactic_apply;
     delete g_tactic_assert_hypothesis;
     delete g_tactic_fapply;
@@ -396,6 +399,7 @@ name const & get_string_name() { return *g_string; }
 name const & get_string_empty_name() { return *g_string_empty; }
 name const & get_string_str_name() { return *g_string_str; }
 name const & get_tactic_name() { return *g_tactic; }
+name const & get_tactic_all_goals_name() { return *g_tactic_all_goals; }
 name const & get_tactic_apply_name() { return *g_tactic_apply; }
 name const & get_tactic_assert_hypothesis_name() { return *g_tactic_assert_hypothesis; }
 name const & get_tactic_fapply_name() { return *g_tactic_fapply; }

src/library/constants.h

@@ -61,6 +61,7 @@ name const & get_string_name();
 name const & get_string_empty_name();
 name const & get_string_str_name();
 name const & get_tactic_name();
+name const & get_tactic_all_goals_name();
 name const & get_tactic_apply_name();
 name const & get_tactic_assert_hypothesis_name();
 name const & get_tactic_fapply_name();

src/library/constants.txt

@@ -54,6 +54,7 @@ string
 string.empty
 string.str
 tactic
+tactic.all_goals
 tactic.apply
 tactic.assert_hypothesis
 tactic.fapply

src/library/tactic/expr_to_tactic.cpp

@@ -368,6 +368,8 @@ void initialize_expr_to_tactic() {
                      [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); });
     register_unary_tac(get_tactic_repeat_name(),
                        [](tactic const & t1) { return repeat(t1); });
+    register_unary_tac(get_tactic_all_goals_name(),
+                       [](tactic const & t1) { return all_goals(t1); });
     register_unary_num_tac(get_tactic_at_most_name(),
                            [](tactic const & t, unsigned k) { return take(t, k); });
     register_unary_num_tac(get_tactic_discard_name(),

src/library/tactic/tactic.cpp

@@ -289,6 +289,18 @@ tactic focus(tactic const & t, unsigned i) {
         });
 }
 
+tactic all_goals(tactic const & t) {
+    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
+            tactic r   = id_tactic();
+            unsigned i = length(s.get_goals());
+            while (i > 0) {
+                --i;
+                r = then(r, focus(t, i));
+            }
+            return r(env, ios, s);
+        });
+}
+
 DECL_UDATA(proof_state_seq)
 static const struct luaL_Reg proof_state_seq_m[] = {
     {"__gc",            proof_state_seq_gc}, // never throws

src/library/tactic/tactic.h

@@ -146,9 +146,11 @@ inline tactic when(proof_state_pred p, tactic const & t) { return cond(p, t, id_
    The tactic fails if the input state does have at least i goals.
 */
 tactic focus(tactic const & t, unsigned i);
-inline tactic focus(tactic const & t) { return focus(t, 1); }
+inline tactic focus(tactic const & t) { return focus(t, 0); }
 /** \brief Return a tactic that applies beta-reduction. */
 tactic beta_tactic();
+/** \brief Apply \c t to all goals in the proof state */
+tactic all_goals(tactic const & t);
 
 UDATA_DEFS_CORE(proof_state_seq)
 UDATA_DEFS_CORE(tactic);

tests/lean/run/all_goals.lean

@@ -0,0 +1,12 @@
+import data.nat
+open nat
+
+attribute nat.add [unfold-c 2]
+attribute nat.rec_on [unfold-c 2]
+
+example (a b c : nat) : a + 0 = 0 + a ∧ b + 0 = 0 + b :=
+begin
+  apply and.intro,
+  all_goals esimp{of_num},
+  all_goals (state; rewrite zero_add)
+end