From 3f6b79227f3c1b6846530a8647d49bf7cb0b6fd7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 17 Nov 2015 18:57:40 -0800
Subject: [PATCH] 
 refactor(library/blast/congruence_closure,library/app_builder): add helper
 methods for theorems heavily used in the congruence closure module

---
 src/library/app_builder.cpp              | 44 ++++++++++++++++++++++++
 src/library/app_builder.h                | 11 ++++++
 src/library/blast/congruence_closure.cpp | 10 +++---
 3 files changed, 60 insertions(+), 5 deletions(-)

diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp
index 7af31a63f..b35127a12 100644
--- a/src/library/app_builder.cpp
+++ b/src/library/app_builder.cpp
@@ -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);
 }
diff --git a/src/library/app_builder.h b/src/library/app_builder.h
index ed52da54a..ff1825de2 100644
--- a/src/library/app_builder.h
+++ b/src/library/app_builder.h
@@ -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);
diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp
index 35df5582e..a67e84099 100644
--- a/src/library/blast/congruence_closure.cpp
+++ b/src/library/blast/congruence_closure.cpp
@@ -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();
         }