max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/tactic): add destruct tactic that is similar to cases, but does not use revert/intro/clear

Browse source 
This tactic is useful for building more complex tactics using ematch and
cc because it does not invalidate cc_state nor ematch_state.
This commit is contained in:
Leonardo de Moura 2016-12-30 17:05:24 -08:00
parent 9c069a3eda
commit b86494f0d4
6 changed files with 163 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/init/meta/interactive.lean
View file

@ -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

5
library/init/meta/tactic.lean
View file

@ -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

2
src/library/tactic/CMakeLists.txt
View file

@ -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)

139
src/library/tactic/destruct_tactic.cpp Normal file
View file

@ -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<expr> 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<expr> refls; /* refl proof for indices and major */
{
type_context::tmp_locals locals(ctx);
buffer<expr> js;
buffer<expr> 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<expr> 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<expr> 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() {
}
}

12
src/library/tactic/destruct_tactic.h Normal file
View file

@ -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();
}

3
src/library/tactic/init_module.cpp
View file

@ -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();