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

fix(library/blast/congruence_closure): do not adjust proofs when blast.cc.heq == false

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-10 15:28:16 -08:00
parent e9d24ec152
commit 912bccb3f9
1 changed files with 13 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/library/blast/congruence_closure.cpp
View file

@ -1220,6 +1220,7 @@ expr congruence_closure::mk_congr_proof_core(name const & R, expr const & lhs, e
it = &(tail(*it));
}
expr r = mk_app(spec_lemma->m_congr_lemma.get_proof(), lemma_args);
lean_assert(g_heq_based);
if (spec_lemma->m_heq_result && !heq_proofs)
r = b.mk_eq_of_heq(r);
else if (!spec_lemma->m_heq_result && heq_proofs)
@ -1263,10 +1264,12 @@ expr congruence_closure::mk_congr_proof_core(name const & R, expr const & lhs, e
lean_assert(!lemma->m_heq_result);
r = b.lift_from_eq(R, r);
}
if (lemma->m_heq_result && !heq_proofs)
r = b.mk_eq_of_heq(r);
else if (!lemma->m_heq_result && heq_proofs)
r = b.mk_heq_of_eq(r);
if (g_heq_based) {
if (lemma->m_heq_result && !heq_proofs)
r = b.mk_eq_of_heq(r);
else if (!lemma->m_heq_result && heq_proofs)
r = b.mk_heq_of_eq(r);
}
return r;
}
} else {
@ -1458,10 +1461,12 @@ optional<expr> congruence_closure::get_eqv_proof(name const & R, expr const & e1
lhs = path2[i];
}
lean_assert(pr);
if (heq_proofs && R == get_eq_name())
pr = b.mk_eq_of_heq(*pr);
else if (!heq_proofs && R == get_heq_name())
pr = b.mk_heq_of_eq(*pr);
if (g_heq_based) {
if (heq_proofs && R == get_eq_name())
pr = b.mk_eq_of_heq(*pr);
else if (!heq_proofs && R == get_heq_name())
pr = b.mk_heq_of_eq(*pr);
}
return pr;
}