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

refactor(library/blast/congruence_closure,library/app_builder): add helper methods for theorems heavily used in the congruence closure module

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-17 18:57:40 -08:00
parent 3de9a89d93
commit 3f6b79227f
3 changed files with 60 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

44
src/library/app_builder.cpp
View file

@ -469,6 +469,31 @@ struct app_builder::imp {
return mk_app(get_congr_name(), {H1, H2});
}
expr mk_iff_false_intro(expr const & H) {
// TODO(Leo): implement custom version if bottleneck.
return mk_app(get_iff_false_intro_name(), {H});
}
expr mk_iff_true_intro(expr const & H) {
// TODO(Leo): implement custom version if bottleneck.
return mk_app(get_iff_true_intro_name(), {H});
}
expr mk_not_of_iff_false(expr const & H) {
// TODO(Leo): implement custom version if bottleneck.
return mk_app(get_not_of_iff_false_name(), {H});
}
expr mk_of_iff_true(expr const & H) {
// TODO(Leo): implement custom version if bottleneck.
return mk_app(get_of_iff_true_name(), {H});
}
expr mk_false_of_true_iff_false(expr const & H) {
// TODO(Leo): implement custom version if bottleneck.
return mk_app(get_false_of_true_iff_false_name(), {H});
}
expr mk_partial_add(expr const & A) {
level lvl = get_level(A);
auto A_has_add = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_has_add_name(), {lvl}), A));
@ -612,6 +637,25 @@ expr app_builder::mk_congr(expr const & H1, expr const & H2) {
return m_ptr->mk_congr(H1, H2);
}
expr app_builder::mk_iff_false_intro(expr const & H) {
return m_ptr->mk_iff_false_intro(H);
}
expr app_builder::mk_iff_true_intro(expr const & H) {
return m_ptr->mk_iff_true_intro(H);
}
expr app_builder::mk_not_of_iff_false(expr const & H) {
return m_ptr->mk_not_of_iff_false(H);
}
expr app_builder::mk_of_iff_true(expr const & H) {
return m_ptr->mk_of_iff_true(H);
}
expr app_builder::mk_false_of_true_iff_false(expr const & H) {
return m_ptr->mk_false_of_true_iff_false(H);
}
expr app_builder::mk_partial_add(expr const & A) {
return m_ptr->mk_partial_add(A);
}

11
src/library/app_builder.h
View file

@ -115,6 +115,17 @@ public:
expr mk_congr_fun(expr const & H, expr const & a);
expr mk_congr(expr const & H1, expr const & H2);
/** \brief not p -> (p <-> false) */
expr mk_iff_false_intro(expr const & H);
/** \brief p -> (p <-> true) */
expr mk_iff_true_intro(expr const & H);
/** \brief (p <-> false) -> not p */
expr mk_not_of_iff_false(expr const & H);
/** \brief (p <-> true) -> p */
expr mk_of_iff_true(expr const & H);
/** \brief (true <-> false) -> false */
expr mk_false_of_true_iff_false(expr const & H);
expr mk_partial_add(expr const & A);
expr mk_partial_mul(expr const & A);
expr mk_zero(expr const & A);

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

@ -246,7 +246,7 @@ void congruence_closure::add(hypothesis_idx hidx) {
if (is_relation_app(p, R, lhs, rhs)) {
if (is_neg) {
internalize(get_iff_name(), p);
add_eqv(get_iff_name(), p, mk_false(), b.mk_app(get_iff_false_intro_name(), h->get_self()));
add_eqv(get_iff_name(), p, mk_false(), b.mk_iff_false_intro(h->get_self()));
} else {
internalize(R, lhs);
internalize(R, rhs);
@ -255,9 +255,9 @@ void congruence_closure::add(hypothesis_idx hidx) {
} else if (is_prop(p)) {
internalize(get_iff_name(), p);
if (is_neg) {
add_eqv(get_iff_name(), p, mk_false(), b.mk_app(get_iff_false_intro_name(), h->get_self()));
add_eqv(get_iff_name(), p, mk_false(), b.mk_iff_false_intro(h->get_self()));
} else {
add_eqv(get_iff_name(), p, mk_true(), b.mk_app(get_iff_true_intro_name(), h->get_self()));
add_eqv(get_iff_name(), p, mk_true(), b.mk_iff_true_intro(h->get_self()));
}
}
} catch (app_builder_exception &) {}
@ -294,7 +294,7 @@ optional<expr> congruence_closure::get_uneqv_proof(name const & R, expr const &
// TODO(Leo): check if this is a bootleneck
expr tmp = b.mk_rel(R, e1, e2);
if (auto p = get_eqv_proof(get_iff_name(), tmp, mk_false())) {
return some_expr(b.mk_app(get_not_of_iff_false_name(), *p));
return some_expr(b.mk_not_of_iff_false(*p));
} else {
return none_expr();
}
@ -311,7 +311,7 @@ optional<expr> congruence_closure::get_inconsistency_proof() const {
try {
app_builder & b = get_app_builder();
if (auto p = get_eqv_proof(get_iff_name(), mk_true(), mk_false())) {
return some_expr(b.mk_app(get_false_of_true_iff_false_name(), *p));
return some_expr(b.mk_false_of_true_iff_false(*p));
} else {
return none_expr();
}