feat(frontends/lean): add syntax-sugar for fold

closes #503

src/emacs/lean-syntax.el

@@ -130,7 +130,7 @@
      (,(rx (not (any "\.")) word-start
            (group
             (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply"
-                "apply" "fapply" "rename" "intro" "intros" "all_goals"
+                "apply" "fapply" "rename" "intro" "intros" "all_goals" "fold"
                 "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "repeat"
                 "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" "esimp" "unfold" "change"))
            word-end)

src/frontends/lean/builtin_exprs.cpp

@@ -518,6 +518,10 @@ static expr parse_esimp_tactic_expr(parser & p, unsigned, expr const *, pos_info
     return p.save_pos(parse_esimp_tactic(p), pos);
 }
 
+static expr parse_fold_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
+    return p.save_pos(parse_fold_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);
@@ -590,6 +594,7 @@ parse_table init_nud_table() {
     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("fold", mk_ext_action(parse_fold_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

@@ -156,4 +156,27 @@ expr parse_esimp_tactic(parser & p) {
     }
     return mk_rewrite_tactic_expr(elems);
 }
+
+expr parse_fold_tactic(parser & p) {
+    buffer<expr> elems;
+    auto pos = p.pos();
+    if (p.curr_is_token(get_lcurly_tk())) {
+        p.next();
+        while (true) {
+            auto pos = p.pos();
+            expr e = p.parse_expr();
+            location loc = parse_tactic_location(p);
+            elems.push_back(p.save_pos(mk_rewrite_fold(e, loc), pos));
+            if (!p.curr_is_token(get_comma_tk()))
+                break;
+            p.next();
+        }
+        p.check_token_next(get_rcurly_tk(), "invalid 'fold' tactic, '}' expected");
+    } else {
+        expr e = p.parse_expr();
+        location loc = parse_tactic_location(p);
+        elems.push_back(p.save_pos(mk_rewrite_fold(e, loc), pos));;
+    }
+    return mk_rewrite_tactic_expr(elems);
+}
 }

src/frontends/lean/parse_rewrite_tactic.h

@@ -11,4 +11,5 @@ namespace lean {
 class parser;
 expr parse_rewrite_tactic(parser & p);
 expr parse_esimp_tactic(parser & p);
+expr parse_fold_tactic(parser & p);
 }

src/frontends/lean/token_table.cpp

@@ -80,7 +80,8 @@ 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}, {";", 1},
-         {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"esimp", 0}, {":=", 0}, {"--", 0}, {"#", 0},
+         {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"esimp", 0}, {"fold", 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/fold.lean

@@ -0,0 +1,16 @@
+definition id {A : Type} (a : A) := a
+
+example (a b c : nat) : id a = id b → a = b :=
+begin
+  intro H,
+  fold {id a, id b},
+  assumption
+end
+
+example (a b c : nat) : id a = id b → a = b :=
+begin
+  intro H,
+  fold (id a),
+  fold (id b),
+  assumption
+end

tests/lean/run/univ1.lean

@@ -4,8 +4,8 @@ namespace S1
 axiom I : Type
 definition F (X : Type) : Type := (X → Prop) → Prop
 axiom unfold.{l} : I.{l} → F I.{l}
-axiom fold.{l}   : F I.{l} → I.{l}
-axiom iso1 : ∀x, fold (unfold x) = x
+axiom foldd.{l}   : F I.{l} → I.{l}
+axiom iso1 : ∀x, foldd (unfold x) = x
 end S1
 
 namespace S2
@@ -13,8 +13,8 @@ universe u
 axiom I : Type.{u}
 definition F (X : Type) : Type := (X → Prop) → Prop
 axiom unfold : I → F I
-axiom fold   : F I → I
-axiom iso1 : ∀x, fold (unfold x) = x
+axiom foldd   : F I → I
+axiom iso1 : ∀x, foldd (unfold x) = x
 end S2
 
 
@@ -23,7 +23,7 @@ context
   hypothesis I : Type
   definition F (X : Type) : Type := (X → Prop) → Prop
   hypothesis unfold : I → F I
-  hypothesis fold   : F I → I
-  hypothesis iso1 : ∀x, fold (unfold x) = x
+  hypothesis foldd   : F I → I
+  hypothesis iso1 : ∀x, foldd (unfold x) = x
 end
 end S3

tests/lean/run/univ2.lean

@@ -3,8 +3,8 @@ import logic
 axiom I : Type
 definition F (X : Type) : Type := (X → Prop) → Prop
 axiom unfold : I → F I
-axiom fold   : F I → I
-axiom iso1 : ∀x, fold (unfold x) = x
+axiom foldd   : F I → I
+axiom iso1 : ∀x, foldd (unfold x) = x
 
-theorem iso2 : ∀x, fold (unfold x) = x
+theorem iso2 : ∀x, foldd (unfold x) = x
 := sorry