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

feat(library/blast/congruence_closure): avoid eq.rec if major premise is eq.refl

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-21 18:59:07 -08:00
parent 607552e51f
commit 5e9914ef45
2 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/app_builder.cpp
View file

@ -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))

7
tests/lean/run/blast_cc10.lean Normal file
View file

@ -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