feat(frontends/lean): add "suffices to show A, from B, C" construct

library/data/hf.lean

@@ -363,7 +363,9 @@ hf.subset.trans (!hf.erase_subset_erase H) (erase_insert_subset a t)
 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, by rewrite[erase_eq_of_not_mem nains]; apply subset_insert)
+  (assume nains : a ∉ s,
+    suffices to show 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 :=
 begin

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" "by" "in" "at" "let" "forall" "fun"
+    "calc" "have" "show" "suffices" "to" "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

@@ -527,6 +527,28 @@ 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");
+    expr body;
+    {
+        parser::local_scope scope(p);
+        p.add_local(local);
+        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");
+    expr rest  = p.parse_expr();
+    expr r = p.mk_app(proof, rest, pos);
+    return r;
+}
+
 static obtain_struct parse_obtain_decls (parser & p, buffer<expr> & ps) {
     buffer<obtain_struct> children;
     parser::local_scope scope(p);
@@ -698,6 +720,7 @@ parse_table init_nud_table() {
     r = r.add({transition("assert", mk_ext_action(parse_assert))}, 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);
     r = r.add({transition("obtain", mk_ext_action(parse_obtain))}, x0);
     r = r.add({transition("abstract", mk_ext_action(parse_nested_declaration))}, x0);
     r = r.add({transition("if", mk_ext_action(parse_if_then_else))}, x0);

src/frontends/lean/token_table.cpp

@@ -88,7 +88,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}, {"obtain", 0},
+        {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"at", 0}, {"have", 0}, {"assert", 0}, {"suppose", 0}, {"show", 0}, {"suffices", 0}, {"obtain", 0},
          {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0}, {"by+", 0}, {"hiding", 0}, {"replacing", 0}, {"renaming", 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},

src/frontends/lean/tokens.cpp

@@ -50,6 +50,7 @@ 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;
@@ -202,6 +203,7 @@ 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"};
@@ -355,6 +357,7 @@ 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;
@@ -507,6 +510,7 @@ 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,6 +52,7 @@ 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,6 +45,7 @@ assume       assume
 suppose      suppose
 take         take
 fun          fun
+to           to
 match        match
 ellipsis     ...
 raw          raw

tests/lean/run/suffices.lean

@@ -0,0 +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,
+Ha