diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index b1b6d330e6..44d18f0d24 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -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 new_goals; list new_goal_cnames; diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp index 5366ab29da..2ca8beaacb 100644 --- a/src/library/tactic/cases_tactic.cpp +++ b/src/library/tactic/cases_tactic.cpp @@ -237,93 +237,46 @@ struct cases_tactic_fn { return tmp.pp_goal(mvar); } - list elim_aux_indices(list const & goals, buffer const & aux_indices_H, renaming_list & rlist) { - lean_assert(length(goals) == length(rlist)); + list elim_aux_indices(list const & goals, buffer const & aux_indices_H, substitutions_list & slist) { + lean_assert(!slist || length(goals) == length(slist)); buffer new_goals; - buffer> new_rlist; + buffer new_slist; list it1 = goals; - list> it2 = rlist; + substitutions_list it2 = slist; while (it1 && it2) { - expr mvar = head(it1); - name_map 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 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 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 & renames, name_map new_renames) { - if (!update_names) return; - if (new_renames.empty()) return; - /* Merge renames and new_renames */ - name_map 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 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 apply_renames(expr const & mvar, name_map const & renames, list 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 unify_eqs(expr mvar, unsigned num_eqs, bool updating, list & new_intros, substitutions & substs) { if (num_eqs == 0) { @@ -424,7 +377,7 @@ struct cases_tactic_fn { } pair, list> unify_eqs(list const & mvars, list const & cnames, unsigned num_eqs, - xintros_list * ilist, substitutions_list * slist) { + intros_list * ilist, substitutions_list * slist) { lean_assert((ilist == nullptr) == (slist == nullptr)); buffer new_goals; buffer> new_ilist; @@ -432,7 +385,7 @@ struct cases_tactic_fn { buffer new_cnames; list it1 = mvars; list itn = cnames; - xintros_list const * it2 = ilist; + intros_list const * it2 = ilist; substitutions_list const * it3 = slist; while (it1) { list new_intros; @@ -474,41 +427,7 @@ struct cases_tactic_fn { m_ids(ids){ } - xintros_list to_xintros_list(list const & new_goals, intros_list const & ilist) { - lean_assert(length(new_goals) == length(ilist)); - buffer> 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(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 const & new_goals, renaming_list const & rlist) { - lean_assert(length(new_goals) == length(rlist)); - buffer 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> operator()(expr const & mvar, expr const & H, xintros_list * ilist, substitutions_list * slist) { + pair, list> 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 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 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 new_goals2 = elim_aux_indices(new_goals1, aux_indices_H, tmp_rlist); + list 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> cases(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx, - expr const & mvar, expr const & H, list & ids, xintros_list * ilist, substitutions_list * slist) { + expr const & mvar, expr const & H, list & 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; diff --git a/src/library/tactic/cases_tactic.h b/src/library/tactic/cases_tactic.h index 30d214b320..cfde3758a1 100644 --- a/src/library/tactic/cases_tactic.h +++ b/src/library/tactic/cases_tactic.h @@ -9,9 +9,6 @@ Author: Leonardo de Moura #include "library/tactic/subst_tactic.h" namespace lean { -typedef list> xintros_list; -typedef list 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_list; since some of the goals are discarded. */ pair, list> cases(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx, - expr const & mvar, expr const & H, list & ids, xintros_list * ilist, substitutions_list * slist); + expr const & mvar, expr const & H, list & ids, intros_list * ilist, substitutions_list * slist); void initialize_cases_tactic(); void finalize_cases_tactic(); diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index b5731df4a8..29851defb2 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -61,31 +61,12 @@ static unsigned get_expr_arity(expr type) { return r; } -bool check_intro_renaming(list const & intros, name_map 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 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 & 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 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 induction(environment const & env, options const & opts, transparency optional 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 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 g2 = mctx.get_metavar_decl(*mvar2); @@ -222,8 +204,8 @@ list induction(environment const & env, options const & opts, transparency unsigned first_idx_pos = rec_info.get_first_index_pos(); bool consumed_major = false; buffer new_goals; - buffer> param_names_buffer; - buffer> rename_buffer; + buffer> params_buffer; + buffer substs_buffer; list 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 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 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 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 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); } diff --git a/src/library/tactic/induction_tactic.h b/src/library/tactic/induction_tactic.h index 222da06ed7..a983ac487a 100644 --- a/src/library/tactic/induction_tactic.h +++ b/src/library/tactic/induction_tactic.h @@ -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> intros_list; -typedef list> renaming_list; +typedef list> intros_list; +typedef list 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> 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 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 & ns, - intros_list * ilist, renaming_list * rlist); + intros_list * ilist, substitutions_list * slist); void initialize_induction_tactic(); void finalize_induction_tactic();