feat(frontends/lean/parse_rewrite_tactic): cleanup rewrite tactic notation

Make a rewrite command sequence explicit.

src/frontends/lean/parse_rewrite_tactic.cpp

@@ -11,10 +11,10 @@ Author: Leonardo de Moura
 
 namespace lean {
 static optional<expr> parse_pattern(parser & p) {
-    if (p.curr_is_token(get_lbracket_tk())) {
+    if (p.curr_is_token(get_lcurly_tk())) {
         p.next();
         expr r = p.parse_expr();
-        p.check_token_next(get_rbracket_tk(), "invalid rewrite pattern, ']' expected");
+        p.check_token_next(get_rcurly_tk(), "invalid rewrite pattern, '}' expected");
         return some_expr(r);
     } else {
         return none_expr();
@@ -80,18 +80,19 @@ expr parse_rewrite_element(parser & p) {
 
 expr parse_rewrite_tactic(parser & p) {
     buffer<expr> elems;
-    while (true) {
+    if (p.curr_is_token(get_lbracket_tk())) {
+        p.next();
+        while (true) {
+            auto pos = p.pos();
+            elems.push_back(p.save_pos(parse_rewrite_element(p), pos));
+            if (!p.curr_is_token(get_comma_tk()))
+                break;
+            p.next();
+        }
+        p.check_token_next(get_rbracket_tk(), "invalid rewrite tactic, ']' expected");
+    } else {
         auto pos = p.pos();
         elems.push_back(p.save_pos(parse_rewrite_element(p), pos));
-        if (!p.curr_is_token(get_sub_tk()) &&
-            !p.curr_is_numeral() &&
-            !p.curr_is_token(get_plus_tk()) &&
-            !p.curr_is_token(get_star_tk()) &&
-            !p.curr_is_token(get_slash_tk()) &&
-            !p.curr_is_identifier() &&
-            !p.curr_is_token(get_lbracket_tk()) &&
-            !p.curr_is_token(get_lparen_tk()))
-            break;
     }
     return mk_rewrite_tactic_expr(elems);
 }

tests/lean/hott/rewriter1.hlean

@@ -5,15 +5,15 @@ constant f {A : Type} : A → A → A
 
 theorem test1 {A : Type} [s : add_comm_group A] (a b c : A) : f (a + 0) (f (a + 0) (a + 0)) = f a (f (0 + a) a) :=
 begin
-  rewrite
+  rewrite [
-    add_right_id at {1 3} -- rewrite 1st and 3rd occurrences
+    add_right_id at {1 3}, -- rewrite 1st and 3rd occurrences
-    [0 + _]add_comm   -- apply commutativity to (0 + _)
+    {0 + _}add_comm]   -- apply commutativity to (0 + _)
 end
 
 axiom Ax {A : Type} [s₁ : has_mul A] [s₂ : has_one A] (a : A) : f (a * 1) (a * 1) = 1
 
 theorem test2 {A : Type} [s : comm_group A] (a b c : A) : f a a = 1 :=
 begin
-  rewrite -(mul_right_id a)  -- - means apply symmetry, rewrite 0 ==> a * 0  at 1st and 2nd occurrences
+  rewrite [-(mul_right_id a),  -- - means apply symmetry, rewrite 0 ==> a * 0  at 1st and 2nd occurrences
-          Ax                 -- use Ax as rewrite rule
+           Ax]                 -- use Ax as rewrite rule
 end

tests/lean/run/rewriter1.lean

@@ -3,7 +3,7 @@ open algebra
 
 theorem test {A : Type} [s : comm_ring A] (a b c : A) : a + b + c = a + c + b :=
 begin
-  rewrite add.assoc [b + _]add.comm -add.assoc,
+  rewrite [add.assoc, {b + _}add.comm, -add.assoc]
 end
 
 print definition test

tests/lean/run/rewriter2.lean

@@ -5,9 +5,8 @@ constant f {A : Type} : A → A → A
 
 theorem test1 {A : Type} [s : comm_ring A] (a b c : A) : f (a + 0) (f (a + 0) (a + 0)) = f a (f (0 + a) a) :=
 begin
-  rewrite
+  rewrite [add_zero at {1 3}, -- rewrite 1st and 3rd occurrences
-    add_zero at {1 3} -- rewrite 1st and 3rd occurrences
+           {0 + _}add.comm]   -- apply commutativity to (0 + _)
-    [0 + _]add.comm   -- apply commutativity to (0 + _)
 end
 
 check @mul_zero
@@ -16,27 +15,27 @@ axiom Ax {A : Type} [s₁ : has_mul A] [s₂ : has_zero A] (a : A) : f (a * 0) (
 
 theorem test2 {A : Type} [s : comm_ring A] (a b c : A) : f 0 0 = 0 :=
 begin
-  rewrite
+  rewrite [
-    -(mul_zero a) at {1 2}  -- - means apply symmetry, rewrite 0 ==> a * 0  at 1st and 2nd occurrences
+    -(mul_zero a) at {1 2},  -- - means apply symmetry, rewrite 0 ==> a * 0  at 1st and 2nd occurrences
-    Ax                      -- use Ax as rewrite rule
+    Ax]                      -- use Ax as rewrite rule
 end
 
 theorem test3 {A : Type} [s : comm_ring A] (a b c : A) : a * 0 + 0 * b + c * 0 + 0 * a = 0 :=
 begin
-  rewrite +mul_zero +zero_mul +add_zero -- in rewrite rules, + is notation for one or more
+  rewrite [+mul_zero, +zero_mul, +add_zero] -- in rewrite rules, + is notation for one or more
 end
 
 print definition test3
 
 theorem test4 {A : Type} [s : comm_ring A] (a b c : A) : a * 0 + 0 * b + c * 0 + 0 * a = 0 :=
 begin
-  rewrite *mul_zero *zero_mul *add_zero *zero_add -- in rewrite rules, * is notation for zero or more
+  rewrite [*mul_zero, *zero_mul, *add_zero, *zero_add] -- in rewrite rules, * is notation for zero or more
 end
 
 theorem test5 {A : Type} [s : comm_ring A] (a b c : A) : a * 0 + 0 * b + c * 0 + 0 * a = 0 :=
 begin
-  rewrite
+  rewrite [
-    2 mul_zero   -- apply mul_zero exactly twice
+    2 mul_zero,   -- apply mul_zero exactly twice
-    2 zero_mul   -- apply zero_mul exactly twice
+    2 zero_mul,  -- apply zero_mul exactly twice
-    5>add_zero   -- apply add_zero at most 5 times
+    5>add_zero]   -- apply add_zero at most 5 times
 end

tests/lean/run/rewriter3.lean

@@ -17,7 +17,6 @@ end
 
 theorem test3 {A : Type} [s : comm_ring A] (a b c : A) (H : a + 0 = 0 + 0) : f a a = f 0 0 :=
 begin
-  rewrite add_zero at H,
+  rewrite [add_zero at H, zero_add at H],
-  rewrite zero_add at H,
   rewrite H
 end