michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/tactic/inversion_tactic): add 'cases_on' step to inversion_tactic

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-27 00:06:26 -08:00
parent ebd320a6b3
commit 5fff3113a9
4 changed files with 237 additions and 104 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/kernel/inductive/inductive.h
View file

@ -68,6 +68,16 @@ optional<name> is_elim_rule(environment const & env, name const & n);
optional<unsigned> get_elim_major_idx(environment const & env, name const & n);
bool is_elim_meta_app(type_checker & tc, expr const & e);
/** \brief Return the number of parameters in the given inductive datatype.
If \c n is not an inductive datatype in \c env, then return none.
*/
inline optional<unsigned> get_num_params(environment const & env, name const & n) {
if (auto ds = is_inductive_decl(env, n))
return optional<unsigned>(std::get<1>(*ds));
else
return optional<unsigned>();
}
/** \brief Return the number of indices in the given inductive datatype.
If \c n is not an inductive datatype in \c env, then return none.
*/

15
src/library/tactic/goal.cpp
View file

@ -144,9 +144,7 @@ void goal::get_hyps(buffer<expr> & r) const {
get_app_args(m_meta, r);
}
name goal::get_unused_name(name const & prefix, unsigned & idx) const {
buffer<expr> locals;
get_app_rev_args(get_meta(), locals);
name get_unused_name(name const & prefix, unsigned & idx, buffer<expr> const & locals) {
while (true) {
bool used = false;
name curr = prefix.append_after(idx);
@ -162,6 +160,17 @@ name goal::get_unused_name(name const & prefix, unsigned & idx) const {
}
}
name get_unused_name(name const & prefix, buffer<expr> const & locals) {
unsigned idx = 1;
return get_unused_name(prefix, idx, locals);
}
name goal::get_unused_name(name const & prefix, unsigned & idx) const {
buffer<expr> locals;
get_app_rev_args(get_meta(), locals);
return ::lean::get_unused_name(prefix, idx, locals);
}
name goal::get_unused_name(name const & prefix) const {
unsigned idx = 1;
return get_unused_name(prefix, idx);

3
src/library/tactic/goal.h
View file

@ -97,6 +97,9 @@ public:
format pp(formatter const & fmt) const;
};
name get_unused_name(name const & prefix, unsigned & idx, buffer<expr> const & locals);
name get_unused_name(name const & prefix, buffer<expr> const & locals);
io_state_stream const & operator<<(io_state_stream const & out, goal const & g);
UDATA_DEFS(goal)

313
src/library/tactic/inversion_tactic.cpp
View file

@ -13,36 +13,207 @@ Author: Leonardo de Moura
#include "library/tactic/expr_to_tactic.h"
namespace lean {
static bool is_inversion_applicable(environment const & env, expr const & t) {
expr const & fn = get_app_fn(t);
if (!is_constant(fn))
return false;
if (!inductive::is_inductive_decl(env, const_name(fn)))
return false;
if (!env.find(name{const_name(fn), "cases_on"}) ||
!env.find(name("eq")) || !env.find(name("heq")))
return false;
return true;
}
class inversion_tac {
environment const & m_env;
io_state const & m_ios;
proof_state const & m_ps;
name_generator m_ngen;
substitution m_subst;
std::unique_ptr<type_checker> m_tc;
static pair<expr, expr> mk_eq(type_checker & tc, expr const & lhs, expr const & rhs) {
expr lhs_type = tc.infer(lhs).first;
expr rhs_type = tc.infer(rhs).first;
constraint_seq cs;
if (tc.is_def_eq(lhs_type, rhs_type, justification(), cs) && !cs) {
level l = sort_level(tc.ensure_type(lhs_type).first);
return mk_pair(mk_app(mk_constant("eq", to_list(l)), lhs_type, lhs, rhs),
mk_app(mk_constant({"eq", "refl"}, to_list(l)), rhs_type, rhs));
} else {
level l = sort_level(tc.ensure_type(lhs_type).first);
return mk_pair(mk_app(mk_constant("heq", to_list(l)), lhs_type, lhs, rhs_type, rhs),
mk_app(mk_constant({"heq", "refl"}, to_list(l)), rhs_type, rhs));
unsigned m_nparams;
unsigned m_nindices;
unsigned m_nminors;
declaration m_I_decl;
declaration m_cases_on_decl;
void init_inductive_info(name const & n) {
m_nindices = *inductive::get_num_indices(m_env, n);
m_nparams = *inductive::get_num_params(m_env, n);
m_nminors = *inductive::get_num_minor_premises(m_env, n);
m_I_decl = m_env.get(n);
m_cases_on_decl = m_env.get({n, "cases_on"});
}
}
tactic generalize_indices_tactic(name const & n) {
auto fn = [=](environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
goals const & gs = s.get_goals();
bool is_inversion_applicable(expr const & t) {
buffer<expr> args;
expr const & fn = get_app_args(t, args);
if (!is_constant(fn))
return false;
if (!inductive::is_inductive_decl(m_env, const_name(fn)))
return false;
if (!m_env.find(name{const_name(fn), "cases_on"}) ||
!m_env.find(name("eq")) || !m_env.find(name("heq")))
return false;
init_inductive_info(const_name(fn));
if (args.size() != m_nindices + m_nparams)
return false;
return true;
}
pair<expr, expr> mk_eq(expr const & lhs, expr const & rhs) {
expr lhs_type = m_tc->infer(lhs).first;
expr rhs_type = m_tc->infer(rhs).first;
level l = sort_level(m_tc->ensure_type(lhs_type).first);
constraint_seq cs;
if (m_tc->is_def_eq(lhs_type, rhs_type, justification(), cs) && !cs) {
return mk_pair(mk_app(mk_constant("eq", to_list(l)), lhs_type, lhs, rhs),
mk_app(mk_constant({"eq", "refl"}, to_list(l)), rhs_type, rhs));
} else {
return mk_pair(mk_app(mk_constant("heq", to_list(l)), lhs_type, lhs, rhs_type, rhs),
mk_app(mk_constant({"heq", "refl"}, to_list(l)), rhs_type, rhs));
}
}
goal generalize_indices(goal const & g, expr const & h, expr const & h_type) {
buffer<expr> hyps;
g.get_hyps(hyps);
expr m = g.get_meta();
expr m_type = g.get_type();
name h_new_name = g.get_unused_name(local_pp_name(h));
buffer<expr> I_args;
expr const & I = get_app_args(h_type, I_args);
if (m_nindices > 0) {
expr h_new_type = mk_app(I, I_args.size() - m_nindices, I_args.data());
expr d = m_tc->whnf(m_tc->infer(h_new_type).first).first;
unsigned eq_idx = 1;
name eq_prefix("H");
buffer<expr> ts;
buffer<expr> eqs;
buffer<expr> refls;
name t_prefix("t");
unsigned nidx = 1;
for (unsigned i = I_args.size() - m_nindices; i < I_args.size(); i++) {
expr t_type = binding_domain(d);
expr t = mk_local(m_ngen.next(), g.get_unused_name(t_prefix, nidx), t_type, binder_info());
expr const & index = I_args[i];
pair<expr, expr> p = mk_eq(t, index);
expr new_eq = p.first;
expr new_refl = p.second;
eqs.push_back(mk_local(m_ngen.next(), g.get_unused_name(eq_prefix, eq_idx), new_eq, binder_info()));
refls.push_back(new_refl);
h_new_type = mk_app(h_new_type, t);
hyps.push_back(t);
ts.push_back(t);
d = instantiate(binding_body(d), t);
}
expr h_new = mk_local(m_ngen.next(), h_new_name, h_new_type, local_info(h));
hyps.push_back(h_new);
expr new_type = Pi(eqs, g.get_type());
expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps);
goal new_g(new_meta, new_type);
expr val = g.abstract(mk_app(mk_app(mk_app(Fun(ts, Fun(h_new, new_meta)), m_nindices, I_args.end() - m_nindices), h), refls));
m_subst.assign(g.get_name(), val);
return new_g;
} else {
expr h_new = mk_local(m_ngen.next(), h_new_name, h_type, local_info(h));
hyps.push_back(h_new);
expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, g.get_type())), hyps);
goal new_g(new_meta, g.get_type());
expr val = g.abstract(mk_app(new_meta, h));
m_subst.assign(g.get_name(), val);
return new_g;
}
}
list<goal> apply_cases_on(goal const & g) {
buffer<expr> hyps;
g.get_hyps(hyps);
expr const & h = hyps.back();
expr const & h_type = mlocal_type(h);
buffer<expr> I_args;
expr const & I = get_app_args(h_type, I_args);
expr g_type = g.get_type();
expr cases_on;
if (length(m_cases_on_decl.get_univ_params()) != length(m_I_decl.get_univ_params())) {
level g_lvl = sort_level(m_tc->ensure_type(g_type).first);
cases_on = mk_constant({const_name(I), "cases_on"}, cons(g_lvl, const_levels(I)));
} else {
cases_on = mk_constant({const_name(I), "cases_on"}, const_levels(I));
}
// add params
cases_on = mk_app(cases_on, m_nparams, I_args.data());
// add type former
expr type_former = Fun(m_nindices, I_args.end() - m_nindices, g_type);
cases_on = mk_app(cases_on, type_former);
// add indices
cases_on = mk_app(cases_on, m_nindices, I_args.end() - m_nindices);
// add h
cases_on = mk_app(cases_on, h);
buffer<expr> new_hyps;
new_hyps.append(hyps.size() - m_nindices - 1, hyps.data());
// add a subgoal for each minor premise of cases_on
expr cases_on_type = m_tc->whnf(m_tc->infer(cases_on).first).first;
buffer<goal> new_goals;
for (unsigned i = 0; i < m_nminors; i++) {
expr new_type = binding_domain(cases_on_type);
expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_hyps, new_type)), new_hyps);
goal new_g(new_meta, new_type);
new_goals.push_back(new_g);
cases_on = mk_app(cases_on, new_meta);
cases_on_type = m_tc->whnf(binding_body(cases_on_type)).first; // the minor premises do not depend on each other
}
expr val = g.abstract(cases_on);
m_subst.assign(g.get_name(), val);
return to_list(new_goals.begin(), new_goals.end());
}
// Store in \c r the number of arguments for each cases_on minor.
void get_minors_nargs(buffer<unsigned> & r) {
expr cases_on_type = m_cases_on_decl.get_type();
for (unsigned i = 0; i < m_nparams + 1 + m_nindices + 1; i++)
cases_on_type = binding_body(cases_on_type);
for (unsigned i = 0; i < m_nminors; i++) {
expr minor_type = binding_domain(cases_on_type);
unsigned nargs = 0;
while (is_pi(minor_type)) {
nargs++;
minor_type = binding_body(minor_type);
}
r.push_back(nargs);
cases_on_type = binding_body(cases_on_type);
}
}
list<goal> intros_minors_args(list<goal> gs) {
buffer<unsigned> minors_nargs;
get_minors_nargs(minors_nargs);
lean_assert(length(gs) == minors_nargs.size());
buffer<goal> new_gs;
for (unsigned i = 0; i < minors_nargs.size(); i++) {
goal const & g = head(gs);
unsigned nargs = minors_nargs[i];
buffer<expr> hyps;
g.get_hyps(hyps);
buffer<expr> new_hyps;
new_hyps.append(hyps);
expr g_type = g.get_type();
for (unsigned i = 0; i < nargs; i++) {
expr type = binding_domain(g_type);
expr new_h = mk_local(m_ngen.next(), get_unused_name(binding_name(g_type), hyps), type, binder_info());
new_hyps.push_back(new_h);
g_type = instantiate(binding_body(g_type), new_h);
}
g_type = head_beta_reduce(g_type);
expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_hyps, g_type)), new_hyps);
goal new_g(new_meta, g_type);
new_gs.push_back(new_g);
expr val = g.abstract(Fun(nargs, new_hyps.end() - nargs, new_meta));
m_subst.assign(g.get_name(), val);
gs = tail(gs);
}
return to_list(new_gs.begin(), new_gs.end());
}
public:
inversion_tac(environment const & env, io_state const & ios, proof_state const & ps):
m_env(env), m_ios(ios), m_ps(ps),
m_ngen(m_ps.get_ngen()),
m_tc(mk_type_checker(m_env, m_ngen.mk_child(), m_ps.relax_main_opaque())) {
}
optional<proof_state> execute(name const & n) {
goals const & gs = m_ps.get_goals();
if (empty(gs))
return none_proof_state();
goal g = head(gs);
@ -51,83 +222,23 @@ tactic generalize_indices_tactic(name const & n) {
if (!p)
return none_proof_state();
expr const & h = p->first;
name_generator ngen = s.get_ngen();
auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
expr h_type = tc->whnf(mlocal_type(h)).first;
if (!is_inversion_applicable(env, h_type))
expr h_type = m_tc->whnf(mlocal_type(h)).first;
if (!is_inversion_applicable(h_type))
return none_proof_state();
buffer<expr> hyps;
g.get_hyps(hyps);
expr m = g.get_meta();
expr m_type = g.get_type();
auto new_subst = s.get_subst();
name h_new_name = g.get_unused_name(local_pp_name(h));
buffer<expr> I_args;
expr const & I = get_app_args(h_type, I_args);
// Set 1. generalize indices
unsigned nindices = *inductive::get_num_indices(env, const_name(I));
if (nindices > 0) {
expr h_new_type = mk_app(I, I_args.size() - nindices, I_args.data());
expr d = tc->whnf(tc->infer(h_new_type).first).first;
unsigned eq_idx = 1;
name eq_prefix("H");
buffer<expr> ts;
buffer<expr> eqs;
buffer<expr> refls;
for (unsigned i = I_args.size() - nindices; i < I_args.size(); i++) {
expr t_type = binding_domain(d);
expr t = mk_local(ngen.next(), g.get_unused_name(binding_name(d)), t_type, binder_info());
expr const & index = I_args[i];
pair<expr, expr> p = mk_eq(*tc, t, index);
expr new_eq = p.first;
expr new_refl = p.second;
eqs.push_back(mk_local(ngen.next(), g.get_unused_name(eq_prefix, eq_idx), new_eq, binder_info()));
refls.push_back(new_refl);
h_new_type = mk_app(h_new_type, t);
hyps.push_back(t);
ts.push_back(t);
d = instantiate(binding_body(d), t);
}
expr h_new = mk_local(ngen.next(), h_new_name, h_new_type, local_info(h));
hyps.push_back(h_new);
expr new_type = Pi(eqs, g.get_type());
expr new_meta = mk_app(mk_metavar(ngen.next(), Pi(hyps, new_type)), hyps);
goal new_g(new_meta, new_type);
expr val = g.abstract(mk_app(mk_app(mk_app(Fun(ts, Fun(h_new, new_meta)), nindices, I_args.end() - nindices), h), refls));
new_subst.assign(g.get_name(), val);
proof_state new_s(s, goals(new_g, tail_gs), new_subst, ngen);
return some_proof_state(new_s);
} else {
expr h_new = mk_local(ngen.next(), h_new_name, h_type, local_info(h));
hyps.push_back(h_new);
expr new_meta = mk_app(mk_metavar(ngen.next(), Pi(hyps, g.get_type())), hyps);
goal new_g(new_meta, g.get_type());
expr val = g.abstract(mk_app(new_meta, h));
new_subst.assign(g.get_name(), val);
proof_state new_s(s, goals(new_g, tail_gs), new_subst, ngen);
return some_proof_state(new_s);
}
};
return tactic01(fn);
}
tactic cases_on_tactic() {
// TODO(Leo)
return id_tactic();
}
tactic inversion_eqs_tactic() {
// TODO(Leo)
return id_tactic();
}
tactic inversion_clear_tactic() {
// TODO(Leo)
return id_tactic();
}
goal g1 = generalize_indices(g, h, h_type);
list<goal> g2s = apply_cases_on(g1);
list<goal> g3s = intros_minors_args(g2s);
proof_state new_s(m_ps, append(g3s, tail_gs), m_subst, m_ngen);
return some_proof_state(new_s);
}
};
tactic inversion_tactic(name const & n) {
return generalize_indices_tactic(n) << cases_on_tactic() << inversion_eqs_tactic() << inversion_clear_tactic();
auto fn = [=](environment const & env, io_state const & ios, proof_state const & ps) -> optional<proof_state> {
inversion_tac tac(env, ios, ps);
return tac.execute(n);
};
return tactic01(fn);
}
void initialize_inversion_tactic() {