From 323300803922b76a972ebd7586d3f03b4fd8523a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Apr 2015 11:57:40 -0700 Subject: [PATCH] feat(library/tactic): allow user to name generalized term in the 'generalize' tactic closes #421 --- hott/init/tactic.hlean | 2 +- library/init/tactic.lean | 2 +- src/frontends/lean/builtin_tactics.cpp | 29 ++++++++++++++++++++---- src/frontends/lean/token_table.cpp | 1 + src/library/constants.cpp | 8 +++---- src/library/constants.h | 2 +- src/library/constants.txt | 2 +- src/library/tactic/generalize_tactic.cpp | 13 +++++++---- src/library/tactic/generalize_tactic.h | 2 +- tests/lean/gen_as.lean | 9 ++++++++ tests/lean/gen_as.lean.expected.out | 4 ++++ 11 files changed, 56 insertions(+), 18 deletions(-) create mode 100644 tests/lean/gen_as.lean create mode 100644 tests/lean/gen_as.lean.expected.out diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index 397c9723d..42d8b8221 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -68,7 +68,7 @@ opaque definition apply (e : expr) : tactic := builtin opaque definition fapply (e : expr) : tactic := builtin opaque definition rename (a b : identifier) : tactic := builtin opaque definition intro (e : identifier_list) : tactic := builtin -opaque definition generalize (e : expr) : tactic := builtin +opaque definition generalize_tac (e : expr) (id : identifier) : tactic := builtin opaque definition clear (e : identifier_list) : tactic := builtin opaque definition revert (e : identifier_list) : tactic := builtin opaque definition refine (e : expr) : tactic := builtin diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 998225af6..de1a049a0 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -68,7 +68,7 @@ opaque definition apply (e : expr) : tactic := builtin opaque definition fapply (e : expr) : tactic := builtin opaque definition rename (a b : identifier) : tactic := builtin opaque definition intro (e : identifier_list) : tactic := builtin -opaque definition generalize (e : expr) : tactic := builtin +opaque definition generalize_tac (e : expr) (id : identifier) : tactic := builtin opaque definition clear (e : identifier_list) : tactic := builtin opaque definition revert (e : identifier_list) : tactic := builtin opaque definition refine (e : expr) : tactic := builtin diff --git a/src/frontends/lean/builtin_tactics.cpp b/src/frontends/lean/builtin_tactics.cpp index c43e8b1b2..becbbc170 100644 --- a/src/frontends/lean/builtin_tactics.cpp +++ b/src/frontends/lean/builtin_tactics.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "library/tactic/let_tactic.h" +#include "library/tactic/generalize_tactic.h" #include "frontends/lean/tokens.h" #include "frontends/lean/parser.h" #include "frontends/lean/parse_rewrite_tactic.h" @@ -38,16 +39,34 @@ static expr parse_let_tactic(parser & p, unsigned, expr const *, pos_info const return p.save_pos(mk_let_tactic_expr(id, value), pos); } +static expr parse_generalize_tactic(parser & p, unsigned, expr const *, pos_info const & pos) { + expr e = p.parse_expr(); + name id; + if (p.curr_is_token(get_as_tk())) { + p.next(); + id = p.check_atomic_id_next("invalid 'generalize' tactic, identifier expected"); + } else { + if (is_constant(e)) + id = const_name(e); + else if (is_local(e)) + id = local_pp_name(e); + else + id = name("x"); + } + return p.save_pos(mk_generalize_tactic_expr(e, id), pos); +} + parse_table init_tactic_nud_table() { action Expr(mk_expr_action()); expr x0 = mk_var(0); parse_table r; r = r.add({transition("(", Expr), transition(")", mk_ext_action(parse_rparen))}, 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("unfold", mk_ext_action(parse_unfold_tactic_expr))}, x0); - r = r.add({transition("fold", mk_ext_action(parse_fold_tactic_expr))}, x0); - r = r.add({transition("let", mk_ext_action(parse_let_tactic))}, 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("generalize", mk_ext_action(parse_generalize_tactic))}, x0); + r = r.add({transition("unfold", mk_ext_action(parse_unfold_tactic_expr))}, x0); + r = r.add({transition("fold", mk_ext_action(parse_fold_tactic_expr))}, x0); + r = r.add({transition("let", mk_ext_action(parse_let_tactic))}, x0); return r; } diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 50245cc87..f7f48c4a8 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -95,6 +95,7 @@ void init_token_table(token_table & t) { {"{|", g_max_prec}, {"|}", 0}, {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0}, {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"esimp", 0}, {"fold", 0}, {"unfold", 0}, + {"generalize", 0}, {"as", 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}, diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 76ad7d3d3..0127b3769 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -91,7 +91,7 @@ name const * g_tactic_opt_identifier_list = nullptr; name const * g_tactic_fail = nullptr; name const * g_tactic_fixpoint = nullptr; name const * g_tactic_focus_at = nullptr; -name const * g_tactic_generalize = nullptr; +name const * g_tactic_generalize_tac = nullptr; name const * g_tactic_generalizes = nullptr; name const * g_tactic_id = nullptr; name const * g_tactic_interleave = nullptr; @@ -210,7 +210,7 @@ void initialize_constants() { g_tactic_fail = new name{"tactic", "fail"}; g_tactic_fixpoint = new name{"tactic", "fixpoint"}; g_tactic_focus_at = new name{"tactic", "focus_at"}; - g_tactic_generalize = new name{"tactic", "generalize"}; + g_tactic_generalize_tac = new name{"tactic", "generalize_tac"}; g_tactic_generalizes = new name{"tactic", "generalizes"}; g_tactic_id = new name{"tactic", "id"}; g_tactic_interleave = new name{"tactic", "interleave"}; @@ -330,7 +330,7 @@ void finalize_constants() { delete g_tactic_fail; delete g_tactic_fixpoint; delete g_tactic_focus_at; - delete g_tactic_generalize; + delete g_tactic_generalize_tac; delete g_tactic_generalizes; delete g_tactic_id; delete g_tactic_interleave; @@ -449,7 +449,7 @@ name const & get_tactic_opt_identifier_list_name() { return *g_tactic_opt_identi name const & get_tactic_fail_name() { return *g_tactic_fail; } name const & get_tactic_fixpoint_name() { return *g_tactic_fixpoint; } name const & get_tactic_focus_at_name() { return *g_tactic_focus_at; } -name const & get_tactic_generalize_name() { return *g_tactic_generalize; } +name const & get_tactic_generalize_tac_name() { return *g_tactic_generalize_tac; } name const & get_tactic_generalizes_name() { return *g_tactic_generalizes; } name const & get_tactic_id_name() { return *g_tactic_id; } name const & get_tactic_interleave_name() { return *g_tactic_interleave; } diff --git a/src/library/constants.h b/src/library/constants.h index 4709ad49d..bc1c7a964 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -93,7 +93,7 @@ name const & get_tactic_opt_identifier_list_name(); name const & get_tactic_fail_name(); name const & get_tactic_fixpoint_name(); name const & get_tactic_focus_at_name(); -name const & get_tactic_generalize_name(); +name const & get_tactic_generalize_tac_name(); name const & get_tactic_generalizes_name(); name const & get_tactic_id_name(); name const & get_tactic_interleave_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index bb0be82c8..b5b2266e6 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -86,7 +86,7 @@ tactic.opt_identifier_list tactic.fail tactic.fixpoint tactic.focus_at -tactic.generalize +tactic.generalize_tac tactic.generalizes tactic.id tactic.interleave diff --git a/src/library/tactic/generalize_tactic.cpp b/src/library/tactic/generalize_tactic.cpp index 3ee31884a..b8ca55ff3 100644 --- a/src/library/tactic/generalize_tactic.cpp +++ b/src/library/tactic/generalize_tactic.cpp @@ -12,6 +12,11 @@ Author: Leonardo de Moura #include "library/tactic/expr_to_tactic.h" namespace lean { +expr mk_generalize_tactic_expr(expr const & e, name const & id) { + return mk_app(mk_constant(get_tactic_generalize_tac_name()), + e, mk_constant(id)); +} + tactic generalize_tactic(elaborate_fn const & elab, expr const & e, name const & x) { return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) { proof_state new_s = s; @@ -60,11 +65,11 @@ tactic generalize_tactic(elaborate_fn const & elab, expr const & e, name const & } void initialize_generalize_tactic() { - register_tac(get_tactic_generalize_name(), + register_tac(get_tactic_generalize_tac_name(), [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - check_tactic_expr(app_arg(e), "invalid 'generalize' tactic, invalid argument"); - // TODO(Leo): allow user to provide name to abstract variable - return generalize_tactic(fn, get_tactic_expr_expr(app_arg(e)), "x"); + check_tactic_expr(app_arg(app_fn(e)), "invalid 'generalize' tactic, invalid argument"); + name id = tactic_expr_to_id(app_arg(e), "invalid 'generalize' tactic, argument must be an identifier"); + return generalize_tactic(fn, get_tactic_expr_expr(app_arg(app_fn(e))), id); }); register_tac(get_tactic_generalizes_name(), diff --git a/src/library/tactic/generalize_tactic.h b/src/library/tactic/generalize_tactic.h index ad74f1b22..03daddf41 100644 --- a/src/library/tactic/generalize_tactic.h +++ b/src/library/tactic/generalize_tactic.h @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "library/tactic/elaborate.h" namespace lean { -tactic generalize_tactic(elaborate_fn const & elab, expr const & e); +expr mk_generalize_tactic_expr(expr const & e, name const & id); void initialize_generalize_tactic(); void finalize_generalize_tactic(); } diff --git a/tests/lean/gen_as.lean b/tests/lean/gen_as.lean new file mode 100644 index 000000000..7a7756a2c --- /dev/null +++ b/tests/lean/gen_as.lean @@ -0,0 +1,9 @@ +import data.nat +open nat + +example (x y : nat) : x + y + y ≥ 0 := +begin + generalize x + y + y as n, + state, + intro n, exact zero_le n +end diff --git a/tests/lean/gen_as.lean.expected.out b/tests/lean/gen_as.lean.expected.out new file mode 100644 index 000000000..7be3850cf --- /dev/null +++ b/tests/lean/gen_as.lean.expected.out @@ -0,0 +1,4 @@ +gen_as.lean:7:2: proof state +x y : ℕ +⊢ ∀ (n : ℕ), + n ≥ 0