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

fix(library/app_builder): make sure app_builder works even if iff is marked as reducible

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-04 13:51:56 -08:00
parent 93b17e2ec1
commit a8b6a286dd
2 changed files with 17 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/library/app_builder.cpp
View file

@ -342,11 +342,13 @@ struct app_builder::imp {
}
expr mk_iff_symm(expr const & H) {
expr p = m_ctx->whnf(m_ctx->infer(H));
expr p = m_ctx->infer(H);
expr lhs, rhs;
if (!is_iff(p, lhs, rhs))
throw app_builder_exception();
return ::lean::mk_app(mk_constant(get_iff_symm_name()), lhs, rhs, H);
if (is_iff(p, lhs, rhs)) {
return ::lean::mk_app(mk_constant(get_iff_symm_name()), lhs, rhs, H);
} else {
return mk_app(get_iff_symm_name(), {H});
}
}
expr mk_eq_trans(expr const & H1, expr const & H2) {
@ -361,12 +363,14 @@ struct app_builder::imp {
}
expr mk_iff_trans(expr const & H1, expr const & H2) {
expr p1 = m_ctx->whnf(m_ctx->infer(H1));
expr p2 = m_ctx->whnf(m_ctx->infer(H2));
expr p1 = m_ctx->infer(H1);
expr p2 = m_ctx->infer(H2);
expr lhs1, rhs1, lhs2, rhs2;
if (!is_iff(p1, lhs1, rhs1) || !is_iff(p2, lhs2, rhs2))
throw app_builder_exception();
return ::lean::mk_app({mk_constant(get_iff_trans_name()), lhs1, rhs1, rhs2, H1, H2});
if (is_iff(p1, lhs1, rhs1) && is_iff(p2, lhs2, rhs2)) {
return ::lean::mk_app({mk_constant(get_iff_trans_name()), lhs1, rhs1, rhs2, H1, H2});
} else {
return mk_app(get_iff_trans_name(), {H1, H2});
}
}
expr mk_rel(name const & n, expr const & lhs, expr const & rhs) {

4
tests/lean/run/blast_ematch10.lean Normal file
View file

@ -0,0 +1,4 @@
attribute iff [reducible]
example (p : nat → Prop) (a b c : nat) : p a → a = b → p b :=
by blast