feat(frontends/lean): polish rewrite tactic notation

src/frontends/lean/parse_rewrite_tactic.cpp

@@ -33,7 +33,7 @@ static expr parse_rule(parser & p) {
 }
 
 expr parse_rewrite_element(parser & p) {
-    if (p.curr_is_token(get_slash_tk())) {
+    if (p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk())) {
         p.next();
         name n = p.check_id_next("invalid unfold rewrite step, identifier expected");
         location loc = parse_tactic_location(p);
@@ -80,7 +80,8 @@ expr parse_rewrite_element(parser & p) {
 
 expr parse_rewrite_tactic(parser & p) {
     buffer<expr> elems;
-    if (p.curr_is_token(get_lbracket_tk())) {
+    bool lbraket = p.curr_is_token(get_lbracket_tk());
+    if (lbraket || p.curr_is_token(get_langle_tk())) {
         p.next();
         while (true) {
             auto pos = p.pos();
@@ -89,7 +90,10 @@ expr parse_rewrite_tactic(parser & p) {
                 break;
             p.next();
         }
-        p.check_token_next(get_rbracket_tk(), "invalid rewrite tactic, ']' expected");
+        if (lbraket)
+            p.check_token_next(get_rbracket_tk(), "invalid rewrite tactic, ']' expected");
+        else
+            p.check_token_next(get_rangle_tk(), "invalid rewrite tactic, '⟩' expected");
     } else {
         auto pos = p.pos();
         elems.push_back(p.save_pos(parse_rewrite_element(p), pos));

src/frontends/lean/token_table.cpp

@@ -78,7 +78,7 @@ void init_token_table(token_table & t) {
          {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0},
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec},
-         {"{|", g_max_prec}, {"|}", 0}, {"⊢", 0},
+         {"{|", g_max_prec}, {"|}", 0}, {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
          {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0},  {"with", 0}, {"...", 0}, {",", 0},
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {":=", 0}, {"--", 0}, {"#", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},

src/frontends/lean/tokens.cpp

@@ -22,6 +22,11 @@ static name * g_lcurlybar    = nullptr;
 static name * g_rcurlybar    = nullptr;
 static name * g_lbracket     = nullptr;
 static name * g_rbracket     = nullptr;
+static name * g_langle       = nullptr;
+static name * g_rangle       = nullptr;
+static name * g_triangle     = nullptr;
+static name * g_caret        = nullptr;
+static name * g_up           = nullptr;
 static name * g_bar          = nullptr;
 static name * g_comma        = nullptr;
 static name * g_add          = nullptr;
@@ -131,6 +136,11 @@ void initialize_tokens() {
     g_rcurlybar    = new name("|}");
     g_lbracket     = new name("[");
     g_rbracket     = new name("]");
+    g_langle       = new name("⟨");
+    g_rangle       = new name("⟩");
+    g_triangle     = new name("▸");
+    g_caret        = new name("^");
+    g_up           = new name("↑");
     g_bar          = new name("|");
     g_comma        = new name(",");
     g_add          = new name("+");
@@ -318,6 +328,11 @@ void finalize_tokens() {
     delete g_turnstile;
     delete g_comma;
     delete g_bar;
+    delete g_langle;
+    delete g_rangle;
+    delete g_triangle;
+    delete g_caret;
+    delete g_up;
     delete g_rbracket;
     delete g_lbracket;
     delete g_rdcurly;
@@ -339,6 +354,11 @@ name const & get_period_tk() { return *g_period; }
 name const & get_placeholder_tk() { return *g_placeholder; }
 name const & get_colon_tk() { return *g_colon; }
 name const & get_dcolon_tk() { return *g_dcolon; }
+name const & get_langle_tk() { return *g_langle; }
+name const & get_rangle_tk() { return *g_rangle; }
+name const & get_triangle_tk() { return *g_triangle; }
+name const & get_caret_tk() { return *g_caret; }
+name const & get_up_tk() { return *g_up; }
 name const & get_lparen_tk() { return *g_lparen; }
 name const & get_rparen_tk() { return *g_rparen; }
 name const & get_llevel_curly_tk() { return *g_llevel_curly; }

src/frontends/lean/tokens.h

@@ -24,6 +24,11 @@ name const & get_lcurlybar_tk();
 name const & get_rcurlybar_tk();
 name const & get_lbracket_tk();
 name const & get_rbracket_tk();
+name const & get_langle_tk();
+name const & get_rangle_tk();
+name const & get_triangle_tk();
+name const & get_caret_tk();
+name const & get_up_tk();
 name const & get_bar_tk();
 name const & get_comma_tk();
 name const & get_add_tk();

tests/lean/run/rewrite4.lean

@@ -0,0 +1,13 @@
+import data.nat
+open algebra
+
+constant f {A : Type} : A → A → A
+
+theorem test1 {A : Type} [s : comm_ring A] (a b c : A) (H : a + 0 = 0) : f a a = f 0 0 :=
+by rewrite ⟨add_zero at H, H⟩
+
+theorem test2 {A : Type} [s : comm_ring A] (a b c : A) (H : a + 0 = 0) : f a a = f 0 0 :=
+by rewrite ⟨add_zero at *, H⟩
+
+theorem test3 {A : Type} [s : comm_ring A] (a b c : A) (H : a + 0 = 0 + 0) : f a a = f 0 0 :=
+by rewrite ⟨add_zero at H, zero_add at H, H⟩