From 1e6550eda62cff692df68c5d3d849b6b478014a0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 30 Jun 2015 10:42:26 -0700 Subject: [PATCH] feat(kernel/default_converter): take into account the 'theorem' annotations in the converability checker The idea is that we should seldon need to unfold theorems. The convertability checker should use that. When the convertability checker was implemented, theorems were opaque in Lean. So, this hint was not needed. This modification is another workaround for the performance problem with the migrate command at library/data/real/division.lean. This solution is better than applying proof irrelevance eagerly because it also addresses similar problems in the HoTT library which does not support proof irrelevance. This commit also enables the conv_opt for all theorems. --- src/kernel/declaration.cpp | 4 ++-- src/kernel/default_converter.cpp | 35 ++++++++------------------------ 2 files changed, 11 insertions(+), 28 deletions(-) diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index 397b336dd..742190036 100644 --- a/src/kernel/declaration.cpp +++ b/src/kernel/declaration.cpp @@ -85,10 +85,10 @@ declaration mk_definition(environment const & env, name const & n, level_param_n } declaration mk_theorem(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v) { unsigned w = get_max_weight(env, v); - return declaration(new declaration::cell(n, params, t, true, v, w+1, false)); + return declaration(new declaration::cell(n, params, t, true, v, w+1, true)); } declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, unsigned weight) { - return declaration(new declaration::cell(n, params, t, true, v, weight, false)); + return declaration(new declaration::cell(n, params, t, true, v, weight, true)); } declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) { return declaration(new declaration::cell(n, params, t, true)); diff --git a/src/kernel/default_converter.cpp b/src/kernel/default_converter.cpp index 91b950b58..9ce58ba69 100644 --- a/src/kernel/default_converter.cpp +++ b/src/kernel/default_converter.cpp @@ -488,12 +488,15 @@ auto default_converter::lazy_delta_reduction_step(expr & t_n, expr & s_n, constr t_n = whnf_core(unfold_names(t_n, 0)); } else if (!d_t && d_s) { s_n = whnf_core(unfold_names(s_n, 0)); - } else if (d_t->get_weight() > d_s->get_weight()) { + } else if (!d_t->is_theorem() && d_s->is_theorem()) { + t_n = whnf_core(unfold_names(t_n, d_t->get_weight())); + } else if (!d_s->is_theorem() && d_t->is_theorem()) { + s_n = whnf_core(unfold_names(s_n, d_s->get_weight())); + } else if (!d_t->is_theorem() && d_t->get_weight() > d_s->get_weight()) { t_n = whnf_core(unfold_names(t_n, d_s->get_weight() + 1)); - } else if (d_t->get_weight() < d_s->get_weight()) { + } else if (!d_s->is_theorem() && d_t->get_weight() < d_s->get_weight()) { s_n = whnf_core(unfold_names(s_n, d_t->get_weight() + 1)); } else { - lean_assert(d_t && d_s && d_t->get_weight() == d_s->get_weight()); if (is_app(t_n) && is_app(s_n) && is_eqp(*d_t, *d_s)) { // If t_n and s_n are both applications of the same (non-opaque) definition, if (has_expr_metavar(t_n) || has_expr_metavar(s_n)) { @@ -587,21 +590,6 @@ bool default_converter::postpone_is_def_eq(expr const & t, expr const & s) { return false; } -/** \brief Return true if we should try proof irrelevance eagerly. - \remark: We do it whenever t and s do not contain metavariables and one of them is a theorem application. -*/ -static bool try_eager_proof_irrel(environment const & env, expr const & t, expr const & s) { - if (!env.prop_proof_irrel()) - return false; - if (has_expr_metavar(t) || has_expr_metavar(s)) - return false; - expr const & f_t = get_app_fn(t); - if (is_constant(f_t) && env.get(const_name(f_t)).is_theorem()) - return true; - expr const & f_s = get_app_fn(s); - return is_constant(f_s) && env.get(const_name(f_s)).is_theorem(); -} - pair default_converter::is_def_eq_core(expr const & t, expr const & s) { check_system("is_definitionally_equal"); constraint_seq cs; @@ -613,11 +601,6 @@ pair default_converter::is_def_eq_core(expr const & t, exp expr t_n = whnf_core(t); expr s_n = whnf_core(s); - constraint_seq pi_cs_1; - bool eager_proof_irrel = try_eager_proof_irrel(m_env, t, s); - if (eager_proof_irrel && is_def_eq_proof_irrel(t, s, pi_cs_1)) - return to_bcs(true, pi_cs_1); - if (!is_eqp(t_n, t) || !is_eqp(s_n, s)) { r = quick_is_def_eq(t_n, s_n, cs); if (r != l_undef) return to_bcs(r == l_true, cs); @@ -642,9 +625,9 @@ pair default_converter::is_def_eq_core(expr const & t, exp if (try_eta_expansion(t_n, s_n, cs)) return to_bcs(true, cs); - constraint_seq pi_cs_2; - if (!eager_proof_irrel && is_def_eq_proof_irrel(t, s, pi_cs_2)) - return to_bcs(true, pi_cs_2); + constraint_seq pi_cs; + if (is_def_eq_proof_irrel(t, s, pi_cs)) + return to_bcs(true, pi_cs); if (is_stuck(t_n) || is_stuck(s_n) || postpone) { cs += constraint_seq(mk_eq_cnstr(t_n, s_n, m_jst->get()));