From ddff37dd0f59963ae1d235bdc1c21bc2f5089a9f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 10 Jan 2016 19:28:55 -0800 Subject: [PATCH] fix(library/blast/congruence_closure): bug when using blast.cc.heq and handling relation congruences --- src/library/blast/congruence_closure.cpp | 19 ++++++++++++++++--- tests/lean/run/flycheck_blast_cc_heq7.lean | 5 +++++ 2 files changed, 21 insertions(+), 3 deletions(-) create mode 100644 tests/lean/run/flycheck_blast_cc_heq7.lean diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp index 7fdce1e42..62034786a 100644 --- a/src/library/blast/congruence_closure.cpp +++ b/src/library/blast/congruence_closure.cpp @@ -432,9 +432,15 @@ static optional mk_relation_congr_lemma(name const & R, expr co } } if (optional 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(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(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; } } } diff --git a/tests/lean/run/flycheck_blast_cc_heq7.lean b/tests/lean/run/flycheck_blast_cc_heq7.lean new file mode 100644 index 000000000..923af7aa4 --- /dev/null +++ b/tests/lean/run/flycheck_blast_cc_heq7.lean @@ -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