refactor(library/tactic/induction_tactic,library/tactic/cases_tactic): replace name_map<name> with substitutions at induction_tactic
This commit also removes dead code from cases_tactic
This commit is contained in:
Leonardo de Moura
parent
206bf613d5
commit
1a675d69fc
5 changed files with 64 additions and 165 deletions
|
|
@ -578,7 +578,7 @@ struct elim_match_fn {
|
|||
lean_assert(is_inductive_app(x_type));
|
||||
name I_name = const_name(get_app_fn(x_type));
|
||||
unsigned I_nparams = get_inductive_num_params(I_name);
|
||||
xintros_list ilist;
|
||||
intros_list ilist;
|
||||
substitutions_list slist;
|
||||
list<expr> new_goals;
|
||||
list<name> new_goal_cnames;
|
||||
|
|
|
|||
|
|
@ -237,93 +237,46 @@ struct cases_tactic_fn {
|
|||
return tmp.pp_goal(mvar);
|
||||
}
|
||||
|
||||
list<expr> elim_aux_indices(list<expr> const & goals, buffer<name> const & aux_indices_H, renaming_list & rlist) {
|
||||
lean_assert(length(goals) == length(rlist));
|
||||
list<expr> elim_aux_indices(list<expr> const & goals, buffer<name> const & aux_indices_H, substitutions_list & slist) {
|
||||
lean_assert(!slist || length(goals) == length(slist));
|
||||
buffer<expr> new_goals;
|
||||
buffer<name_map<name>> new_rlist;
|
||||
buffer<substitutions> new_slist;
|
||||
list<expr> it1 = goals;
|
||||
list<name_map<name>> it2 = rlist;
|
||||
substitutions_list it2 = slist;
|
||||
while (it1 && it2) {
|
||||
expr mvar = head(it1);
|
||||
name_map<name> rmap = head(rlist);
|
||||
expr mvar = head(it1);
|
||||
substitutions substs = head(it2);
|
||||
name_set removed;
|
||||
lean_assert(aux_indices_H.size() > 1);
|
||||
unsigned i = aux_indices_H.size() - 1; /* last element is the auxiliary major premise */
|
||||
while (i > 0) {
|
||||
--i;
|
||||
name idx_name = aux_indices_H[i];
|
||||
if (auto ridx_name = rmap.find(idx_name)) {
|
||||
idx_name = *ridx_name;
|
||||
rmap.erase(idx_name);
|
||||
removed.insert(idx_name);
|
||||
removed.insert(idx_name);
|
||||
if (auto ridx = substs.find(idx_name)) {
|
||||
lean_assert(is_local(*ridx));
|
||||
name new_name = mlocal_name(*ridx);
|
||||
substs.erase(idx_name);
|
||||
idx_name = new_name;
|
||||
}
|
||||
expr H_idx = m_mctx.get_hypothesis_of(mvar, idx_name)->mk_ref();
|
||||
mvar = clear(m_mctx, mvar, H_idx);
|
||||
}
|
||||
name_map<name> new_rmap;
|
||||
rmap.for_each([&](name const & from, name const & to) {
|
||||
if (!removed.contains(to))
|
||||
new_rmap.insert(from, to);
|
||||
substitutions new_substs;
|
||||
substs.for_each([&](name const & from, expr const & to) {
|
||||
lean_assert(is_local(to));
|
||||
if (!removed.contains(mlocal_name(to)))
|
||||
new_substs.insert(from, to);
|
||||
});
|
||||
new_goals.push_back(mvar);
|
||||
new_rlist.push_back(new_rmap);
|
||||
new_slist.push_back(new_substs);
|
||||
it1 = tail(it1);
|
||||
it2 = tail(it2);
|
||||
}
|
||||
lean_assert(!it1 && !it2);
|
||||
rlist = to_list(new_rlist);
|
||||
slist = to_list(new_slist);
|
||||
return to_list(new_goals);
|
||||
}
|
||||
|
||||
substitutions to_substitutions(expr const & mvar, name_map<name> const & renames) {
|
||||
if (renames.empty()) return substitutions();
|
||||
local_context lctx = m_mctx.get_metavar_decl(mvar)->get_context();
|
||||
substitutions R;
|
||||
renames.for_each([&](name const & x, name const & y) {
|
||||
R.insert(x, lctx.get_local_decl(y)->mk_ref());
|
||||
});
|
||||
return R;
|
||||
}
|
||||
|
||||
/* Apply the new_renames at new_names and renames. */
|
||||
void merge_renames(bool update_names, name_map<name> & renames, name_map<name> new_renames) {
|
||||
if (!update_names) return;
|
||||
if (new_renames.empty()) return;
|
||||
/* Merge renames and new_renames */
|
||||
name_map<name> m;
|
||||
renames.for_each([&](name const & k, name const & d) {
|
||||
if (auto r = new_renames.find(d)) {
|
||||
m.insert(k, *r);
|
||||
/* entry d -> *r can be removed from new_renames, since d was not in the initial state. */
|
||||
new_renames.erase(d);
|
||||
} else {
|
||||
m.insert(k, d);
|
||||
}
|
||||
});
|
||||
/* Copy remaining at new_renames entries to m. */
|
||||
new_renames.for_each([&](name const & k, name const & d) {
|
||||
m.insert(k, d);
|
||||
});
|
||||
renames = m;
|
||||
}
|
||||
|
||||
expr apply_renames(local_context const & lctx, name_map<name> const & renames, expr const & e) {
|
||||
return replace(e, [&](expr const & e, unsigned) {
|
||||
if (is_local(e)) {
|
||||
if (auto n = renames.find(mlocal_name(e))) {
|
||||
return some_expr(lctx.get_local_decl(*n)->mk_ref());
|
||||
}
|
||||
}
|
||||
return none_expr();
|
||||
});
|
||||
}
|
||||
|
||||
list<expr> apply_renames(expr const & mvar, name_map<name> const & renames, list<expr> const & es) {
|
||||
if (renames.empty()) return es;
|
||||
local_context lctx = m_mctx.get_metavar_decl(mvar)->get_context();
|
||||
return map(es, [&](expr const & e) { return apply_renames(lctx, renames, e); });
|
||||
}
|
||||
|
||||
optional<expr> unify_eqs(expr mvar, unsigned num_eqs, bool updating,
|
||||
list<expr> & new_intros, substitutions & substs) {
|
||||
if (num_eqs == 0) {
|
||||
|
|
@ -424,7 +377,7 @@ struct cases_tactic_fn {
|
|||
}
|
||||
|
||||
pair<list<expr>, list<name>> unify_eqs(list<expr> const & mvars, list<name> const & cnames, unsigned num_eqs,
|
||||
xintros_list * ilist, substitutions_list * slist) {
|
||||
intros_list * ilist, substitutions_list * slist) {
|
||||
lean_assert((ilist == nullptr) == (slist == nullptr));
|
||||
buffer<expr> new_goals;
|
||||
buffer<list<expr>> new_ilist;
|
||||
|
|
@ -432,7 +385,7 @@ struct cases_tactic_fn {
|
|||
buffer<name> new_cnames;
|
||||
list<expr> it1 = mvars;
|
||||
list<name> itn = cnames;
|
||||
xintros_list const * it2 = ilist;
|
||||
intros_list const * it2 = ilist;
|
||||
substitutions_list const * it3 = slist;
|
||||
while (it1) {
|
||||
list<expr> new_intros;
|
||||
|
|
@ -474,41 +427,7 @@ struct cases_tactic_fn {
|
|||
m_ids(ids){
|
||||
}
|
||||
|
||||
xintros_list to_xintros_list(list<expr> const & new_goals, intros_list const & ilist) {
|
||||
lean_assert(length(new_goals) == length(ilist));
|
||||
buffer<list<expr>> new_intros;
|
||||
auto it1 = new_goals;
|
||||
auto it2 = ilist;
|
||||
while (it1 && it2) {
|
||||
expr const & mvar = head(it1);
|
||||
local_context lctx = m_mctx.get_metavar_decl(mvar)->get_context();
|
||||
new_intros.push_back(map2<expr>(head(it2), [&](name const & n) {
|
||||
return lctx.get_local_decl(n)->mk_ref();
|
||||
}));
|
||||
it1 = tail(it1);
|
||||
it2 = tail(it2);
|
||||
}
|
||||
lean_assert(!it1 && !it2);
|
||||
return to_list(new_intros);
|
||||
}
|
||||
|
||||
substitutions_list to_substitutions_list(list<expr> const & new_goals, renaming_list const & rlist) {
|
||||
lean_assert(length(new_goals) == length(rlist));
|
||||
buffer<substitutions> R;
|
||||
auto it1 = new_goals;
|
||||
auto it2 = rlist;
|
||||
while (it1 && it2) {
|
||||
expr const & mvar = head(it1);
|
||||
local_context lctx = m_mctx.get_metavar_decl(mvar)->get_context();
|
||||
R.push_back(to_substitutions(mvar, head(it2)));
|
||||
it1 = tail(it1);
|
||||
it2 = tail(it2);
|
||||
}
|
||||
lean_assert(!it1 && !it2);
|
||||
return to_list(R);
|
||||
}
|
||||
|
||||
pair<list<expr>, list<name>> operator()(expr const & mvar, expr const & H, xintros_list * ilist, substitutions_list * slist) {
|
||||
pair<list<expr>, list<name>> operator()(expr const & mvar, expr const & H, intros_list * ilist, substitutions_list * slist) {
|
||||
lean_assert((ilist != nullptr) == (slist != nullptr));
|
||||
lean_assert(is_metavar(mvar));
|
||||
lean_assert(m_mctx.get_metavar_decl(mvar));
|
||||
|
|
@ -524,16 +443,10 @@ struct cases_tactic_fn {
|
|||
even when indices are independent. */
|
||||
if (has_indep_indices(g, H) && (!slist || m_nindices == 0)) {
|
||||
/* Easy case */
|
||||
intros_list tmp_ilist;
|
||||
renaming_list tmp_rlist;
|
||||
auto p = mk_pair(induction(m_env, m_opts, m_mode, m_mctx, mvar, H,
|
||||
m_cases_on_decl.get_name(), m_ids,
|
||||
ilist ? &tmp_ilist : nullptr,
|
||||
slist ? &tmp_rlist : nullptr),
|
||||
cname_list);
|
||||
if (ilist) *ilist = to_xintros_list(p.first, tmp_ilist);
|
||||
if (slist) *slist = to_substitutions_list(p.first, tmp_rlist);
|
||||
return p;
|
||||
return mk_pair(induction(m_env, m_opts, m_mode, m_mctx, mvar, H,
|
||||
m_cases_on_decl.get_name(), m_ids,
|
||||
ilist, slist),
|
||||
cname_list);
|
||||
} else {
|
||||
buffer<name> aux_indices_H; /* names of auxiliary indices and major */
|
||||
unsigned num_eqs; /* number of equations that need to be processed */
|
||||
|
|
@ -541,16 +454,19 @@ struct cases_tactic_fn {
|
|||
lean_cases_trace(mvar1, tout() << "after generalize_indices:\n" << pp_goal(mvar1) << "\n";);
|
||||
expr H1 = m_mctx.get_metavar_decl(mvar1)->get_context().get_last_local_decl()->mk_ref();
|
||||
intros_list tmp_ilist;
|
||||
renaming_list tmp_rlist;
|
||||
substitutions_list tmp_slist;
|
||||
list<expr> new_goals1 = induction(m_env, m_opts, m_mode, m_mctx, mvar1, H1, m_cases_on_decl.get_name(),
|
||||
m_ids, &tmp_ilist, &tmp_rlist);
|
||||
m_ids, &tmp_ilist, &tmp_slist);
|
||||
lean_cases_trace(mvar1, tout() << "after applying cases_on:";
|
||||
for (auto g : new_goals1) tout() << "\n" << pp_goal(g) << "\n";);
|
||||
list<expr> new_goals2 = elim_aux_indices(new_goals1, aux_indices_H, tmp_rlist);
|
||||
list<expr> new_goals2 = elim_aux_indices(new_goals1, aux_indices_H, tmp_slist);
|
||||
if (ilist) {
|
||||
lean_assert(slist);
|
||||
*ilist = tmp_ilist;
|
||||
*slist = tmp_slist;
|
||||
}
|
||||
lean_cases_trace(mvar1, tout() << "after eliminating auxiliary indices:";
|
||||
for (auto g : new_goals2) tout() << "\n" << pp_goal(g) << "\n";);
|
||||
if (ilist) *ilist = to_xintros_list(new_goals2, tmp_ilist);
|
||||
if (slist) *slist = to_substitutions_list(new_goals2, tmp_rlist);
|
||||
return unify_eqs(new_goals2, cname_list, num_eqs, ilist, slist);
|
||||
}
|
||||
}
|
||||
|
|
@ -558,7 +474,7 @@ struct cases_tactic_fn {
|
|||
|
||||
pair<list<expr>, list<name>>
|
||||
cases(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx,
|
||||
expr const & mvar, expr const & H, list<name> & ids, xintros_list * ilist, substitutions_list * slist) {
|
||||
expr const & mvar, expr const & H, list<name> & ids, intros_list * ilist, substitutions_list * slist) {
|
||||
auto r = cases_tactic_fn(env, opts, m, mctx, ids)(mvar, H, ilist, slist);
|
||||
lean_assert(length(r.first) == length(r.second));
|
||||
return r;
|
||||
|
|
|
|||
|
|
@ -9,9 +9,6 @@ Author: Leonardo de Moura
|
|||
#include "library/tactic/subst_tactic.h"
|
||||
|
||||
namespace lean {
|
||||
typedef list<list<expr>> xintros_list;
|
||||
typedef list<substitutions> substitutions_list;
|
||||
|
||||
/** \brief Similar to induction, but applies 'cases_on' and has bettern support for dependent types. Failures are reported using exceptions.
|
||||
\c ids (if available) provides the names for new hypotheses.
|
||||
If ilist and slist are not nullptr, then
|
||||
|
|
@ -32,7 +29,7 @@ typedef list<substitutions> substitutions_list;
|
|||
since some of the goals are discarded. */
|
||||
pair<list<expr>, list<name>>
|
||||
cases(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx,
|
||||
expr const & mvar, expr const & H, list<name> & ids, xintros_list * ilist, substitutions_list * slist);
|
||||
expr const & mvar, expr const & H, list<name> & ids, intros_list * ilist, substitutions_list * slist);
|
||||
|
||||
void initialize_cases_tactic();
|
||||
void finalize_cases_tactic();
|
||||
|
|
|
|||
|
|
@ -61,31 +61,12 @@ static unsigned get_expr_arity(expr type) {
|
|||
return r;
|
||||
}
|
||||
|
||||
bool check_intro_renaming(list<name> const & intros, name_map<name> const & renames) {
|
||||
for (name const & H : intros) {
|
||||
lean_assert(!renames.contains(H));
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool check_ilist_rlist(intros_list const & ilist, renaming_list const & rlist) {
|
||||
auto it1 = ilist;
|
||||
auto it2 = rlist;
|
||||
lean_assert(length(it1) == length(it2));
|
||||
while (it1 && it2) {
|
||||
lean_assert(check_intro_renaming(head(it1), head(it2)));
|
||||
it1 = tail(it1);
|
||||
it2 = tail(it2);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
list<expr> induction(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx,
|
||||
expr const & mvar, expr const & H, name const & rec_name, list<name> & ns,
|
||||
intros_list * ilist, renaming_list * rlist) {
|
||||
intros_list * ilist, substitutions_list * slist) {
|
||||
lean_assert(is_metavar(mvar));
|
||||
lean_assert(is_local(H));
|
||||
lean_assert((ilist == nullptr) == (rlist == nullptr));
|
||||
lean_assert((ilist == nullptr) == (slist == nullptr));
|
||||
optional<metavar_decl> g = mctx.get_metavar_decl(mvar);
|
||||
lean_assert(g);
|
||||
type_context ctx1 = mk_type_context_for(env, opts, mctx, g->get_context(), m);
|
||||
|
|
@ -147,11 +128,12 @@ list<expr> induction(environment const & env, options const & opts, transparency
|
|||
optional<expr> mvar2 = intron(env, opts, mctx, mvar1, indices.size() + 1, indices_H);
|
||||
if (!mvar2)
|
||||
throw exception("induction tactic failed, failed to reintroduce major premise");
|
||||
name_map<name> base_renames; /* renames for all branches */
|
||||
if (rlist) {
|
||||
substitutions base_substs; /* substitutions for all branches */
|
||||
if (slist) {
|
||||
local_context lctx = mctx.get_metavar_decl(*mvar2)->get_context();
|
||||
/* store old index name -> new index name */
|
||||
for (unsigned i = 0; i < indices.size(); i++) {
|
||||
base_renames.insert(mlocal_name(indices[i]), indices_H[i]);
|
||||
base_substs.insert(mlocal_name(indices[i]), lctx.get_local_decl(indices_H[i])->mk_ref());
|
||||
}
|
||||
}
|
||||
optional<metavar_decl> g2 = mctx.get_metavar_decl(*mvar2);
|
||||
|
|
@ -222,8 +204,8 @@ list<expr> induction(environment const & env, options const & opts, transparency
|
|||
unsigned first_idx_pos = rec_info.get_first_index_pos();
|
||||
bool consumed_major = false;
|
||||
buffer<expr> new_goals;
|
||||
buffer<list<name>> param_names_buffer;
|
||||
buffer<name_map<name>> rename_buffer;
|
||||
buffer<list<expr>> params_buffer;
|
||||
buffer<substitutions> substs_buffer;
|
||||
list<bool> produce_motive = rec_info.get_produce_motive();
|
||||
while (is_pi(rec_type) && curr_pos < rec_info.get_num_args()) {
|
||||
if (first_idx_pos == curr_pos) {
|
||||
|
|
@ -265,18 +247,22 @@ list<expr> induction(environment const & env, options const & opts, transparency
|
|||
set_intron(aux_M, ctx2, new_M, nparams, ns, param_names);
|
||||
/* Introduce hypothesis that had to be reverted because they depended on indices and/or major premise. */
|
||||
set_intron(aux_M, ctx2, aux_M, nextra, extra_names);
|
||||
local_context aux_M_lctx = ctx2.mctx().get_metavar_decl(aux_M)->get_context();
|
||||
if (ilist) {
|
||||
/* Save name of constructor parameters that have been introduced for new goal. */
|
||||
param_names_buffer.push_back(to_list(param_names));
|
||||
buffer<expr> params;
|
||||
for (name const & n : param_names)
|
||||
params.push_back(aux_M_lctx.get_local_decl(n)->mk_ref());
|
||||
params_buffer.push_back(to_list(params));
|
||||
}
|
||||
if (rlist) {
|
||||
if (slist) {
|
||||
/* Save renaming for hypothesis that depend on indices and/or major premise. */
|
||||
name_map<name> rmap = base_renames;
|
||||
substitutions S = base_substs;
|
||||
lean_assert(extra_names.size() == nextra);
|
||||
for (unsigned i = indices.size() + 1, j = 0; i < to_revert.size(); i++, j++) {
|
||||
rmap.insert(mlocal_name(to_revert[i]), extra_names[j]);
|
||||
S.insert(mlocal_name(to_revert[i]), aux_M_lctx.get_local_decl(extra_names[j])->mk_ref());
|
||||
}
|
||||
rename_buffer.push_back(rmap);
|
||||
substs_buffer.push_back(S);
|
||||
}
|
||||
/* Clear hypothesis in the new goal. */
|
||||
set_clear(aux_M, ctx2, aux_M, H2);
|
||||
|
|
@ -295,10 +281,9 @@ list<expr> induction(environment const & env, options const & opts, transparency
|
|||
mctx = ctx2.mctx();
|
||||
mctx.assign(*mvar2, rec);
|
||||
if (ilist) {
|
||||
lean_assert(rlist);
|
||||
*ilist = to_list(param_names_buffer);
|
||||
*rlist = to_list(rename_buffer);
|
||||
lean_assert(check_ilist_rlist(*ilist, *rlist));
|
||||
lean_assert(slist);
|
||||
*ilist = to_list(params_buffer);
|
||||
*slist = to_list(substs_buffer);
|
||||
}
|
||||
return to_list(new_goals);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -6,16 +6,17 @@ Author: Leonardo de Moura
|
|||
*/
|
||||
#pragma once
|
||||
#include "library/tactic/tactic_state.h"
|
||||
#include "library/tactic/subst_tactic.h"
|
||||
|
||||
namespace lean {
|
||||
typedef list<list<name>> intros_list;
|
||||
typedef list<name_map<name>> renaming_list;
|
||||
typedef list<list<expr>> intros_list;
|
||||
typedef list<substitutions> substitutions_list;
|
||||
|
||||
/** \brief Apply the induction lemma \c rec_name on the hypothesis \c H at goal \c mvar.
|
||||
The tactic uses ns (if available) to name parameters associated with minor premises.
|
||||
|
||||
If ilist != nullptr, then tactic stores the (internal) names for parameters introduced.
|
||||
If rlist != nullptr, then tactic stores renamed hypotheses for each new goal.
|
||||
If ilist != nullptr, then tactic stores the new hypotheses introduced for each new goal.
|
||||
If slist != nullptr, then tactic stores renamed hypotheses for each new goal.
|
||||
|
||||
The result is a list of goals (new metavariables).
|
||||
|
||||
|
|
@ -24,10 +25,10 @@ typedef list<name_map<name>> renaming_list;
|
|||
\pre mctx.get_metavar_decl(mvar) != none
|
||||
|
||||
\post ilist != nullptr ==> length(*ilist) == length(result)
|
||||
\post rlist != nullptr ==> length(*rlist) == length(result) */
|
||||
\post slist != nullptr ==> length(*slist) == length(result) */
|
||||
list<expr> induction(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx,
|
||||
expr const & mvar, expr const & H, name const & rec_name, list<name> & ns,
|
||||
intros_list * ilist, renaming_list * rlist);
|
||||
intros_list * ilist, substitutions_list * slist);
|
||||
|
||||
void initialize_induction_tactic();
|
||||
void finalize_induction_tactic();
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue