From 0e099b5fd8111e19673884e431cc22c64afbd93a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 6 Jun 2015 20:30:14 -0700 Subject: [PATCH] feat(library/tactic/rewrite_tactic): apply beta&eta reduction before rewriting steps, add option 'rewrite.beta_eta' (default true) to control new feature. --- src/kernel/instantiate.cpp | 22 ----------- src/kernel/instantiate.h | 1 - src/library/normalize.cpp | 38 +++++++++++++++++++ src/library/normalize.h | 2 + src/library/tactic/rewrite_tactic.cpp | 27 ++++++++++++- src/library/tactic/tactic.cpp | 1 + src/tests/kernel/instantiate.cpp | 1 - .../finset_induction_bug.lean.expected.out | 2 +- 8 files changed, 67 insertions(+), 27 deletions(-) diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index 3991aefec..a51cbcba7 100644 --- a/src/kernel/instantiate.cpp +++ b/src/kernel/instantiate.cpp @@ -121,28 +121,6 @@ expr head_beta_reduce(expr const & t) { } } -expr beta_reduce(expr t) { - bool reduced = false; - auto f = [&](expr const & m, unsigned) -> optional { - if (is_head_beta(m)) { - reduced = true; - return some_expr(head_beta_reduce(m)); - } else if (is_local(m) || is_metavar(m)) { - return some_expr(m); // do not simplify local constants and metavariables types. - } else { - return none_expr(); - } - }; - while (true) { - reduced = false; - expr new_t = replace(t, f); - if (!reduced) - return new_t; - else - t = new_t; - } -} - expr instantiate_univ_params(expr const & e, level_param_names const & ps, levels const & ls) { if (!has_param_univ(e)) return e; diff --git a/src/kernel/instantiate.h b/src/kernel/instantiate.h index aa4f7e8cf..6047f69bc 100644 --- a/src/kernel/instantiate.h +++ b/src/kernel/instantiate.h @@ -24,7 +24,6 @@ expr instantiate_rev(expr const & e, unsigned n, expr const * s); expr apply_beta(expr f, unsigned num_args, expr const * args); bool is_head_beta(expr const & t); expr head_beta_reduce(expr const & t); -expr beta_reduce(expr t); /** \brief Instantiate the universe level parameters \c ps occurring in \c e with the levels \c ls. \pre length(ps) == length(ls) diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp index 7fdc58977..82c2cc8f7 100644 --- a/src/library/normalize.cpp +++ b/src/library/normalize.cpp @@ -7,11 +7,13 @@ Author: Leonardo de Moura #include #include "util/interrupt.h" #include "util/name_generator.h" +#include "kernel/replace_fn.h" #include "kernel/type_checker.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" #include "kernel/free_vars.h" #include "kernel/inductive/inductive.h" +#include "library/replace_visitor.h" #include "library/reducible.h" #include "library/util.h" #include "library/scoped_ext.h" @@ -186,6 +188,42 @@ expr try_eta(expr const & e) { } } +template +class eta_beta_reduce_fn : public replace_visitor { +public: + virtual expr visit_app(expr const & e) { + expr e1 = replace_visitor::visit_app(e); + if (Beta && is_head_beta(e1)) { + return visit(head_beta_reduce(e1)); + } else { + return e1; + } + } + + virtual expr visit_lambda(expr const & e) { + expr e1 = replace_visitor::visit_lambda(e); + if (Eta) { + while (true) { + expr e2 = try_eta(e1); + if (is_eqp(e1, e2)) + return e1; + else + e1 = e2; + } + } else { + return e1; + } + } +}; + +expr beta_reduce(expr t) { + return eta_beta_reduce_fn()(t); +} + +expr beta_eta_reduce(expr t) { + return eta_beta_reduce_fn()(t); +} + class normalize_fn { type_checker & m_tc; name_generator m_ngen; diff --git a/src/library/normalize.h b/src/library/normalize.h index cd3f25a46..b428df3fb 100644 --- a/src/library/normalize.h +++ b/src/library/normalize.h @@ -61,6 +61,8 @@ environment erase_constructor_hint(environment const & env, name const & n, bool optional has_constructor_hint(environment const & env, name const & d); expr try_eta(expr const & e); +expr beta_reduce(expr t); +expr beta_eta_reduce(expr t); void initialize_normalize(); void finalize_normalize(); diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index d48edd45a..7f2e35dff 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -52,10 +52,16 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_REWRITER_TRACE true #endif +#ifndef LEAN_DEFAULT_REWRITER_BETA_ETA +#define LEAN_DEFAULT_REWRITER_BETA_ETA true +#endif + + namespace lean { static name * g_rewriter_max_iterations = nullptr; static name * g_rewriter_syntactic = nullptr; static name * g_rewriter_trace = nullptr; +static name * g_rewriter_beta_eta = nullptr; unsigned get_rewriter_max_iterations(options const & opts) { return opts.get_unsigned(*g_rewriter_max_iterations, LEAN_DEFAULT_REWRITER_MAX_ITERATIONS); @@ -69,6 +75,10 @@ bool get_rewriter_trace(options const & opts) { return opts.get_bool(*g_rewriter_trace, LEAN_DEFAULT_REWRITER_TRACE); } +bool get_rewriter_beta_eta(options const & opts) { + return opts.get_bool(*g_rewriter_beta_eta, LEAN_DEFAULT_REWRITER_BETA_ETA); +} + class unfold_info { list m_names; location m_location; @@ -568,6 +578,7 @@ class rewrite_fn { bool m_use_trace; bool m_keyed; unsigned m_max_iter; + bool m_beta_eta; buffer> m_lsubst; // auxiliary buffer for pattern matching buffer> m_esubst; // auxiliary buffer for pattern matching @@ -1271,9 +1282,16 @@ class rewrite_fn { lean::check_term(m_env, m_g.abstract(H)); } + expr apply_beta_eta(expr const & e) { + if (m_beta_eta) + return beta_eta_reduce(e); + else + return e; + } + bool process_rewrite_hypothesis(expr const & hyp, expr const & orig_elem, expr const & pattern, occurrence const & occ) { add_target(hyp, true); - expr Pa = mlocal_type(hyp); + expr Pa = apply_beta_eta(mlocal_type(hyp)); bool is_goal = false; if (auto it = find_target(Pa, pattern, orig_elem, is_goal)) { expr a, Heq, b; // Heq is a proof of a = b @@ -1326,7 +1344,7 @@ class rewrite_fn { } bool process_rewrite_goal(expr const & orig_elem, expr const & pattern, occurrence const & occ) { - expr Pa = m_g.get_type(); + expr Pa = apply_beta_eta(m_g.get_type()); add_target(Pa, false); bool is_goal = true; if (auto it = find_target(Pa, pattern, orig_elem, is_goal)) { @@ -1539,6 +1557,7 @@ public: m_subst = m_ps.get_subst(); m_max_iter = get_rewriter_max_iterations(ios.get_options()); m_use_trace = get_rewriter_trace(ios.get_options()); + m_beta_eta = get_rewriter_beta_eta(ios.get_options()); } proof_state_seq operator()(buffer const & elems) { @@ -1594,6 +1613,10 @@ void initialize_rewrite_tactic() { g_rewriter_trace = new name{"rewriter", "trace"}; register_bool_option(*g_rewriter_trace, LEAN_DEFAULT_REWRITER_TRACE, "(rewriter tactic) if true tactic will generate a trace for rewrite step failures"); + g_rewriter_beta_eta = new name{"rewriter", "beta_eta"}; + register_bool_option(*g_rewriter_beta_eta, LEAN_DEFAULT_REWRITER_BETA_ETA, + "(rewriter tactic) apply beta and eta reduction before rewrite steps"); + 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"})); diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 3812adc44..ace9ce2b7 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -16,6 +16,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "kernel/for_each_fn.h" #include "kernel/replace_fn.h" +#include "library/normalize.h" #include "library/kernel_bindings.h" #include "library/tactic/tactic.h" #include "library/io_state_stream.h" diff --git a/src/tests/kernel/instantiate.cpp b/src/tests/kernel/instantiate.cpp index aebbf5400..71ed92415 100644 --- a/src/tests/kernel/instantiate.cpp +++ b/src/tests/kernel/instantiate.cpp @@ -32,7 +32,6 @@ static void tst1() { expr F3 = mk_app(Fun(x, mk_app(f, mk_app(Fun(y, y), x), x)), a); lean_assert(is_head_beta(F3)); lean_assert(head_beta_reduce(F3) == mk_app(f, mk_app(Fun(y, y), a), a)); - lean_assert(beta_reduce(F3) == mk_app(f, a, a)); } int main() { diff --git a/tests/lean/finset_induction_bug.lean.expected.out b/tests/lean/finset_induction_bug.lean.expected.out index e352f339c..641094896 100644 --- a/tests/lean/finset_induction_bug.lean.expected.out +++ b/tests/lean/finset_induction_bug.lean.expected.out @@ -1,5 +1,5 @@ finset_induction_bug.lean:30:23: error:invalid 'rewrite' tactic, step produced type incorrect term, details: type mismatch at application - @subtype.tag (list A) (λ (l : list A), @nodup A l) x nodup_al' + @subtype.tag (list A) (@nodup A) x nodup_al' term nodup_al' has type