fix(frontends/lean): rename multiword keyword "suffices to show" to "suffices"

library/data/hf.lean

@@ -364,7 +364,7 @@ theorem insert_erase_subset (a : hf) (s : hf) : s ⊆ insert a (erase a s) :=
 decidable.by_cases
   (assume ains : a ∈ s, by rewrite [!insert_erase ains]; apply subset.refl)
   (assume nains : a ∉ s,
-    suffices to show s ⊆ insert a s, by rewrite [erase_eq_of_not_mem nains]; assumption,
+    suffices s ⊆ insert a s, by rewrite [erase_eq_of_not_mem nains]; assumption,
     subset_insert s a)
 
 theorem insert_subset_insert (a : hf) {s t : hf} : s ⊆ t → insert a s ⊆ insert a t :=

src/emacs/lean-syntax.el

@@ -20,7 +20,7 @@
     "using" "namespace" "section" "fields" "find_decl"
     "attribute" "local" "set_option" "extends" "include" "omit" "classes"
     "instances" "coercions" "metaclasses" "raw" "migrate" "replacing"
-    "calc" "have" "show" "suffices" "to" "by" "in" "at" "let" "forall" "fun"
+    "calc" "have" "show" "suffices" "by" "in" "at" "let" "forall" "fun"
     "exists" "if" "dif" "then" "else" "assume" "assert" "take"
     "obtain" "from")
   "lean keywords ending with 'word' (not symbol)")

src/frontends/lean/builtin_exprs.cpp

@@ -528,14 +528,12 @@ static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos)
 }
 
 static expr parse_suffices_to_show(parser & p, unsigned, expr const *, pos_info const & pos) {
-    p.check_token_or_id_next(get_to_tk(), "invalid 'suffices to show' declaration, 'to' expected");
-    p.check_token_next(get_show_tk(), "invalid 'suffices to show' declaration, 'show' expected");
     auto prop_pos = p.pos();
     expr from  = p.parse_expr();
     expr to    = p.save_pos(mk_expr_placeholder(), prop_pos);
     expr prop  = p.save_pos(mk_arrow(from, to), prop_pos);
     expr local = p.save_pos(mk_local(get_this_tk(), from), prop_pos);
-    p.check_token_next(get_comma_tk(), "invalid 'suffices to show' declaration, ',' expected");
+    p.check_token_next(get_comma_tk(), "invalid 'suffices' declaration, ',' expected");
     expr body;
     {
         parser::local_scope scope(p);
@@ -543,7 +541,7 @@ static expr parse_suffices_to_show(parser & p, unsigned, expr const *, pos_info
         body = parse_proof(p, prop);
     }
     expr proof = p.save_pos(Fun(local, body), pos);
-    p.check_token_next(get_comma_tk(), "invalid 'suffices to show' declaration, ',' expected");
+    p.check_token_next(get_comma_tk(), "invalid 'suffices' declaration, ',' expected");
     expr rest  = p.parse_expr();
     expr r = p.mk_app(proof, rest, pos);
     return r;

src/frontends/lean/tokens.cpp

@@ -50,7 +50,6 @@ static name const * g_assume_tk = nullptr;
 static name const * g_suppose_tk = nullptr;
 static name const * g_take_tk = nullptr;
 static name const * g_fun_tk = nullptr;
-static name const * g_to_tk = nullptr;
 static name const * g_match_tk = nullptr;
 static name const * g_ellipsis_tk = nullptr;
 static name const * g_raw_tk = nullptr;
@@ -203,7 +202,6 @@ void initialize_tokens() {
     g_suppose_tk = new name{"suppose"};
     g_take_tk = new name{"take"};
     g_fun_tk = new name{"fun"};
-    g_to_tk = new name{"to"};
     g_match_tk = new name{"match"};
     g_ellipsis_tk = new name{"..."};
     g_raw_tk = new name{"raw"};
@@ -357,7 +355,6 @@ void finalize_tokens() {
     delete g_suppose_tk;
     delete g_take_tk;
     delete g_fun_tk;
-    delete g_to_tk;
     delete g_match_tk;
     delete g_ellipsis_tk;
     delete g_raw_tk;
@@ -510,7 +507,6 @@ 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; }
 name const & get_fun_tk() { return *g_fun_tk; }
-name const & get_to_tk() { return *g_to_tk; }
 name const & get_match_tk() { return *g_match_tk; }
 name const & get_ellipsis_tk() { return *g_ellipsis_tk; }
 name const & get_raw_tk() { return *g_raw_tk; }

src/frontends/lean/tokens.h

@@ -52,7 +52,6 @@ name const & get_assume_tk();
 name const & get_suppose_tk();
 name const & get_take_tk();
 name const & get_fun_tk();
-name const & get_to_tk();
 name const & get_match_tk();
 name const & get_ellipsis_tk();
 name const & get_raw_tk();

src/frontends/lean/tokens.txt

@@ -45,7 +45,6 @@ assume       assume
 suppose      suppose
 take         take
 fun          fun
-to           to
 match        match
 ellipsis     ...
 raw          raw

tests/lean/run/suffices.lean

@@ -1,6 +1,6 @@
 variables {a b c : Prop}
 
 theorem foo (Ha : a) (Hab : a → b) (Hbc : b → c) : c :=
-suffices to show b, from Hbc this,
-suffices to show a, from Hab this,
+suffices b, from Hbc this,
+suffices a, from Hab this,
 Ha