From 207e8e86da2ea81b6381d147aa2050692e2b247c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 10 May 2015 11:06:18 -0700 Subject: [PATCH] fix(library/definitional/equations): do not clear eliminated hypotheses when invoking 'cases' tactic from definitional package --- src/library/definitional/equations.cpp | 3 ++- src/library/tactic/inversion_tactic.cpp | 19 +++++++++++-------- src/library/tactic/inversion_tactic.h | 3 ++- 3 files changed, 15 insertions(+), 10 deletions(-) diff --git a/src/library/definitional/equations.cpp b/src/library/definitional/equations.cpp index f1754130e..1cf25d887 100644 --- a/src/library/definitional/equations.cpp +++ b/src/library/definitional/equations.cpp @@ -896,7 +896,8 @@ class equation_compiler_fn { expr h = p.get_var(*head(p.m_var_stack)); goal g = to_goal(p); auto imps = to_implementation_list(p); - if (auto r = apply(env(), ios(), m_tc, g, h, imps)) { + bool clear_elim = false; + if (auto r = apply(env(), ios(), m_tc, g, h, imps, clear_elim)) { substitution subst = r->m_subst; list> args = r->m_args; list rn_maps = r->m_renames; diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp index 515bfc2ec..59d7fef91 100644 --- a/src/library/tactic/inversion_tactic.cpp +++ b/src/library/tactic/inversion_tactic.cpp @@ -115,6 +115,7 @@ class inversion_tac { declaration m_cases_on_decl; bool m_throw_tactic_exception; // if true, then throw tactic_exception in case of failure, instead of returning none + bool m_clear_elim; // if true, then clear eliminated variables expr whnf(expr const & e) { return m_tc.whnf(e).first; } expr infer_type(expr const & e) { return m_tc.infer(e).first; } @@ -798,7 +799,7 @@ class inversion_tac { // Remark: A is the type of lhs and rhs hyps.pop_back(); // remove processed equality buffer non_deps, deps; - bool clear_rhs = true; + bool clear_rhs = m_clear_elim; split_deps(hyps, rhs, non_deps, deps, clear_rhs); if (deps.empty() && !depends_on(g_type, rhs)) { // eq.rec is not necessary @@ -1021,14 +1022,15 @@ class inversion_tac { public: inversion_tac(environment const & env, io_state const & ios, name_generator const & ngen, type_checker & tc, substitution const & subst, list const & ids, - bool throw_tactic_ex): + bool throw_tactic_ex, bool clear_elim): m_env(env), m_ios(ios), m_tc(tc), m_ids(ids), - m_ngen(ngen), m_subst(subst), m_throw_tactic_exception(throw_tactic_ex) { + m_ngen(ngen), m_subst(subst), m_throw_tactic_exception(throw_tactic_ex), + m_clear_elim(clear_elim) { m_proof_irrel = m_env.prop_proof_irrel(); } - inversion_tac(environment const & env, io_state const & ios, type_checker & tc): - inversion_tac(env, ios, tc.mk_ngen(), tc, substitution(), list(), false) {} + inversion_tac(environment const & env, io_state const & ios, type_checker & tc, bool clear_elim): + inversion_tac(env, ios, tc.mk_ngen(), tc, substitution(), list(), false, clear_elim) {} typedef inversion::result result; @@ -1083,8 +1085,8 @@ public: namespace inversion { optional apply(environment const & env, io_state const & ios, type_checker & tc, - goal const & g, expr const & h, implementation_list const & imps) { - return inversion_tac(env, ios, tc).execute(g, h, imps); + goal const & g, expr const & h, implementation_list const & imps, bool clear_elim) { + return inversion_tac(env, ios, tc, clear_elim).execute(g, h, imps); } } @@ -1097,7 +1099,8 @@ tactic inversion_tactic(name const & n, list const & ids) { goals tail_gs = tail(gs); name_generator ngen = ps.get_ngen(); std::unique_ptr tc = mk_type_checker(env, ngen.mk_child()); - inversion_tac tac(env, ios, ngen, *tc, ps.get_subst(), ids, ps.report_failure()); + bool clear_elim = true; + inversion_tac tac(env, ios, ngen, *tc, ps.get_subst(), ids, ps.report_failure(), clear_elim); if (auto res = tac.execute(g, n, implementation_list())) { proof_state new_s(ps, append(res->m_goals, tail_gs), res->m_subst, res->m_ngen); return some_proof_state(new_s); diff --git a/src/library/tactic/inversion_tactic.h b/src/library/tactic/inversion_tactic.h index ad8c1c653..9939dabff 100644 --- a/src/library/tactic/inversion_tactic.h +++ b/src/library/tactic/inversion_tactic.h @@ -57,7 +57,8 @@ struct result { }; optional apply(environment const & env, io_state const & ios, type_checker & tc, - goal const & g, expr const & h, implementation_list const & imps); + goal const & g, expr const & h, implementation_list const & imps, + bool clear_elim); } tactic inversion_tactic(name const & n, list const & ids = list());