From 235b8975d29d42b626f9fb2a5652abf843c28814 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 10 Oct 2014 14:37:45 -0700 Subject: [PATCH] feat(kernel/inductive): K-like reduction in the kernel Given (H_1 : a = a), we have that eq.rec H_2 H_1 reduces to H_2 This is not exclusive to equality. It applies to any inductive datatype in Prop, containing only one constructor with zero "arguments" (we say they are nullary). BTW, the restriction to only one constructor is not needed, but it is does not buy much to support multiple nullary constructors since Prop is proof irrelevant. --- src/kernel/inductive/inductive.cpp | 91 ++++++++++++++++++++++++++---- tests/lean/run/kcomp.lean | 25 ++++++++ 2 files changed, 105 insertions(+), 11 deletions(-) create mode 100644 tests/lean/run/kcomp.lean diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index 52ed60e7b3..dc9ab906e4 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -794,10 +794,54 @@ bool inductive_normalizer_extension::supports(name const & feature) const { return feature == *g_inductive_extension; } -optional> inductive_normalizer_extension::operator()(expr const & e, extension_context & ctx) const { +/** \brief Return true if \c e is an introduction rule for an eliminator named \c elim */ +static inductive_env_ext::comp_rule const * is_intro_for(inductive_env_ext const & ext, name const & elim, expr const & e) { + expr const & intro_fn = get_app_fn(e); + if (!is_constant(intro_fn)) + return nullptr; + auto it = ext.m_comp_rules.find(const_name(intro_fn)); + if (it && it->m_elim_name == elim) + return it; + else + return nullptr; +} + +/** \brief If \c d_name is the name of a non-empty inductive datatype, then return the + name of the first introduction rule. Return none otherwise. */ +static optional get_first_intro(environment const & env, name const & d_name) { + inductive_env_ext const & ext = get_extension(env); + if (inductive_decls const * it = ext.m_inductive_info.find(d_name)) { + list const & decls = std::get<2>(*it); + for (auto const & decl : decls) { + if (inductive_decl_name(decl) != d_name) + continue; + auto intros = inductive_decl_intros(decl); + if (intros) + return optional(intro_rule_name(head(intros))); + } + } + return optional(); +} + +static optional mk_nullary_intro(environment const & env, expr const & type, unsigned num_params) { + buffer args; + expr const & d = get_app_args(type, args); + if (!is_constant(d)) + return none_expr(); + name const & d_name = const_name(d); + auto intro_name = get_first_intro(env, d_name); + if (!intro_name) + return none_expr(); + args.shrink(num_params); + return some(mk_app(mk_constant(*intro_name, const_levels(d)), args)); +} + +auto inductive_normalizer_extension::operator()(expr const & e, extension_context & ctx) const + -> optional> { // Reduce terms \c e of the form // elim_k A C e p[A,b] (intro_k_i A b u) - inductive_env_ext const & ext = get_extension(ctx.env()); + environment const & env = ctx.env(); + inductive_env_ext const & ext = get_extension(env); expr const & elim_fn = get_app_fn(e); if (!is_constant(elim_fn)) return none_ecs(); @@ -812,14 +856,37 @@ optional> inductive_normalizer_extension::operator()( auto intro_app_cs = ctx.whnf(elim_args[major_idx]); expr intro_app = intro_app_cs.first; constraint_seq cs = intro_app_cs.second; - expr const & intro_fn = get_app_fn(intro_app); - // Last argument must be a constant and an application of a constant. - if (!is_constant(intro_fn)) - return none_ecs(); - // Check if intro_fn is an introduction rule matching elim_fn - auto it2 = ext.m_comp_rules.find(const_name(intro_fn)); - if (!it2 || it2->m_elim_name != const_name(elim_fn)) - return none_ecs(); + auto it2 = is_intro_for(ext, const_name(elim_fn), intro_app); + if (!it2) { + if (it1->m_K_target) { + // If the inductive type support K-like reduction + // we try to replace the term with associated nullary + // intro rule + auto app_type_cs = ctx.infer_type(intro_app); + expr app_type = app_type_cs.first; + if (has_expr_metavar(app_type)) + return none_ecs(); + auto new_intro_app = mk_nullary_intro(env, app_type, it1->m_num_params); + if (!new_intro_app) + return none_ecs(); + auto new_type_cs = ctx.infer_type(*new_intro_app); + expr new_type = new_type_cs.first; + if (has_expr_metavar(new_type)) + return none_ecs(); + simple_delayed_justification jst([=]() { + return mk_justification("elim/intro global parameters must match", some_expr(e)); + }); + auto dcs = ctx.is_def_eq(app_type, new_type, jst); + if (!dcs.first) + return none_ecs(); + cs += app_type_cs.second + new_type_cs.second + dcs.second; + intro_app = *new_intro_app; + it2 = ext.m_comp_rules.find(const_name(get_app_fn(intro_app))); + } else { + return none_ecs(); + } + } + buffer intro_args; get_app_args(intro_app, intro_args); // Check intro num_args @@ -827,7 +894,9 @@ optional> inductive_normalizer_extension::operator()( return none_ecs(); if (it1->m_num_params > 0) { // Global parameters of elim and intro be definitionally equal - simple_delayed_justification jst([=]() { return mk_justification("elim/intro global parameters must match", some_expr(e)); }); + simple_delayed_justification jst([=]() { + return mk_justification("elim/intro global parameters must match", some_expr(e)); + }); for (unsigned i = 0; i < it1->m_num_params; i++) { auto dcs = ctx.is_def_eq(elim_args[i], intro_args[i], jst); if (!dcs.first) diff --git a/tests/lean/run/kcomp.lean b/tests/lean/run/kcomp.lean new file mode 100644 index 0000000000..12767798a8 --- /dev/null +++ b/tests/lean/run/kcomp.lean @@ -0,0 +1,25 @@ +import logic +set_option pp.notation false +constant A : Type +constants a b : A +constant P : A → Type +constant H₁ : a = a +constant H₂ : P a +constant H₃ : a = b +constant f {A : Type} (a : A) : a = a +eval eq.rec H₂ (f a) +eval eq.rec H₂ H₁ +eval eq.rec H₂ H₃ +eval eq.rec H₂ (eq.refl a) +eval λ (A : Type) (a b : A) (H₁ : a = a) (P : A → Prop) (H₂ : P a) (H₃ : a = a) (c : A), eq.rec (eq.rec H₂ H₁) H₃ +check @eq.rec A a P H₂ a +check λ H : a = a, H₂ +inductive to_type {B : Type} : B → Type := +mk : Π (b : B), to_type b + +definition tst1 : to_type (λ H : a = a, H₂) := to_type.mk (@eq.rec A a P H₂ a) +check to_type.mk(λ H : a = a, H₂) +check to_type.mk(@eq.rec A a P H₂ a) +check to_type.mk(λ H : a = a, H₂) = to_type.mk(@eq.rec A a P H₂ a) +check to_type.mk(eq.rec H₂ H₁) = to_type.mk(H₂) +check to_type.mk(eq.rec H₂ (f a)) = to_type.mk(H₂)