From 9d273d924fbdc6e323be44e3bedca74751c4b5de Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 8 Jan 2017 00:36:57 -0800
Subject: [PATCH] fix(library/tactic/smt/congruence_closure): must check
 whether constructors have the same type or not

---
 src/library/tactic/smt/congruence_closure.cpp |  9 +++-
 tests/lean/run/smt_ematch3.lean               | 45 +++++++++++++++++++
 2 files changed, 53 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/smt_ematch3.lean

diff --git a/src/library/tactic/smt/congruence_closure.cpp b/src/library/tactic/smt/congruence_closure.cpp
index 3cd9627a30..27a7699c5b 100644
--- a/src/library/tactic/smt/congruence_closure.cpp
+++ b/src/library/tactic/smt/congruence_closure.cpp
@@ -1253,6 +1253,13 @@ void congruence_closure::propagate_constructor_eq(expr const & e1, expr const &
     optional<name> c1 = is_constructor_app(env(), e1);
     optional<name> c2 = is_constructor_app(env(), e2);
     lean_assert(c1 && c2);
+    if (!m_ctx.is_def_eq(m_ctx.infer(e1), m_ctx.infer(e2))) {
+        /* The implications above only hold if the types are equal.
+
+           TODO(Leo): if the types are different, we may still propagate by searching the equivalence
+           classes of e1 and e2 for other constructors that may have compatible types. */
+        return;
+    }
     expr type       = mk_eq(m_ctx, e1, e2);
     expr h          = *get_eq_proof(e1, e2);
     if (*c1 == *c2) {
@@ -1885,7 +1892,7 @@ void congruence_closure::add_eqv_step(expr e1, expr e2, expr const & H, bool heq
                auto fmt = out.get_formatter();
                out << "merged: " << e1_root << " = " << e2_root << "\n";
                out << m_state.pp_eqcs(fmt) << "\n";
-               out << m_state.pp_parent_occs(fmt) << "\n";
+               // out << m_state.pp_parent_occs(fmt) << "\n";
                out << "--------\n";);
 }
 
diff --git a/tests/lean/run/smt_ematch3.lean b/tests/lean/run/smt_ematch3.lean
new file mode 100644
index 0000000000..a442f82a00
--- /dev/null
+++ b/tests/lean/run/smt_ematch3.lean
@@ -0,0 +1,45 @@
+open nat
+notation `⟦`:max a `⟧`:0 := cast (by simp) a
+
+inductive vector (α : Type) : nat → Type
+| nil {} : vector 0
+| cons   : Π {n}, α → vector n → vector (succ n)
+
+namespace vector
+local attribute [simp] add_succ succ_add add_comm
+
+variable {α : Type}
+
+def app : Π {n m : nat}, vector α n → vector α m → vector α (n + m)
+| 0        m nil        w := ⟦ w ⟧
+| (succ n) m (cons a v) w := ⟦ cons a (app v w) ⟧
+
+lemma app_nil_right {n : nat} (v : vector α n) : app v nil == v :=
+begin induction v, reflexivity, {[smt] ematch_using [app, add_comm, zero_add, add_zero] }, end
+
+def smt_cfg : smt_config :=
+{ default_smt_config with cc_cfg := {default_cc_config with ac := ff}}
+
+lemma app_assoc {n₁ n₂ n₃ : nat} (v₁ : vector α n₁) (v₂ : vector α n₂) (v₃ : vector α n₃) :
+                     app v₁ (app v₂ v₃) == app (app v₁ v₂) v₃ :=
+begin
+  intros,
+  induction v₁,
+  {[smt] ematch_using [app, zero_add] },
+  {[smt] with smt_cfg, repeat { ematch_using [app, add_succ, succ_add, add_comm, add_assoc] }}
+end
+
+def rev : Π {n : nat}, vector α n → vector α n
+| 0     nil         := nil
+| (n+1) (cons x xs) := app (rev xs) (cons x nil)
+
+lemma rev_app : ∀ {n₁ n₂ : nat} (v₁ : vector α n₁) (v₂ : vector α n₂),
+  rev (app v₁ v₂) == app (rev v₂) (rev v₁) :=
+begin
+  intros,
+  induction v₁,
+  {[smt] repeat {ematch_using [app, rev, zero_add, add_zero, add_comm, app_nil_right]}},
+  {[smt] repeat {ematch_using [app, rev, zero_add, add_zero, add_comm, app_assoc, add_one_eq_succ]} }
+end
+
+end vector