From 85409a59d36e6f373e57cb7d60aea8d33c6aad45 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 27 May 2015 16:32:43 -0700 Subject: [PATCH] feat(library/tactic/rewrite_tactic): add xrewrite and krewrite tactic variants closes #511 --- hott/init/tactic.hlean | 4 +- library/init/tactic.lean | 4 +- src/emacs/lean-syntax.el | 7 +- src/frontends/lean/builtin_tactics.cpp | 10 ++ src/frontends/lean/parse_rewrite_tactic.cpp | 20 +++- src/frontends/lean/parse_rewrite_tactic.h | 2 + src/frontends/lean/token_table.cpp | 12 +- src/library/tactic/rewrite_tactic.cpp | 115 +++++++++++++++----- src/library/tactic/rewrite_tactic.h | 2 + tests/lean/run/511a.lean | 14 +++ 10 files changed, 151 insertions(+), 39 deletions(-) create mode 100644 tests/lean/run/511a.lean diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index d08e41df3..d1b43860e 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -87,7 +87,9 @@ definition trace (s : string) : tactic := builtin -- rewrite_tac is just a marker for the builtin 'rewrite' notation -- used to create instances of this tactic. -definition rewrite_tac (e : expr_list) : tactic := builtin +definition rewrite_tac (e : expr_list) : tactic := builtin +definition xrewrite_tac (e : expr_list) : tactic := builtin +definition krewrite_tac (e : expr_list) : tactic := builtin definition cases (id : identifier) (ids : opt_identifier_list) : tactic := builtin diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 4bfa43182..72dd1a852 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -87,7 +87,9 @@ definition trace (s : string) : tactic := builtin -- rewrite_tac is just a marker for the builtin 'rewrite' notation -- used to create instances of this tactic. -definition rewrite_tac (e : expr_list) : tactic := builtin +definition rewrite_tac (e : expr_list) : tactic := builtin +definition xrewrite_tac (e : expr_list) : tactic := builtin +definition krewrite_tac (e : expr_list) : tactic := builtin definition cases (id : identifier) (ids : opt_identifier_list) : tactic := builtin diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index dab26aad5..386464836 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -137,9 +137,10 @@ (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply" "apply" "fapply" "eapply" "rename" "intro" "intros" "all_goals" "fold" "focus" "focus_at" "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "rexact" - "refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" "esimp" - "unfold" "change" "check_expr" "contradiction" "exfalso" "split" "existsi" "constructor" "left" "right" - "injection" "congruence" "reflexivity" "symmetry" "transitivity" "state" "induction" "induction_using" + "refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" + "xrewrite" "krewrite" "esimp" "unfold" "change" "check_expr" "contradiction" + "exfalso" "split" "existsi" "constructor" "left" "right" "injection" "congruence" "reflexivity" + "symmetry" "transitivity" "state" "induction" "induction_using" "substvars")) word-end) (1 'font-lock-constant-face)) diff --git a/src/frontends/lean/builtin_tactics.cpp b/src/frontends/lean/builtin_tactics.cpp index bf1809998..b652a9cb6 100644 --- a/src/frontends/lean/builtin_tactics.cpp +++ b/src/frontends/lean/builtin_tactics.cpp @@ -16,6 +16,14 @@ static expr parse_rewrite_tactic_expr(parser & p, unsigned, expr const *, pos_in return p.save_pos(parse_rewrite_tactic(p), pos); } +static expr parse_xrewrite_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) { + return p.save_pos(parse_xrewrite_tactic(p), pos); +} + +static expr parse_krewrite_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) { + return p.save_pos(parse_krewrite_tactic(p), pos); +} + static expr parse_esimp_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) { return p.save_pos(parse_esimp_tactic(p), pos); } @@ -62,6 +70,8 @@ parse_table init_tactic_nud_table() { 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("krewrite", mk_ext_action(parse_krewrite_tactic_expr))}, x0); + r = r.add({transition("xrewrite", mk_ext_action(parse_xrewrite_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); diff --git a/src/frontends/lean/parse_rewrite_tactic.cpp b/src/frontends/lean/parse_rewrite_tactic.cpp index 677b90d14..6c3d6a401 100644 --- a/src/frontends/lean/parse_rewrite_tactic.cpp +++ b/src/frontends/lean/parse_rewrite_tactic.cpp @@ -120,8 +120,7 @@ static expr parse_rewrite_element(parser & p, bool use_paren) { } } -expr parse_rewrite_tactic(parser & p) { - buffer elems; +void parse_rewrite_tactic_elems(parser & p, buffer & elems) { if (p.curr_is_token(get_lbracket_tk())) { p.next(); while (true) { @@ -136,9 +135,26 @@ expr parse_rewrite_tactic(parser & p) { auto pos = p.pos(); elems.push_back(p.save_pos(parse_rewrite_element(p, true), pos)); } +} + +expr parse_rewrite_tactic(parser & p) { + buffer elems; + parse_rewrite_tactic_elems(p, elems); return mk_rewrite_tactic_expr(elems); } +expr parse_xrewrite_tactic(parser & p) { + buffer elems; + parse_rewrite_tactic_elems(p, elems); + return mk_xrewrite_tactic_expr(elems); +} + +expr parse_krewrite_tactic(parser & p) { + buffer elems; + parse_rewrite_tactic_elems(p, elems); + return mk_krewrite_tactic_expr(elems); +} + expr parse_esimp_tactic(parser & p) { buffer elems; auto pos = p.pos(); diff --git a/src/frontends/lean/parse_rewrite_tactic.h b/src/frontends/lean/parse_rewrite_tactic.h index 8ca998cd0..367cb7318 100644 --- a/src/frontends/lean/parse_rewrite_tactic.h +++ b/src/frontends/lean/parse_rewrite_tactic.h @@ -10,6 +10,8 @@ Author: Leonardo de Moura namespace lean { class parser; expr parse_rewrite_tactic(parser & p); +expr parse_krewrite_tactic(parser & p); +expr parse_xrewrite_tactic(parser & p); expr parse_esimp_tactic(parser & p); expr parse_unfold_tactic(parser & p); expr parse_fold_tactic(parser & p); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 0e167e5ce..92405f845 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -94,10 +94,11 @@ void init_token_table(token_table & t) { {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"{|", 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}, {"begin+", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, + {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"xrewrite", 0}, {"krewrite", 0}, + {"esimp", 0}, {"fold", 0}, {"unfold", 0}, + {"generalize", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0}, + {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"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}, {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0}, {"(macro_def(e).raw())->get_info(); } -expr mk_rewrite_tactic_expr(buffer const & elems) { - lean_assert(std::all_of(elems.begin(), elems.end(), [](expr const & e) { +bool check_tactic_elems(buffer const & elems) { + if (std::all_of(elems.begin(), elems.end(), [](expr const & e) { return is_rewrite_step(e) || is_rewrite_unfold_step(e) || - is_rewrite_reduce_step(e) || is_rewrite_fold_step(e); - })); + is_rewrite_reduce_step(e) || is_rewrite_fold_step(e); })) { + lean_unreachable(); + return false; + } + return true; +} + +expr mk_rewrite_tactic_expr(buffer const & elems) { + lean_assert(check_tactic_elems(elems)); return mk_app(*g_rewrite_tac, mk_expr_list(elems.size(), elems.data())); } +expr mk_krewrite_tactic_expr(buffer const & elems) { + lean_assert(check_tactic_elems(elems)); + return mk_app(*g_krewrite_tac, mk_expr_list(elems.size(), elems.data())); +} + +expr mk_xrewrite_tactic_expr(buffer const & elems) { + lean_assert(check_tactic_elems(elems)); + return mk_app(*g_xrewrite_tac, mk_expr_list(elems.size(), elems.data())); +} + /** \brief make sure hypothesis h occur after hs (if possible). This procedure assumes that all hypotheses in \c hs occur in g, and it has no duplicates. @@ -548,6 +567,7 @@ class rewrite_fn { expr m_expr_loc; // auxiliary expression used for error localization bool m_use_trace; + bool m_keyed; unsigned m_max_iter; buffer> m_lsubst; // auxiliary buffer for pattern matching @@ -902,9 +922,11 @@ class rewrite_fn { } // Given the rewrite step \c e, return a pattern to be used to locate the term to be rewritten. - expr get_pattern(expr const & e) { + expr get_pattern_core(expr const & e) { lean_assert(is_rewrite_step(e)); if (has_rewrite_pattern(e)) { + if (m_keyed) + throw_rewrite_exception("invalid krewrite tactic, keyed-matching does not support user-defined patterns"); return to_meta_idx(get_rewrite_pattern(e)); } else { // Remark: we discard constraints generated producing the pattern. @@ -933,6 +955,20 @@ class rewrite_fn { } } + expr get_pattern(expr const & e) { + expr r = get_pattern_core(e); + if (m_keyed) { + expr const & f = get_app_fn(r); + if (is_constant(f) || is_local(f)) + return f; + else + throw_rewrite_exception("invalid krewrite tactic, " + "left-hand-side of equation must be headed by a constant or local"); + } else { + return r; + } + } + // Set m_esubst and m_lsubst elements to none void reset_subst() { for (optional & l : m_lsubst) @@ -1004,7 +1040,8 @@ class rewrite_fn { return format(); if (!m_failures) { if (m_is_hypothesis) - return line() + format("no subterm in the hypothesis '") + fmt(m_target) + format("' matched the pattern"); + return line() + format("no subterm in the hypothesis '") + + fmt(m_target) + format("' matched the pattern"); else return line() + format("no subterm in the goal matched the pattern"); } @@ -1196,10 +1233,16 @@ class rewrite_fn { return false; // stop search if (closed(t)) { lean_assert(std::all_of(m_esubst.begin(), m_esubst.end(), [&](optional const & e) { return !e; })); - bool assigned = false; - bool r = match(pattern, t, m_lsubst, m_esubst, nullptr, nullptr, &m_mplugin, &assigned); - if (assigned) - reset_subst(); + bool r; + if (m_keyed) { + expr const & f = get_app_fn(t); + r = f == pattern; + } else { + bool assigned = false; + r = match(pattern, t, m_lsubst, m_esubst, nullptr, nullptr, &m_mplugin, &assigned); + if (assigned) + reset_subst(); + } if (r) { if (auto p = unify_target(t, orig_elem, is_goal)) { result = std::make_tuple(t, p->second, p->first); @@ -1424,12 +1467,12 @@ class rewrite_fn { } } - type_checker_ptr mk_matcher_tc() { + type_checker_ptr mk_matcher_tc(bool full) { if (get_rewriter_syntactic(m_ios.get_options())) { // use an everything opaque converter return mk_opaque_type_checker(m_env, m_ngen.mk_child()); } else { - auto aux_pred = mk_not_reducible_pred(m_env); + auto aux_pred = full ? mk_irreducible_pred(m_env) : mk_not_reducible_pred(m_env); return mk_type_checker(m_env, m_ngen.mk_child(), [=](name const & n) { return is_projection(m_env, n) || aux_pred(n); }); @@ -1482,13 +1525,15 @@ class rewrite_fn { } public: - rewrite_fn(environment const & env, io_state const & ios, elaborate_fn const & elab, proof_state const & ps): + rewrite_fn(environment const & env, io_state const & ios, elaborate_fn const & elab, proof_state const & ps, + bool full, bool keyed): m_env(env), m_ios(ios), m_elab(elab), m_ps(ps), m_ngen(ps.get_ngen()), - m_tc(mk_type_checker(m_env, m_ngen.mk_child(), UnfoldQuasireducible)), - m_matcher_tc(mk_matcher_tc()), + m_tc(mk_type_checker(m_env, m_ngen.mk_child(), full ? UnfoldSemireducible : UnfoldQuasireducible)), + m_matcher_tc(mk_matcher_tc(full)), m_relaxed_tc(mk_type_checker(m_env, m_ngen.mk_child())), m_mplugin(m_ios, *m_matcher_tc) { - m_ps = apply_substitution(m_ps); + m_keyed = keyed; + m_ps = apply_substitution(m_ps); goals const & gs = m_ps.get_goals(); lean_assert(gs); update_goal(head(gs)); @@ -1517,17 +1562,29 @@ public: } }; -tactic mk_rewrite_tactic(elaborate_fn const & elab, buffer const & elems) { +tactic mk_rewrite_tactic_core(elaborate_fn const & elab, buffer const & elems, bool full, bool keyed) { return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { goals const & gs = s.get_goals(); if (empty(gs)) { throw_no_goal_if_enabled(s); return proof_state_seq(); } - return rewrite_fn(env, ios, elab, s)(elems); + return rewrite_fn(env, ios, elab, s, full, keyed)(elems); }); } +tactic mk_rewrite_tactic(elaborate_fn const & elab, expr const & e, bool full, bool keyed) { + buffer args; + get_tactic_expr_list_elements(app_arg(e), args, "invalid 'rewrite' tactic, invalid argument"); + for (expr const & arg : args) { + if (!is_rewrite_step(arg) && !is_rewrite_unfold_step(arg) && + !is_rewrite_reduce_step(arg) && !is_rewrite_fold_step(arg)) + throw expr_to_tactic_exception(e, "invalid 'rewrite' tactic, invalid argument"); + } + bool fail_if_metavars = true; + return then(mk_rewrite_tactic_core(elab, args, full, keyed), try_tactic(refl_tactic(elab, fail_if_metavars))); +} + void initialize_rewrite_tactic() { g_rewriter_max_iterations = new name{"rewriter", "max_iter"}; register_unsigned_option(*g_rewriter_max_iterations, LEAN_DEFAULT_REWRITER_MAX_ITERATIONS, @@ -1540,6 +1597,8 @@ void initialize_rewrite_tactic() { "(rewriter tactic) if true tactic will generate a trace for rewrite step failures"); name rewrite_tac_name{"tactic", "rewrite_tac"}; g_rewrite_tac = new expr(Const(rewrite_tac_name)); + g_xrewrite_tac = new expr(Const(name{"tactic", "xrewrite_tac"})); + g_krewrite_tac = new expr(Const(name{"tactic", "krewrite_tac"})); g_rewrite_reduce_name = new name("rewrite_reduce"); g_rewrite_reduce_opcode = new std::string("RWR"); g_rewrite_unfold_name = new name("rewrite_unfold"); @@ -1587,15 +1646,15 @@ void initialize_rewrite_tactic() { }); register_tac(rewrite_tac_name, [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) { - buffer args; - get_tactic_expr_list_elements(app_arg(e), args, "invalid 'rewrite' tactic, invalid argument"); - for (expr const & arg : args) { - if (!is_rewrite_step(arg) && !is_rewrite_unfold_step(arg) && - !is_rewrite_reduce_step(arg) && !is_rewrite_fold_step(arg)) - throw expr_to_tactic_exception(e, "invalid 'rewrite' tactic, invalid argument"); - } - bool fail_if_metavars = true; - return then(mk_rewrite_tactic(elab, args), try_tactic(refl_tactic(elab, fail_if_metavars))); + return mk_rewrite_tactic(elab, e, false, false); + }); + register_tac(name{"tactic", "xrewrite_tac"}, + [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) { + return mk_rewrite_tactic(elab, e, true, false); + }); + register_tac(name{"tactic", "krewrite_tac"}, + [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) { + return mk_rewrite_tactic(elab, e, true, true); }); } @@ -1604,6 +1663,8 @@ void finalize_rewrite_tactic() { delete g_rewriter_syntactic; delete g_rewriter_trace; delete g_rewrite_tac; + delete g_krewrite_tac; + delete g_xrewrite_tac; delete g_rewrite_reduce_name; delete g_rewrite_reduce_opcode; delete g_rewrite_unfold_name; diff --git a/src/library/tactic/rewrite_tactic.h b/src/library/tactic/rewrite_tactic.h index c2e1870bb..95fc5f7c4 100644 --- a/src/library/tactic/rewrite_tactic.h +++ b/src/library/tactic/rewrite_tactic.h @@ -23,6 +23,8 @@ bool is_rewrite_step(expr const & e); /** \brief Create a rewrite tactic expression, where elems was created using \c mk_rewrite_* procedures. */ expr mk_rewrite_tactic_expr(buffer const & elems); +expr mk_xrewrite_tactic_expr(buffer const & elems); +expr mk_krewrite_tactic_expr(buffer const & elems); void initialize_rewrite_tactic(); void finalize_rewrite_tactic(); diff --git a/tests/lean/run/511a.lean b/tests/lean/run/511a.lean new file mode 100644 index 000000000..6c39434fa --- /dev/null +++ b/tests/lean/run/511a.lean @@ -0,0 +1,14 @@ +import data.nat +open nat + +example (a b : nat) (f : nat → nat) (h : f (succ a) = 0) : f (a+1) = 0 := +by rewrite [add_one, h] + +example (a b : nat) (f : nat → nat) (h : f (succ a) = 0) : f (a+1) = 0 := +by xrewrite h + +definition g (a : nat) := a + 1 +definition h (a : nat) := a + +example (a b : nat) (f : nat → nat) (h : f (g (h a)) = 0) : f (a+1) = 0 := +by krewrite h