From 1ea3bc16836e5559c4e15b267d31abcd975568f2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 21 Aug 2016 15:46:48 -0700 Subject: [PATCH] fix(library/tactic/cases_tactic): lowlevel interface that gives access to renamed/introduced hypotheses --- src/library/tactic/cases_tactic.cpp | 91 ++++++++++++++++++++--------- src/library/tactic/cases_tactic.h | 8 ++- src/library/tactic/subst_tactic.cpp | 15 ++++- 3 files changed, 84 insertions(+), 30 deletions(-) diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp index 0e31d69b17..5b82b55945 100644 --- a/src/library/tactic/cases_tactic.cpp +++ b/src/library/tactic/cases_tactic.cpp @@ -71,6 +71,18 @@ struct cases_tactic_fn { m_cases_on_decl = m_env.get({n, "cases_on"}); } + /* For debugging purposes, check whether all hypotheses in Hs are in the local context for mvar */ + bool check_hypotheses_in_context(expr const & mvar, list> const & Hs) { + local_context lctx = m_mctx.get_metavar_decl(mvar)->get_context(); + for (optional const & H : Hs) { + if (H && !lctx.get_local_decl(*H)) { + lean_unreachable(); + return false; + } + } + return true; + } + bool is_cases_applicable(expr const & mvar, expr const & H) { type_context ctx = mk_type_context_for(mvar); expr t = ctx.infer(H); @@ -255,18 +267,21 @@ struct cases_tactic_fn { } /* Apply the new_renames at new_names and renames. */ - void merge_renames(bool update_renames, list & new_names, name_map & renames, name_map new_renames) { - if (!update_renames) return; + void merge_renames(bool update_names, list> & new_names, name_map & renames, name_map new_renames) { + if (!update_names) return; + if (new_renames.empty()) return; /* Apply new_renames to new_names. */ - buffer new_new_names; - for (name const & n : new_names) { - if (auto r = new_renames.find(n)) - new_new_names.push_back(*r); + buffer> new_new_names; + for (optional const & n : new_names) { + if (!n) + new_new_names.push_back(n); + else if (auto r = new_renames.find(*n)) + new_new_names.push_back(optional(*r)); else new_new_names.push_back(n); } new_names = to_list(new_new_names); - /* Merge renames and new_names */ + /* Merge renames and new_renames */ name_map m; renames.for_each([&](name const & k, name const & d) { if (auto r = new_renames.find(d)) { @@ -284,7 +299,7 @@ struct cases_tactic_fn { renames = m; } - optional unify_eqs(expr mvar, unsigned num_eqs, bool update_renames, list & new_names, name_map & renames) { + optional unify_eqs(expr mvar, unsigned num_eqs, bool updating_names, list> & new_names, name_map & renames) { if (num_eqs == 0) return some_expr(mvar); expr A, B, lhs, rhs; @@ -326,15 +341,24 @@ struct cases_tactic_fn { expr val = mk_app(mvar2, mk_eq_of_heq(ctx, H)); m_mctx.assign(*mvar1, val); lean_cases_trace(mvar, tout() << "converted heq => eq\n";); - return unify_eqs(mvar2, num_eqs, update_renames, new_names, renames); + return unify_eqs(mvar2, num_eqs, updating_names, new_names, renames); } else if (is_eq(H_type, A, lhs, rhs)) { if (is_local(rhs) || is_local(lhs)) { lean_cases_trace(mvar, tout() << "substitute\n";); name_map extra_renames; bool symm = is_local(rhs); - expr mvar2 = subst(m_env, m_opts, m_mode, m_mctx, *mvar1, H, symm, update_renames ? &extra_renames : nullptr); - merge_renames(update_renames, new_names, renames, extra_renames); - return unify_eqs(mvar2, num_eqs - 1, update_renames, new_names, renames); + lean_assert(check_hypotheses_in_context(*mvar1, new_names)); + if (updating_names && is_local(rhs)) { + /* The next substitution may eliminate introduced hypothesis */ + name from_name = mlocal_name(rhs); + new_names = map(new_names, [&](optional const & n) { + return (n && *n == from_name) ? optional() : n; + }); + } + expr mvar2 = subst(m_env, m_opts, m_mode, m_mctx, *mvar1, H, symm, updating_names ? &extra_renames : nullptr); + merge_renames(updating_names, new_names, renames, extra_renames); + lean_assert(check_hypotheses_in_context(mvar2, new_names)); + return unify_eqs(mvar2, num_eqs - 1, updating_names, new_names, renames); } else { optional c1 = is_constructor_app(m_env, lhs); optional c2 = is_constructor_app(m_env, rhs); @@ -359,7 +383,7 @@ struct cases_tactic_fn { m_mctx.assign(*mvar1, val); unsigned A_nparams = *inductive::get_num_params(m_env, const_name(A_fn)); lean_assert(get_app_num_args(lhs) >= A_nparams); - return unify_eqs(mvar2, num_eqs - 1 + get_app_num_args(lhs) - A_nparams, update_renames, new_names, renames); + return unify_eqs(mvar2, num_eqs - 1 + get_app_num_args(lhs) - A_nparams, updating_names, new_names, renames); } else { /* conflict, closes the goal */ lean_cases_trace(*mvar1, tout() << "conflicting equality detected, closing goal using no_confusion\n";); @@ -374,23 +398,25 @@ struct cases_tactic_fn { } } - pair, list> unify_eqs(list const & mvars, list const & cnames, unsigned num_eqs, intros_list * ilist, renaming_list * rlist) { - buffer new_goals; - buffer> new_ilist; - buffer> new_rlist; - buffer new_cnames; + pair, list> unify_eqs(list const & mvars, list const & cnames, unsigned num_eqs, cintros_list * ilist, renaming_list * rlist) { + lean_assert((ilist == nullptr) == (rlist == nullptr)); + buffer new_goals; + buffer>> new_ilist; + buffer> new_rlist; + buffer new_cnames; list it1 = mvars; list itn = cnames; - intros_list const * it2 = ilist; + cintros_list const * it2 = ilist; renaming_list const * it3 = rlist; while (it1) { - list new_names; + list> new_names; name_map renames; if (ilist) { new_names = head(*it2); - renames = head(*it3); + renames = head(*it3); } - optional new_mvar = unify_eqs(head(it1), num_eqs, ilist != nullptr, new_names, renames); + bool updating_names = ilist != nullptr; + optional new_mvar = unify_eqs(head(it1), num_eqs, updating_names, new_names, renames); if (new_mvar) { new_goals.push_back(*new_mvar); new_cnames.push_back(head(itn)); @@ -401,6 +427,7 @@ struct cases_tactic_fn { it2 = &tail(*it2); it3 = &tail(*it3); if (new_mvar) { + lean_assert(check_hypotheses_in_context(*new_mvar, new_names)); new_ilist.push_back(new_names); new_rlist.push_back(renames); } @@ -421,7 +448,14 @@ struct cases_tactic_fn { m_ids(ids) { } - pair, list> operator()(expr const & mvar, expr const & H, intros_list * ilist, renaming_list * rlist) { + cintros_list to_cintros_list(intros_list const & ilist) { + return map2>>(ilist, [](list const & ls) { + return map2>(ls, [](name const & n) { + return optional(n); }); + }); + } + + pair, list> operator()(expr const & mvar, expr const & H, cintros_list * ilist, renaming_list * rlist) { lean_assert((ilist != nullptr) == (rlist != nullptr)); lean_assert(is_metavar(mvar)); lean_assert(m_mctx.get_metavar_decl(mvar)); @@ -435,8 +469,11 @@ struct cases_tactic_fn { metavar_decl g = *m_mctx.get_metavar_decl(mvar); if (has_indep_indices(g, H)) { /* Easy case */ - return mk_pair(induction(m_env, m_opts, m_mode, m_mctx, mvar, H, m_cases_on_decl.get_name(), m_ids, ilist, rlist), - cname_list); + intros_list tmp_ilist; + 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, rlist), + cname_list); + if (ilist) *ilist = to_cintros_list(tmp_ilist); + return p; } else { buffer aux_indices_H; /* names of auxiliary indices and major */ unsigned num_eqs; /* number of equations that need to be processed */ @@ -451,7 +488,7 @@ struct cases_tactic_fn { list new_goals2 = elim_aux_indices(new_goals1, aux_indices_H, tmp_rlist); lean_cases_trace(mvar1, tout() << "after eliminating auxiliary indices:"; for (auto g : new_goals2) tout() << "\n" << pp_goal(g) << "\n";); - if (ilist) *ilist = tmp_ilist; + if (ilist) *ilist = to_cintros_list(tmp_ilist); if (rlist) *rlist = tmp_rlist; return unify_eqs(new_goals2, cname_list, num_eqs, ilist, rlist); } @@ -460,7 +497,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, intros_list * ilist, renaming_list * rlist) { + expr const & mvar, expr const & H, list & ids, cintros_list * ilist, renaming_list * rlist) { auto r = cases_tactic_fn(env, opts, m, mctx, ids)(mvar, H, ilist, rlist); 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 6715e91561..69f3409fd3 100644 --- a/src/library/tactic/cases_tactic.h +++ b/src/library/tactic/cases_tactic.h @@ -8,10 +8,14 @@ Author: Leonardo de Moura #include "library/tactic/induction_tactic.h" namespace lean { +typedef list>> cintros_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 rlist are not nullptr, then + If cilist and rlist are not nullptr, then 1- Store in ilist the new hypotheses introduced for each new goal. + We have a new hypothesis for each constructor field. + The entry is none if the field was eliminated during dependent pattern matching. 2- Store in rlist the hypotheses renamed in each new goal. \pre (ilist == nullptr) iff (rlist == nullptr) \post ilist != nullptr -> rlist != nullptr -> length(*ilist) == length(*rlist) @@ -24,7 +28,7 @@ namespace lean { 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, intros_list * ilist, renaming_list * rlist); + expr const & mvar, expr const & H, list & ids, cintros_list * ilist, renaming_list * rlist); void initialize_cases_tactic(); void finalize_cases_tactic(); diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp index d8e36e30b4..cfd10d39e6 100644 --- a/src/library/tactic/subst_tactic.cpp +++ b/src/library/tactic/subst_tactic.cpp @@ -20,6 +20,16 @@ Author: Leonardo de Moura #include "library/tactic/app_builder_tactics.h" namespace lean { +/* For debugging purposes, make sure H is in the local context for mvar */ +static bool check_hypothesis_in_context(metavar_context const & mctx, expr const & mvar, name const & H) { + local_context lctx = mctx.get_metavar_decl(mvar)->get_context(); + if (!lctx.get_local_decl(H)) { + lean_unreachable(); + return false; + } + return true; +} + expr subst(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx, expr const & mvar, expr const & H, bool symm, name_map * renames) { #define lean_subst_trace(CODE) lean_trace(name({"tactic", "subst"}), CODE) @@ -74,14 +84,17 @@ expr subst(environment const & env, options const & opts, transparency_mode cons expr mvar5 = clear(mctx, mvar4, lhs); buffer new_Hnames; optional mvar6 = intron(env, opts, mctx, mvar5, to_revert.size() - 2, new_Hnames); + if (!mvar6) throw exception("subst tactic failed, unexpected failure when re-introducing dependencies"); + lean_assert(new_Hnames.size() == to_revert.size() - 2); if (renames) { name_map rmap; for (unsigned i = 0; i < to_revert.size() - 2; i++) { + lean_assert(check_hypothesis_in_context(mctx, mvar, mlocal_name(to_revert[i+2]))); + lean_assert(check_hypothesis_in_context(mctx, *mvar6, new_Hnames[i])); rmap.insert(mlocal_name(to_revert[i+2]), new_Hnames[i]); } *renames = rmap; } - if (!mvar6) throw exception("subst tactic failed, unexpected failure when re-introducing dependencies"); lean_subst_trace_state(*mvar6, "after intro remaining reverted hypotheses:\n"); return *mvar6; }