From 5e9914ef45505249bc8d950849784420ace925d2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 21 Nov 2015 18:59:07 -0800 Subject: [PATCH] feat(library/blast/congruence_closure): avoid eq.rec if major premise is eq.refl --- src/library/app_builder.cpp | 4 ++++ tests/lean/run/blast_cc10.lean | 7 +++++++ 2 files changed, 11 insertions(+) create mode 100644 tests/lean/run/blast_cc10.lean diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index 644a1141b..21d2f7be7 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -441,6 +441,8 @@ struct app_builder::imp { } expr mk_eq_rec(expr const & motive, expr const & H1, expr const & H2) { + if (is_constant(get_app_fn(H2), get_eq_refl_name())) + return H1; expr p = m_ctx->whnf(m_ctx->infer(H2)); expr lhs, rhs; if (!is_eq(p, lhs, rhs)) @@ -456,6 +458,8 @@ struct app_builder::imp { } expr mk_eq_drec(expr const & motive, expr const & H1, expr const & H2) { + if (is_constant(get_app_fn(H2), get_eq_refl_name())) + return H1; expr p = m_ctx->whnf(m_ctx->infer(H2)); expr lhs, rhs; if (!is_eq(p, lhs, rhs)) diff --git a/tests/lean/run/blast_cc10.lean b/tests/lean/run/blast_cc10.lean new file mode 100644 index 000000000..a11b62670 --- /dev/null +++ b/tests/lean/run/blast_cc10.lean @@ -0,0 +1,7 @@ +set_option blast.subst false +set_option blast.simp false + +definition t1 (a b : nat) : (a = b ↔ a = b) := +by blast + +print t1