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

fix(library/blast/forward/ematch): extract lemma using target expression instead of pattern

Browse source 
Reason: pattern contains temporary universe meta-variables.
This commit is contained in:
Leonardo de Moura 2015-11-30 07:58:34 -07:00
parent 9f3f24b46c
commit 3d7831284b
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/library/blast/forward/ematch.cpp
View file

@ -158,17 +158,20 @@ struct ematch_fn {
if (m_ctx->is_mvar(fn)) if (m_ctx->is_mvar(fn))
return is_eqv(R, p, t); return is_eqv(R, p, t);
buffer<expr> candidates; buffer<expr> candidates;
expr t_fn;
expr it = t; expr it = t;
do { do {
if (m_cc.is_congr_root(R, t) && m_ctx->is_def_eq(get_app_fn(it), fn) && expr const & it_fn = get_app_fn(it);
if (m_cc.is_congr_root(R, t) && m_ctx->is_def_eq(it_fn, fn) &&
get_app_num_args(it) == p_args.size()) { get_app_num_args(it) == p_args.size()) {
t_fn = it_fn;
candidates.push_back(it); candidates.push_back(it);
} }
it = m_cc.get_next(R, it); it = m_cc.get_next(R, it);
} while (it != t); } while (it != t);
if (candidates.empty()) if (candidates.empty())
return false; return false;
optional<ext_congr_lemma> lemma = mk_ext_congr_lemma(R, fn, p_args.size()); optional<ext_congr_lemma> lemma = mk_ext_congr_lemma(R, t_fn, p_args.size());
if (!lemma) if (!lemma)
return false; return false;
buffer<state> new_states; buffer<state> new_states;
@ -280,7 +283,7 @@ struct ematch_fn {
} }
m_choice_stack.clear(); m_choice_stack.clear();
m_state = s; m_state = s;
optional<ext_congr_lemma> cg_lemma = mk_ext_congr_lemma(R, f, p0_args.size()); optional<ext_congr_lemma> cg_lemma = mk_ext_congr_lemma(R, get_app_fn(t), p0_args.size());
if (!cg_lemma) if (!cg_lemma)
return; return;
buffer<expr> t_args; buffer<expr> t_args;