From 7ccbf0eb025ebad6bb202fb6dd140ad22089766f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 29 Dec 2016 11:24:36 -0800
Subject: [PATCH] feat(library/tactic/congruence/theory_ac): add collapse
 transition

---
 src/library/tactic/congruence/theory_ac.cpp   | 30 ++++++++++++++++++-
 src/library/tactic/congruence/theory_ac.h     |  4 +++
 .../run/{cc_ac_support.lean => cc_ac1.lean}   |  0
 tests/lean/run/cc_ac2.lean                    |  4 +++
 4 files changed, 37 insertions(+), 1 deletion(-)
 rename tests/lean/run/{cc_ac_support.lean => cc_ac1.lean} (100%)
 create mode 100644 tests/lean/run/cc_ac2.lean

diff --git a/src/library/tactic/congruence/theory_ac.cpp b/src/library/tactic/congruence/theory_ac.cpp
index 41d5802890..735a0e0437 100644
--- a/src/library/tactic/congruence/theory_ac.cpp
+++ b/src/library/tactic/congruence/theory_ac.cpp
@@ -519,6 +519,11 @@ void theory_ac::insert_R_occs(expr const & lhs, expr const & rhs) {
     insert_R_occs(rhs, lhs, false);
 }
 
+void theory_ac::erase_R_occs(expr const & lhs, expr const & rhs) {
+    erase_R_occs(lhs, lhs, true);
+    erase_R_occs(rhs, lhs, false);
+}
+
 /*
   Given, e is of the form lhs*r, (H : lhs = rhs),
   return (rhs*r) and proof ac_simp_pr(e, lhs, rhs, r, rhs*r, H) : e = rhs*r
@@ -633,7 +638,30 @@ void theory_ac::compose(expr const & lhs, expr const & rhs, expr const & H) {
 }
 
 void theory_ac::collapse(expr const & lhs, expr const & rhs, expr const & H) {
-    // TODO(Leo)
+    expr x           = m_state.get_var_with_least_lhs_occs(lhs);
+    occurrences occs = m_state.m_entries.find(x)->get_R_lhs_occs();
+    occs.for_each([&](expr const & R_lhs) {
+            if (is_ac_subset(lhs, R_lhs)) {
+                expr R_rhs, R_H;
+                std::tie(R_rhs, R_H) = *m_state.m_R.find(R_lhs);
+                erase_R_occs(R_lhs, R_rhs);
+                m_state.m_R.erase(R_lhs);
+                expr new_R_lhs, R_lhs_eq_new_R_lhs;
+                std::tie(new_R_lhs, R_lhs_eq_new_R_lhs) = simplify_core(R_lhs, lhs, rhs, H);
+                expr new_R_lhs_eq_R_lhs = mk_eq_symm(m_ctx, R_lhs, new_R_lhs, R_lhs_eq_new_R_lhs);
+                expr new_R_H            = mk_eq_trans(m_ctx, new_R_lhs, R_lhs, R_rhs, new_R_lhs_eq_R_lhs, R_H);
+                m_todo.emplace_back(new_R_lhs, R_rhs, new_R_H);
+                lean_trace(name({"debug", "cc", "ac"}), scope_trace_env s(m_ctx.env(), m_ctx);
+                           auto out      = tout();
+                           auto fmt      = out.get_formatter();
+                           format new_rw = group(paren(pp_term(fmt, lhs) + line() + format("-->") + line() + pp_term(fmt, rhs)));
+                           format old_rw = group(paren(pp_term(fmt, R_rhs) + line() + format("<--") + line() + pp_term(fmt, R_lhs)));
+                           format r      = format("collapse:");
+                           r += nest(get_pp_indent(fmt.get_options()), line() + group(new_rw + line() + format("at") + line() + old_rw) +
+                                     line() + format(":=") + line() + pp_term(fmt, new_R_lhs));
+                           out << group(r) << "\n";);
+            }
+        });
 }
 
 void theory_ac::superpose(expr const & lhs, expr const & rhs, expr const & H) {
diff --git a/src/library/tactic/congruence/theory_ac.h b/src/library/tactic/congruence/theory_ac.h
index bc66572a88..91c5602a95 100644
--- a/src/library/tactic/congruence/theory_ac.h
+++ b/src/library/tactic/congruence/theory_ac.h
@@ -83,6 +83,9 @@ public:
         expr get_var_with_least_rhs_occs(expr const & e) const {
             return get_var_with_least_occs(e, false);
         }
+        expr get_var_with_least_lhs_occs(expr const & e) const {
+            return get_var_with_least_occs(e, true);
+        }
     };
 
 private:
@@ -102,6 +105,7 @@ private:
     void erase_R_rhs_occs(expr const & e, expr const & lhs) { erase_R_occs(e, lhs, false); }
     void insert_R_rhs_occs(expr const & e, expr const & lhs) { insert_R_occs(e, lhs, false); }
     void insert_R_occs(expr const & lhs, expr const & rhs);
+    void erase_R_occs(expr const & lhs, expr const & rhs);
     void compose(expr const & lhs, expr const & rhs, expr const & H);
     void collapse(expr const & lhs, expr const & rhs, expr const & H);
     void superpose(expr const & lhs, expr const & rhs, expr const & H);
diff --git a/tests/lean/run/cc_ac_support.lean b/tests/lean/run/cc_ac1.lean
similarity index 100%
rename from tests/lean/run/cc_ac_support.lean
rename to tests/lean/run/cc_ac1.lean
diff --git a/tests/lean/run/cc_ac2.lean b/tests/lean/run/cc_ac2.lean
new file mode 100644
index 0000000000..97f989f066
--- /dev/null
+++ b/tests/lean/run/cc_ac2.lean
@@ -0,0 +1,4 @@
+open tactic
+
+example (a b c d : nat) (f : nat → nat → nat) : b + a = d → f (a + b + c) a = f (c + d) a :=
+by cc