From b86494f0d482d270ea5c04f7bbcf2e28a25233f5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 30 Dec 2016 17:05:24 -0800 Subject: [PATCH] feat(library/tactic): add destruct tactic that is similar to cases, but does not use revert/intro/clear This tactic is useful for building more complex tactics using ematch and cc because it does not invalidate cc_state nor ematch_state. --- library/init/meta/interactive.lean | 3 + library/init/meta/tactic.lean | 5 + src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/destruct_tactic.cpp | 139 +++++++++++++++++++++++++ src/library/tactic/destruct_tactic.h | 12 +++ src/library/tactic/init_module.cpp | 3 + 6 files changed, 163 insertions(+), 1 deletion(-) create mode 100644 src/library/tactic/destruct_tactic.cpp create mode 100644 src/library/tactic/destruct_tactic.h diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 7f1dfd7896..fc5f7da73e 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -230,6 +230,9 @@ do e ← to_expr p, h ← tactic.intro1, cases_core semireducible h ids +meta def destruct (p : qexpr0) : tactic unit := +to_expr p >>= tactic.destruct + meta def generalize (p : qexpr) (x : ident) : tactic unit := do e ← to_expr p, tactic.generalize e x diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 7ad600996f..e2571369ea 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -350,6 +350,8 @@ meta constant induction_core : transparency → expr → name → list name → /- (cases_core m H ns) apply cases_on recursor, names for the new hypotheses are retrieved from ns. H must be a local constant -/ meta constant cases_core : transparency → expr → list name → tactic unit +/- (destruct_core m e) similar to cases tactic, but does not revert/intro/clear hypotheses. -/ +meta constant destruct_core : transparency → expr → tactic unit /- (generalize_core m e n) -/ meta constant generalize_core : transparency → expr → name → tactic unit /- instantiate assigned metavariables in the given expression -/ @@ -713,6 +715,9 @@ cases_core semireducible H [] meta def cases_using : expr → list name → tactic unit := cases_core semireducible +meta def destruct (e : expr) : tactic unit := +destruct_core semireducible e + meta def generalize : expr → name → tactic unit := generalize_core semireducible diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 748d1746e5..ab40d27bd6 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -8,4 +8,4 @@ add_library(tactic OBJECT occurrences.cpp kabstract.cpp tactic_state.cpp hsubstitution.cpp gexpr.cpp elaborate.cpp init_module.cpp simp_result.cpp user_attribute.cpp eval.cpp simp_lemmas.cpp eqn_lemmas.cpp dsimplify.cpp simplify.cpp - vm_monitor.cpp norm_num_tactic.cpp) + vm_monitor.cpp destruct_tactic.cpp norm_num_tactic.cpp) diff --git a/src/library/tactic/destruct_tactic.cpp b/src/library/tactic/destruct_tactic.cpp new file mode 100644 index 0000000000..7879cdbcb2 --- /dev/null +++ b/src/library/tactic/destruct_tactic.cpp @@ -0,0 +1,139 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/instantiate.h" +#include "kernel/inductive/inductive.h" +#include "library/app_builder.h" +#include "library/trace.h" +#include "library/vm/vm_expr.h" +#include "library/tactic/tactic_state.h" + +namespace lean { +tactic_state destruct(transparency_mode md, expr const & e, tactic_state const & s) { + if (!s.goals()) + throw exception("destruct tactic failed, there are no goals to be solved"); + + type_context ctx = mk_type_context_for(s, md); + environment const & env = ctx.env(); + expr target = s.get_main_goal_decl()->get_type(); + level target_lvl = get_level(ctx, target); + + expr e_type = ctx.relaxed_whnf(ctx.infer(e)); + buffer I_args; + expr const & I = get_app_args(e_type, I_args); + if (!is_constant(I) || + !inductive::is_inductive_decl(env, const_name(I)) || + !env.find(name{const_name(I), "cases_on"})) + throw exception("destruct tactic failed, type of given expression is not an inductive datatype"); + + name const & I_name = const_name(I); + levels const I_lvls = const_levels(I); + bool dep_elim = inductive::has_dep_elim(env, I_name); + unsigned nindices = *inductive::get_num_indices(env, I_name); + unsigned nparams = *inductive::get_num_params(env, I_name); + unsigned nminors = *inductive::get_num_intro_rules(env, I_name); + declaration I_decl = env.get(I_name); + declaration cases_on_decl = env.get({I_name, "cases_on"}); + + if (!dep_elim) + throw exception("destruct tactic failed, cases_on recursor does not support dependent elimination"); + + if (I_args.size() != nindices + nparams) + throw exception("destruct tactic failed, ill-formed inductive datatype"); + + /* cases will contain the cases_on application that we will assing to the main goal */ + expr cases = mk_constant(cases_on_decl.get_name(), cons(target_lvl, I_lvls)); + /* add params */ + cases = mk_app(cases, I_args.size() - nindices, I_args.data()); + /* add motive */ + buffer refls; /* refl proof for indices and major */ + { + type_context::tmp_locals locals(ctx); + buffer js; + buffer eqs; + expr I_A = mk_app(I, I_args.size() - nindices, I_args.data()); + expr I_A_type = ctx.infer(I_A); + if (nindices > 0) { + for (unsigned idx = 0; idx < nindices; idx++) { + I_A_type = ctx.relaxed_whnf(I_A_type); + if (!is_pi(I_A_type)) + throw exception("destruct tactic failed, ill-formed inductive datatype"); + expr j = locals.push_local_from_binding(I_A_type); + js.push_back(j); + expr i = I_args[nparams + idx]; + if (ctx.is_def_eq(ctx.infer(j), ctx.infer(i))) { + eqs.push_back(mk_eq(ctx, i, j)); + refls.push_back(mk_eq_refl(ctx, i)); + } else { + eqs.push_back(mk_heq(ctx, i, j)); + refls.push_back(mk_heq_refl(ctx, i)); + } + I_A_type = instantiate(binding_body(I_A_type), j); + } + } + expr motive = target; + expr w = locals.push_local("w", mk_app(I_A, js)); + if (ctx.is_def_eq(ctx.infer(w), e_type)) { + motive = mk_arrow(mk_eq(ctx, e, w), motive); + refls.push_back(mk_eq_refl(ctx, e)); + } else { + motive = mk_arrow(mk_heq(ctx, e, w), motive); + refls.push_back(mk_heq_refl(ctx, e)); + } + unsigned i = eqs.size(); + while (i > 0) { + --i; + motive = mk_arrow(eqs[i], motive); + } + motive = locals.mk_lambda(motive); + cases = mk_app(cases, motive); + } + /* add indices */ + cases = mk_app(cases, nindices, I_args.data() + nparams); + /* add major */ + cases = mk_app(cases, e); + /* add minors */ + expr cases_type = ctx.infer(cases); + buffer new_goals; + for (unsigned i = 0; i < nminors; i++) { + cases_type = ctx.relaxed_whnf(cases_type); + if (!is_pi(cases_type)) + throw exception("destruct tactic failed, ill-formed inductive datatype"); + expr new_type = annotated_head_beta_reduce(binding_domain(cases_type)); + expr new_M = ctx.mk_metavar_decl(ctx.lctx(), new_type); + new_goals.push_back(new_M); + cases = mk_app(cases, new_M); + cases_type = binding_body(cases_type); + } + /* add refl proofs for indices */ + cases = mk_app(cases, refls); + + /* create new tactic state */ + expr g = head(s.goals()); + list gs = tail(s.goals()); + metavar_context mctx = ctx.mctx(); + mctx.assign(g, cases); + return set_mctx_goals(s, mctx, to_list(new_goals.begin(), new_goals.end(), gs)); +} + +vm_obj tactic_destruct_core(vm_obj const & md, vm_obj const & e, vm_obj const & _s) { + tactic_state const & s = to_tactic_state(_s); + try { + if (!s.goals()) return mk_no_goals_exception(s); + tactic_state new_s = destruct(to_transparency_mode(md), to_expr(e), s); + return mk_tactic_success(new_s); + } catch (exception & ex) { + return mk_tactic_exception(ex, s); + } +} + +void initialize_destruct_tactic() { + DECLARE_VM_BUILTIN(name({"tactic", "destruct_core"}), tactic_destruct_core); +} + +void finalize_destruct_tactic() { +} +} diff --git a/src/library/tactic/destruct_tactic.h b/src/library/tactic/destruct_tactic.h new file mode 100644 index 0000000000..abb1027f2e --- /dev/null +++ b/src/library/tactic/destruct_tactic.h @@ -0,0 +1,12 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once + +namespace lean { +void initialize_destruct_tactic(); +void finalize_destruct_tactic(); +} diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 772dab1d42..fd8f979a7f 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -34,6 +34,7 @@ Author: Leonardo de Moura #include "library/tactic/simplify.h" #include "library/tactic/vm_monitor.h" #include "library/tactic/norm_num_tactic.h" +#include "library/tactic/destruct_tactic.h" #include "library/tactic/backward/init_module.h" #include "library/tactic/smt/init_module.h" @@ -70,10 +71,12 @@ void initialize_tactic_module() { initialize_dsimplify(); initialize_norm_num_tactic(); initialize_vm_monitor(); + initialize_destruct_tactic(); initialize_smt_module(); } void finalize_tactic_module() { finalize_smt_module(); + finalize_destruct_tactic(); finalize_vm_monitor(); finalize_norm_num_tactic(); finalize_dsimplify();