chore(frontends/lean): remove 'assert' keyword

In Lean3, `assert` was just an alias for `have`.

src/emacs/lean-syntax.el

@@ -21,8 +21,7 @@
     "attribute" "local" "set_option" "extends" "include" "omit" "classes"
     "instances" "coercions" "metaclasses" "raw" "migrate" "replacing"
     "calc" "have" "show" "suffices" "by" "in" "at" "do" "let" "forall" "Pi" "fun"
-    "exists" "if" "dif" "then" "else" "assume" "assert" "take"
-    "obtain" "from" "aliases")
+    "exists" "if" "dif" "then" "else" "assume" "take" "obtain" "from" "aliases")
   "lean keywords ending with 'word' (not symbol)")
 (defconst lean-keywords1-regexp
   (eval `(rx word-start (or ,@lean-keywords1) word-end)))

src/frontends/lean/builtin_exprs.cpp

@@ -245,7 +245,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
         expr fn = p.save_pos(mk_local(id, prop, mk_rec_info(true)), id_pos);
         proof = parse_local_equations(p, fn);
     } else {
-        p.check_token_next(get_comma_tk(), "invalid 'have/assert' declaration, ',' expected");
+        p.check_token_next(get_comma_tk(), "invalid 'have' declaration, ',' expected");
         if (prev_local) {
             parser::local_scope scope(p);
             p.add_local(*prev_local);
@@ -257,7 +257,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
             proof = parse_proof(p);
         }
     }
-    p.check_token_next(get_comma_tk(), "invalid 'have/assert' declaration, ',' expected");
+    p.check_token_next(get_comma_tk(), "invalid 'have' declaration, ',' expected");
     parser::local_scope scope(p);
     expr l = p.save_pos(mk_local(id, prop), pos);
     p.add_local(l);
@@ -265,11 +265,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
     if (p.curr_is_token(get_then_tk())) {
         auto then_pos = p.pos();
         p.next();
-        if (p.curr_is_token(get_assert_tk())) {
-            p.next();
-        } else {
-            p.check_token_next(get_have_tk(), "invalid 'then' declaration, 'have' or 'assert' expected");
-        }
+        p.check_token_next(get_have_tk(), "invalid 'then' declaration, 'have' expected");
         body  = parse_have_core(p, then_pos, some_expr(l));
     } else {
         body  = p.parse_expr();
@@ -613,7 +609,6 @@ parse_table init_nud_table() {
     r = r.add({transition("_", mk_ext_action(parse_placeholder))}, x0);
     r = r.add({transition("by", mk_ext_action_core(parse_by))}, x0);
     r = r.add({transition("have", mk_ext_action(parse_have))}, x0);
-    r = r.add({transition("assert", mk_ext_action(parse_have))}, x0);
     r = r.add({transition("suppose", mk_ext_action(parse_suppose))}, x0);
     r = r.add({transition("show", mk_ext_action(parse_show))}, x0);
     r = r.add({transition("suffices", mk_ext_action(parse_suffices_to_show))}, x0);

src/frontends/lean/token_table.cpp

@@ -89,7 +89,7 @@ static char const * g_decreasing_unicode = "↓";
 
 void init_token_table(token_table & t) {
     pair<char const *, unsigned> builtin[] =
-        {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"at", 0}, {"have", 0}, {"assert", 0}, {"suppose", 0}, {"show", 0}, {"suffices", 0}, {"obtain", 0},
+        {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"at", 0}, {"have", 0}, {"suppose", 0}, {"show", 0}, {"suffices", 0}, {"obtain", 0},
          {"do", 0}, {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0}, {"hiding", 0}, {"replacing", 0}, {"renaming", 0},
          {"from", 0}, {"(", g_max_prec}, {"`(", g_max_prec}, {"%%", g_max_prec}, {"()", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec},

src/frontends/lean/tokens.cpp

@@ -47,7 +47,6 @@ static name const * g_import_tk = nullptr;
 static name const * g_prelude_tk = nullptr;
 static name const * g_show_tk = nullptr;
 static name const * g_have_tk = nullptr;
-static name const * g_assert_tk = nullptr;
 static name const * g_assume_tk = nullptr;
 static name const * g_suppose_tk = nullptr;
 static name const * g_take_tk = nullptr;
@@ -196,7 +195,6 @@ void initialize_tokens() {
     g_prelude_tk = new name{"prelude"};
     g_show_tk = new name{"show"};
     g_have_tk = new name{"have"};
-    g_assert_tk = new name{"assert"};
     g_assume_tk = new name{"assume"};
     g_suppose_tk = new name{"suppose"};
     g_take_tk = new name{"take"};
@@ -346,7 +344,6 @@ void finalize_tokens() {
     delete g_prelude_tk;
     delete g_show_tk;
     delete g_have_tk;
-    delete g_assert_tk;
     delete g_assume_tk;
     delete g_suppose_tk;
     delete g_take_tk;
@@ -495,7 +492,6 @@ name const & get_import_tk() { return *g_import_tk; }
 name const & get_prelude_tk() { return *g_prelude_tk; }
 name const & get_show_tk() { return *g_show_tk; }
 name const & get_have_tk() { return *g_have_tk; }
-name const & get_assert_tk() { return *g_assert_tk; }
 name const & get_assume_tk() { return *g_assume_tk; }
 name const & get_suppose_tk() { return *g_suppose_tk; }
 name const & get_take_tk() { return *g_take_tk; }

src/frontends/lean/tokens.h

@@ -49,7 +49,6 @@ name const & get_import_tk();
 name const & get_prelude_tk();
 name const & get_show_tk();
 name const & get_have_tk();
-name const & get_assert_tk();
 name const & get_assume_tk();
 name const & get_suppose_tk();
 name const & get_take_tk();

src/frontends/lean/tokens.txt

@@ -42,7 +42,6 @@ import       import
 prelude      prelude
 show         show
 have         have
-assert       assert
 assume       assume
 suppose      suppose
 take         take

tests/lean/run/have6.lean

@@ -9,11 +9,11 @@ axiom Hb : b
 axiom Hc : c
 check
   have a ∧ b, from and_intro a b Ha Hb,
-  assert b ∧ a, from and_intro b a Hb Ha,
+  have b ∧ a, from and_intro b a Hb Ha,
+  have H : a ∧ b, from and_intro a b Ha Hb,
   have H : a ∧ b, from and_intro a b Ha Hb,
-  assert H : a ∧ b, from and_intro a b Ha Hb,
   then have a ∧ b, from and_intro a b Ha Hb,
-  then assert b ∧ a, from and_intro b a Hb Ha,
+  then have b ∧ a, from and_intro b a Hb Ha,
+  then have H : a ∧ b, from and_intro a b Ha Hb,
   then have H : a ∧ b, from and_intro a b Ha Hb,
-  then assert H : a ∧ b, from and_intro a b Ha Hb,
     Ha