feat(frontends/lean): add esimp tactic based on rewrite tactic

closes #358

src/emacs/lean-syntax.el

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

src/frontends/lean/builtin_exprs.cpp

@@ -415,6 +415,10 @@ static expr parse_rewrite_tactic_expr(parser & p, unsigned, expr const *, pos_in
     return p.save_pos(parse_rewrite_tactic(p), pos);
 }
 
+static expr parse_esimp_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
+    return p.save_pos(parse_esimp_tactic(p), pos);
+}
+
 static expr parse_overwrite_notation(parser & p, unsigned, expr const *, pos_info const &) {
     name n = p.check_id_next("invalid '#' local notation, identifier expected");
     environment env = overwrite_notation(p.env(), n);
@@ -485,6 +489,7 @@ parse_table init_nud_table() {
     r = r.add({transition("let", mk_ext_action(parse_let_expr))}, x0);
     r = r.add({transition("calc", mk_ext_action(parse_calc_expr))}, x0);
     r = r.add({transition("rewrite", mk_ext_action(parse_rewrite_tactic_expr))}, x0);
+    r = r.add({transition("esimp", mk_ext_action(parse_esimp_tactic_expr))}, x0);
     r = r.add({transition("#", mk_ext_action(parse_overwrite_notation))}, x0);
     r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0);
     r = r.add({transition("!", mk_ext_action(parse_consume_args_expr))}, x0);

src/frontends/lean/parse_rewrite_tactic.cpp

@@ -32,8 +32,8 @@ static expr parse_rule(parser & p) {
     }
 }
 
-expr parse_rewrite_element(parser & p) {
-    if (p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk())) {
+static expr parse_rewrite_unfold(parser & p) {
+    lean_assert(p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk()));
     p.next();
     buffer<name> to_unfold;
     if (p.curr_is_token(get_lcurly_tk())) {
@@ -50,7 +50,11 @@ expr parse_rewrite_element(parser & p) {
     }
     location loc = parse_tactic_location(p);
     return mk_rewrite_unfold(to_list(to_unfold), loc);
-    }
+}
+
+expr parse_rewrite_element(parser & p) {
+    if (p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk()))
+        return parse_rewrite_unfold(p);
     bool symm = false;
     if (p.curr_is_token(get_sub_tk())) {
         p.next();
@@ -123,4 +127,15 @@ expr parse_rewrite_tactic(parser & p) {
     }
     return mk_rewrite_tactic_expr(elems);
 }
+
+expr parse_esimp_tactic(parser & p) {
+    buffer<expr> elems;
+    if (p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk())) {
+        elems.push_back(parse_rewrite_unfold(p));
+    } else {
+        location loc = parse_tactic_location(p);
+        elems.push_back(mk_rewrite_reduce(loc));
+    }
+    return mk_rewrite_tactic_expr(elems);
+}
 }

src/frontends/lean/parse_rewrite_tactic.h

@@ -10,4 +10,5 @@ Author: Leonardo de Moura
 namespace lean {
 class parser;
 expr parse_rewrite_tactic(parser & p);
+expr parse_esimp_tactic(parser & p);
 }

src/frontends/lean/token_table.cpp

@@ -80,7 +80,7 @@ void init_token_table(token_table & t) {
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec},
          {"{|", 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}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"esimp", 0}, {":=", 0}, {"--", 0}, {"#", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec},
          {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0},

tests/lean/run/esimp1.lean

@@ -0,0 +1,28 @@
+open nat
+
+example (x y : nat) (H : (fun (a : nat),  sigma.pr1 ⟨a, y⟩) x = 0) : x = 0 :=
+begin
+  esimp at H,
+  exact H
+end
+
+definition foo [irreducible] (a : nat) := a
+
+example (x y : nat) (H : (fun (a : nat), sigma.pr1 ⟨foo a, y⟩) x = 0) : x = 0 :=
+begin
+  esimp ↑foo at H,
+  exact H
+end
+
+example (x y : nat) (H : x = 0) : (fun (a : nat), sigma.pr1 ⟨foo a, y⟩) x = 0 :=
+begin
+  esimp ↑foo,
+  exact H
+end
+
+example (x y : nat) (H : x = 0) : (fun (a : nat), sigma.pr1 ⟨foo a, y⟩) x = 0 :=
+begin
+  esimp,
+  unfold foo,
+  exact H
+end