From 3ce8c5d6f7bffaca29a8c0ce62fd60de4529537b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 18 Aug 2015 17:04:38 -0700 Subject: [PATCH] feat(frontends/lean): add "suffices to show A, from B, C" construct --- library/data/hf.lean | 4 +++- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/builtin_exprs.cpp | 23 +++++++++++++++++++++++ src/frontends/lean/token_table.cpp | 2 +- src/frontends/lean/tokens.cpp | 4 ++++ src/frontends/lean/tokens.h | 1 + src/frontends/lean/tokens.txt | 1 + tests/lean/run/suffices.lean | 6 ++++++ 8 files changed, 40 insertions(+), 3 deletions(-) create mode 100644 tests/lean/run/suffices.lean diff --git a/library/data/hf.lean b/library/data/hf.lean index d3f0bd582..74983aede 100644 --- a/library/data/hf.lean +++ b/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 diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 4f098ac61..8cb09db78 100644 --- a/src/emacs/lean-syntax.el +++ b/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)") diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 09a38eecd..b046bc87b 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/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 & ps) { buffer 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); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index fb1beac26..460eaf126 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -88,7 +88,7 @@ static char const * g_decreasing_unicode = "↓"; void init_token_table(token_table & t) { pair 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}, diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index c212c5d06..55e279a6f 100644 --- a/src/frontends/lean/tokens.cpp +++ b/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; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index e8d58538a..ab4978f22 100644 --- a/src/frontends/lean/tokens.h +++ b/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(); diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt index 0d50302bf..204d20c29 100644 --- a/src/frontends/lean/tokens.txt +++ b/src/frontends/lean/tokens.txt @@ -45,6 +45,7 @@ assume assume suppose suppose take take fun fun +to to match match ellipsis ... raw raw diff --git a/tests/lean/run/suffices.lean b/tests/lean/run/suffices.lean new file mode 100644 index 000000000..92435231f --- /dev/null +++ b/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