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

fix(library/definitional/equations): do not clear eliminated hypotheses when invoking 'cases' tactic from definitional package

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-10 11:06:18 -07:00
parent 299fd5c919
commit 207e8e86da
3 changed files with 15 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/definitional/equations.cpp
View file

@ -896,7 +896,8 @@ class equation_compiler_fn {
expr h = p.get_var(*head(p.m_var_stack)); expr h = p.get_var(*head(p.m_var_stack));
goal g = to_goal(p); goal g = to_goal(p);
auto imps = to_implementation_list(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; substitution subst = r->m_subst;
list<list<expr>> args = r->m_args; list<list<expr>> args = r->m_args;
list<rename_map> rn_maps = r->m_renames; list<rename_map> rn_maps = r->m_renames;

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

@ -115,6 +115,7 @@ class inversion_tac {
declaration m_cases_on_decl; 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_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 whnf(expr const & e) { return m_tc.whnf(e).first; }
expr infer_type(expr const & e) { return m_tc.infer(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 // Remark: A is the type of lhs and rhs
hyps.pop_back(); // remove processed equality hyps.pop_back(); // remove processed equality
buffer<expr> non_deps, deps; buffer<expr> non_deps, deps;
bool clear_rhs = true; bool clear_rhs = m_clear_elim;
split_deps(hyps, rhs, non_deps, deps, clear_rhs); split_deps(hyps, rhs, non_deps, deps, clear_rhs);
if (deps.empty() && !depends_on(g_type, rhs)) { if (deps.empty() && !depends_on(g_type, rhs)) {
// eq.rec is not necessary // eq.rec is not necessary
@ -1021,14 +1022,15 @@ class inversion_tac {
public: public:
inversion_tac(environment const & env, io_state const & ios, name_generator const & ngen, inversion_tac(environment const & env, io_state const & ios, name_generator const & ngen,
type_checker & tc, substitution const & subst, list<name> const & ids, type_checker & tc, substitution const & subst, list<name> 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_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(); m_proof_irrel = m_env.prop_proof_irrel();
} }
inversion_tac(environment const & env, io_state const & ios, type_checker & tc): 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<name>(), false) {} inversion_tac(env, ios, tc.mk_ngen(), tc, substitution(), list<name>(), false, clear_elim) {}
typedef inversion::result result; typedef inversion::result result;
@ -1083,8 +1085,8 @@ public:
namespace inversion { namespace inversion {
optional<result> apply(environment const & env, io_state const & ios, type_checker & tc, optional<result> 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) {
return inversion_tac(env, ios, tc).execute(g, h, imps); return inversion_tac(env, ios, tc, clear_elim).execute(g, h, imps);
} }
} }
@ -1097,7 +1099,8 @@ tactic inversion_tactic(name const & n, list<name> const & ids) {
goals tail_gs = tail(gs); goals tail_gs = tail(gs);
name_generator ngen = ps.get_ngen(); name_generator ngen = ps.get_ngen();
std::unique_ptr<type_checker> tc = mk_type_checker(env, ngen.mk_child()); std::unique_ptr<type_checker> 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())) { 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); proof_state new_s(ps, append(res->m_goals, tail_gs), res->m_subst, res->m_ngen);
return some_proof_state(new_s); return some_proof_state(new_s);

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

@ -57,7 +57,8 @@ struct result {
}; };
optional<result> apply(environment const & env, io_state const & ios, type_checker & tc, optional<result> 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<name> const & ids = list<name>()); tactic inversion_tactic(name const & n, list<name> const & ids = list<name>());