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

fix(library/blast/congruence_closure): bug when using blast.cc.heq and handling relation congruences

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-10 19:28:55 -08:00
parent 2b38d0fe9b
commit ddff37dd0f
2 changed files with 21 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -432,9 +432,15 @@ static optional<ext_congr_lemma> mk_relation_congr_lemma(name const & R, expr co
}
}
if (optional<congr_lemma> cgr = mk_rel_eq_congr(fn)) {
bool heq_proof = false;
if (g_heq_based && R == get_heq_name()) {
heq_proof = true;
}
auto child_rel_names = rel_names_from_arg_kinds(cgr->get_arg_kinds(), const_name(fn));
bool lift_needed = R != get_eq_name();
return optional<ext_congr_lemma>(R, *cgr, child_rel_names, lift_needed);
ext_congr_lemma r(R, *cgr, child_rel_names, lift_needed);
r.m_heq_result = heq_proof;
return optional<ext_congr_lemma>(r);
}
}
}
@ -1332,7 +1338,6 @@ expr congruence_closure::mk_congr_proof_core(name const & R, expr const & lhs, e
}
expr r = mk_app(lemma->m_congr_lemma.get_proof(), lemma_args);
if (lemma->m_lift_needed) {
lean_assert(!lemma->m_heq_result);
r = b.lift_from_eq(R, r);
}
if (g_heq_based) {
@ -1406,7 +1411,15 @@ expr congruence_closure::mk_congr_proof(name const & R, expr const & e1, expr co
if (R != get_eq_name())
e1_eqv_new_e1 = b.lift_from_eq(R, e1_eqv_new_e1);
}
return b.mk_trans(R, e1_eqv_new_e1, mk_congr_proof_core(R, new_e1, e2, heq_proofs));
bool cgr_heq_proofs = g_heq_based && R == get_heq_name();
expr r = b.mk_trans(R, e1_eqv_new_e1, mk_congr_proof_core(R, new_e1, e2, cgr_heq_proofs));
if (g_heq_based) {
if (cgr_heq_proofs && !heq_proofs)
r = b.mk_eq_of_heq(r);
else if (!cgr_heq_proofs && heq_proofs)
r = b.mk_heq_of_eq(r);
}
return r;
}
}
}

5
tests/lean/run/flycheck_blast_cc_heq7.lean Normal file
View file

@ -0,0 +1,5 @@
set_option blast.cc.heq true
set_option trace.app_builder true
definition t3 (a b : nat) : (a = b) == (b = a) :=
by blast