feat(library/tactic): add 'clears' and 'reverts' variants

library/tools/tactic.lean

@@ -47,31 +47,37 @@ definition rotate (k : num) := rotate_left k
 inductive expr : Type :=
 builtin : expr
 
-opaque definition apply   (e : expr) : tactic := builtin
-opaque definition rapply  (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
+opaque definition apply      (e : expr)   : tactic := builtin
+opaque definition rapply     (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
+opaque definition clear      (e : expr)   : tactic := builtin
+opaque definition revert     (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
 
 inductive expr_list : Type :=
 nil  : expr_list,
 cons : expr → expr_list → expr_list
 
-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 intro_lst (es : expr_list) : tactic := builtin
+notation `intros`   := intro_lst expr_list.nil
+notation `intros` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := intro_lst 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 generalize_lst (es : expr_list) : tactic := builtin
+notation `generalizes` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := generalize_lst l
 
-opaque definition clear (e : expr) : tactic := builtin
-opaque definition revert (e : expr) : tactic := builtin
+opaque definition clear_lst  (es : expr_list) : tactic := builtin
+notation `clears` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := clear_lst l
+
+opaque definition revert_lst (es : expr_list) : tactic := builtin
+notation `reverts` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := revert_lst l
 
-opaque definition unfold      (e : expr) : tactic := builtin
-opaque definition exact       (e : expr) : tactic := builtin
-opaque definition trace       (s : string) : tactic := builtin
 infixl `;`:15 := and_then
 notation `[` h:10 `|`:10 r:(foldl 10 `|` (e r, or_else r e) h) `]` := r
+
 definition try         (t : tactic) : tactic := [t | id]
 definition repeat1     (t : tactic) : tactic := t ; repeat t
 definition focus       (t : tactic) : tactic := focus_at t 0

src/library/tactic/clear_tactic.cpp

@@ -52,16 +52,24 @@ tactic clear_tactic(name const & n) {
     return tactic01(fn);
 }
 
-static name const & get_clear_arg(expr const & e) {
-    return tactic_expr_to_id(e, "invalid 'clear' tactic, argument must be an identifier");
-}
-
 void initialize_clear_tactic() {
     register_tac(name({"tactic", "clear"}),
                  [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
-                     name n = get_clear_arg(app_arg(e));
+                     name n = tactic_expr_to_id(app_arg(e), "invalid 'clear' tactic, argument must be an identifier");
                      return clear_tactic(n);
                  });
+    register_tac(name({"tactic", "clear_lst"}),
+                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                     buffer<name> ns;
+                     get_tactic_id_list_elements(app_arg(e), ns, "invalid 'clears' tactic, list of identifiers expected");
+                     tactic r = clear_tactic(ns.back());
+                     ns.pop_back();
+                     while (!ns.empty()) {
+                         r = then(clear_tactic(ns.back()), r);
+                         ns.pop_back();
+                     }
+                     return r;
+                 });
 }
 void finalize_clear_tactic() {}
 }

src/library/tactic/generalize_tactic.cpp

@@ -56,7 +56,7 @@ void initialize_generalize_tactic() {
                      return generalize_tactic(fn, get_tactic_expr_expr(app_arg(e)), "x");
                  });
 
-    register_tac(name({"tactic", "generalize_list"}),
+    register_tac(name({"tactic", "generalize_lst"}),
                  [](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");

src/library/tactic/intros_tactic.cpp

@@ -81,7 +81,7 @@ void initialize_intros_tactic() {
                      name const & id = tactic_expr_to_id(app_arg(e), "invalid 'intro' tactic, argument must be an identifier");
                      return intros_tactic(to_list(id));
                  });
-    register_tac(name({"tactic", "intro_list"}),
+    register_tac(name({"tactic", "intro_lst"}),
                  [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
                      buffer<name> ns;
                      get_tactic_id_list_elements(app_arg(e), ns, "invalid 'intros' tactic, arguments must be identifiers");

src/library/tactic/revert_tactic.cpp

@@ -51,16 +51,22 @@ tactic revert_tactic(name const & n) {
     return tactic01(fn);
 }
 
-static name const & get_revert_arg(expr const & e) {
-    return tactic_expr_to_id(e, "invalid 'revert' tactic, argument must be an identifier");
-}
-
 void initialize_revert_tactic() {
     register_tac(name({"tactic", "revert"}),
                  [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
-                     name n = get_revert_arg(app_arg(e));
+                     name n = tactic_expr_to_id(app_arg(e), "invalid 'revert' tactic, argument must be an identifier");
                      return revert_tactic(n);
                  });
+
+    register_tac(name({"tactic", "revert_lst"}),
+                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                     buffer<name> ns;
+                     get_tactic_id_list_elements(app_arg(e), ns, "invalid 'reverts' tactic, list of identifiers expected");
+                     tactic r = revert_tactic(ns[0]);
+                     for (unsigned i = 1; i < ns.size(); i++)
+                         r = then(revert_tactic(ns[i]), r);
+                     return r;
+                 });
 }
 void finalize_revert_tactic() {}
 }

tests/lean/run/clears_tac.lean

@@ -0,0 +1,15 @@
+import logic
+
+example {a b c : Prop} : a → b → c → a ∧ b :=
+begin
+  intros (Ha, Hb, Hc),
+  clears (Hc, c),
+  apply  (and.intro Ha Hb),
+end
+
+example {a b c : Prop} : a → b → c → c ∧ b :=
+begin
+  intros (Ha, Hb, Hc),
+  clears (Ha, a),
+  apply  (and.intro Hc Hb),
+end

tests/lean/run/reverts_tac.lean

@@ -0,0 +1,28 @@
+import logic
+
+theorem tst {a b c : Prop} : a → b → c → a ∧ b :=
+begin
+  intros (Ha, Hb, Hc),
+  reverts (Hb, Ha),
+  intros (Hb2, Ha2),
+  apply (and.intro Ha2 Hb2),
+end
+
+theorem foo1 {A : Type} (a b c : A) (P : A → Prop) : P a → a = b → P b :=
+begin
+  intros  (Hp, Heq),
+  reverts (Heq, Hp),
+  intro Heq,
+  apply (eq.rec_on Heq),
+  intro Pa,
+  apply Pa
+end
+
+theorem foo2 {A : Type} (a b c : A) (P : A → Prop) : P a → a = b → P b :=
+begin
+  intros (Hp, Heq),
+  apply (eq.rec_on Heq Hp)
+end
+
+print definition foo1
+print definition foo2