feat(library/tactic/generalize): add 'generalizes' syntax sugar, closes #327

library/tools/tactic.lean

@@ -61,6 +61,11 @@ opaque definition intro_list (es : expr_list) : tactic := builtin
 notation `intros`   := intro_list expr_list.nil
 notation `intros` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := intro_list l
 
+opaque definition generalize_list (es : expr_list) : tactic := builtin
+notation `generalizes` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := generalize_list l
+
+opaque definition clear (e : expr) : tactic := builtin
+
 opaque definition unfold      (e : expr) : tactic := builtin
 opaque definition exact       (e : expr) : tactic := builtin
 opaque definition trace       (s : string) : tactic := builtin

src/emacs/lean-syntax.el

@@ -122,7 +122,7 @@
      ;; tactics
      (,(rx (not (any "\.")) word-start
            (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply" "apply" "rename" "intro" "intros"
-               "generalize" "back" "beta" "done" "exact" "repeat" "whnf" "rotate" "rotate_left" "rotate_right")
+               "generalize" "generalizes" "back" "beta" "done" "exact" "repeat" "whnf" "rotate" "rotate_left" "rotate_right")
            word-end)
       . 'font-lock-constant-face)
      ;; Types

src/library/tactic/generalize_tactic.cpp

@@ -55,6 +55,21 @@ void initialize_generalize_tactic() {
                      // TODO(Leo): allow user to provide name to abstract variable
                      return generalize_tactic(fn, get_tactic_expr_expr(app_arg(e)), "x");
                  });
+
+    register_tac(name({"tactic", "generalize_list"}),
+                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                     buffer<expr> args;
+                     get_tactic_expr_list_elements(app_arg(e), args, "invalid 'generalizes' tactic, list of expressions expected");
+                     if (args.empty())
+                         return id_tactic();
+                     tactic r = generalize_tactic(fn, args.back(), "x");
+                     args.pop_back();
+                     while (!args.empty()) {
+                         r = then(generalize_tactic(fn, args.back(), "x"), r);
+                         args.pop_back();
+                     }
+                     return r;
+                 });
 }
 
 void finalize_generalize_tactic() {

tests/lean/run/generalizes.lean

@@ -0,0 +1,8 @@
+import logic
+
+theorem tst (A B : Type) (a : A) (b : B) : a == b → b == a :=
+begin
+  generalizes (a, b, B),
+  intros (B', b, a, H),
+  apply (heq.symm H),
+end