From 19bfbe2df83462f2cc2fe5d3c623d7a3f8cb41d2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 16 Jan 2016 19:53:36 -0800
Subject: [PATCH] fix(library/blast/congruence_closure): uselist initialization
 (aka add_occurrence)

Make sure it matches the description in the paper.
---
 src/library/blast/congruence_closure.cpp | 26 ++++++++++++++++--------
 tests/lean/run/blast_cc_heq9.lean        |  4 ++++
 tests/lean/run/blast_cc_missed.lean      | 13 ++++++++++++
 3 files changed, 35 insertions(+), 8 deletions(-)
 create mode 100644 tests/lean/run/blast_cc_missed.lean

diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp
index 499eb9f0ca..9827808415 100644
--- a/src/library/blast/congruence_closure.cpp
+++ b/src/library/blast/congruence_closure.cpp
@@ -999,8 +999,12 @@ void congruence_closure::internalize_core(name R, expr const & e, bool toplevel,
                 internalize_core(R, app_fn(e), toplevel, to_propagate);
                 internalize_core(R, app_arg(e), toplevel, to_propagate);
                 bool eq_table = true;
-                add_occurrence(R, e, R, app_fn(e), eq_table);
-                add_occurrence(R, e, R, app_arg(e), eq_table);
+                expr it = e;
+                while (is_app(it)) {
+                    add_occurrence(R, e, R, app_fn(it), eq_table);
+                    add_occurrence(R, e, R, app_arg(it), eq_table);
+                    it = app_fn(it);
+                }
                 add_eq_congruence_table(e);
             } else {
                 /* Handle user-defined congruence lemmas, congruence lemmas for other relations,
@@ -1419,12 +1423,18 @@ expr congruence_closure::mk_eq_congr_proof(expr const & lhs, expr const & rhs, b
     buffer<expr> lhs_args, rhs_args;
     expr const * lhs_it = &lhs;
     expr const * rhs_it = &rhs;
-    while (is_app(*lhs_it) && is_app(*rhs_it) && *lhs_it != *rhs_it) {
-        lean_assert(is_eqv(get_eq_name(), *lhs_it, *rhs_it));
-        lhs_args.push_back(app_arg(*lhs_it));
-        rhs_args.push_back(app_arg(*rhs_it));
-        lhs_it = &app_fn(*lhs_it);
-        rhs_it = &app_fn(*rhs_it);
+    if (lhs != rhs) {
+        while (true) {
+            lean_assert(is_eqv(get_eq_name(), *lhs_it, *rhs_it));
+            lhs_args.push_back(app_arg(*lhs_it));
+            rhs_args.push_back(app_arg(*rhs_it));
+            lhs_it = &app_fn(*lhs_it);
+            rhs_it = &app_fn(*rhs_it);
+            if (*lhs_it == *rhs_it)
+                break;
+            if (is_def_eq(infer_type(*lhs_it), infer_type(*rhs_it)))
+                break;
+        }
     }
     if (lhs_args.empty()) {
         if (heq_proofs)
diff --git a/tests/lean/run/blast_cc_heq9.lean b/tests/lean/run/blast_cc_heq9.lean
index 15c78b09f1..bf3818592b 100644
--- a/tests/lean/run/blast_cc_heq9.lean
+++ b/tests/lean/run/blast_cc_heq9.lean
@@ -5,6 +5,10 @@ example (f g : Π {A : Type₁}, A → A → A) (h : nat → nat) (a b : nat) :
         h = f a → h b = f a b :=
 by blast
 
+example (f g : Π {A : Type₁}, A → A → A) (h : nat → nat) (a b : nat) :
+        h = f a → h b = f a b :=
+by blast
+
 example (f g : Π {A : Type₁} (a b : A), {x : A | x ≠ b}) (h : Π (b : nat), {x : nat | x ≠ b}) (a b₁ b₂ : nat) :
         h = f a → b₁ = b₂ → h b₁ == f a b₂ :=
 by blast
diff --git a/tests/lean/run/blast_cc_missed.lean b/tests/lean/run/blast_cc_missed.lean
new file mode 100644
index 0000000000..c91cce5759
--- /dev/null
+++ b/tests/lean/run/blast_cc_missed.lean
@@ -0,0 +1,13 @@
+set_option blast.strategy "cc"
+
+example (C : nat → Type) (f : Π n, C n → C n) (n m : nat) (c : C n) (d : C m) :
+        f n == f m → c == d → n == m → f n c == f m d :=
+by blast
+
+example (f : nat → nat → nat) (a b c d : nat) :
+        c = d → f a = f b → f a c = f b d :=
+by blast
+
+example (f : nat → nat → nat) (a b c d : nat) :
+        c == d → f a == f b → f a c == f b d :=
+by blast