From 424a6acb684ac8fae1a5b64f9679cfbe0741db45 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 24 Dec 2016 08:43:04 -0800
Subject: [PATCH] fix(library/tactic/congruence/congruence_closure): missing
 proof construction step

---
 .../tactic/congruence/congruence_closure.cpp  | 13 +++-
 tests/lean/run/cc5.lean                       | 61 +++++++++++++++++++
 2 files changed, 73 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/cc5.lean

diff --git a/src/library/tactic/congruence/congruence_closure.cpp b/src/library/tactic/congruence/congruence_closure.cpp
index 1b7739fd91..2b520c34a1 100644
--- a/src/library/tactic/congruence/congruence_closure.cpp
+++ b/src/library/tactic/congruence/congruence_closure.cpp
@@ -864,7 +864,18 @@ expr congruence_closure::mk_congr_proof_core(expr const & lhs, expr const & rhs,
             r = mk_eq_of_heq(m_ctx, r);
         else if (!lemma->m_heq_result && heq_proofs)
             r = mk_heq_of_eq(m_ctx, r);
-        return r;
+        if (lhs_fn == rhs_fn ||
+            m_ctx.is_def_eq(lhs_fn, rhs_fn))
+            return r;
+        /* Convert r into a proof of lhs = rhs using eq.rec and
+           the proof that lhs_fn = rhs_fn */
+        expr lhs_fn_eq_rhs_fn = *get_eq_proof(lhs_fn, rhs_fn);
+        type_context::tmp_locals locals(m_ctx);
+        expr x                = locals.push_local("_x", m_ctx.infer(lhs_fn));
+        expr motive_rhs       = mk_app(x, rhs_args);
+        expr motive           = heq_proofs ? mk_heq(m_ctx, lhs, motive_rhs) : mk_eq(m_ctx, lhs, motive_rhs);
+        motive                = locals.mk_lambda(motive);
+        return mk_eq_rec(m_ctx, motive, r, lhs_fn_eq_rhs_fn);
     } else {
         /* This branch builds congruence proofs that handle equality between functions.
            The proof is created using congr_arg/congr_fun/congr lemmas.
diff --git a/tests/lean/run/cc5.lean b/tests/lean/run/cc5.lean
new file mode 100644
index 0000000000..6c661f01ac
--- /dev/null
+++ b/tests/lean/run/cc5.lean
@@ -0,0 +1,61 @@
+universes l1 l2 l3 l4 l5 l6
+constants (A : Type l1) (B : A → Type l2) (C : ∀ (a : A) (ba : B a), Type l3)
+          (D : ∀ (a : A) (ba : B a) (cba : C a ba), Type l4)
+          (E : ∀ (a : A) (ba : B a) (cba : C a ba) (dcba : D a ba cba), Type l5)
+          (F : ∀ (a : A) (ba : B a) (cba : C a ba) (dcba : D a ba cba) (edcba : E a ba cba dcba), Type l6)
+          (C_ss : ∀ a ba, subsingleton (C a ba))
+          (a1 a2 a3 : A)
+          (mk_B1 mk_B2 : ∀ a, B a)
+          (mk_C1 mk_C2 : ∀ {a} ba, C a ba)
+
+          (tr_B : ∀ {a}, B a → B a)
+          (x y z : A → A)
+
+          (f f' : ∀ {a : A} {ba : B a} (cba : C a ba), D a ba cba)
+          (g : ∀ {a : A} {ba : B a} {cba : C a ba} (dcba : D a ba cba), E a ba cba dcba)
+          (h : ∀ {a : A} {ba : B a} {cba : C a ba} {dcba : D a ba cba} (edcba : E a ba cba dcba), F a ba cba dcba edcba)
+
+
+attribute [instance] C_ss
+open tactic
+
+example : ∀ (a a' : A), a == a' → mk_B1 a == mk_B1 a' :=
+by cc
+
+example : ∀ (a a' : A), a == a' → mk_B2 a == mk_B2 a' :=
+by cc
+
+example : a1 == y a2 → mk_B1 a1 == mk_B1 (y a2) :=
+by cc
+
+example : a1 == x a2 → a2 == y a1 → mk_B1 (x (y a1)) == mk_B1 (x (y (x a2))) :=
+by cc
+
+example : a1 == y a2 → mk_B1 a1 == mk_B2 (y a2) → f (mk_C1 (mk_B2 a1)) == f (mk_C2 (mk_B1 (y a2))) :=
+by cc
+
+example : a1 == y a2 → tr_B (mk_B1 a1) == mk_B2 (y a2) → f (mk_C1 (mk_B2 a1)) == f (mk_C2 (tr_B (mk_B1 (y a2)))) :=
+by cc
+
+example : a1 == y a2 → mk_B1 a1 == mk_B2 (y a2) → g (f (mk_C1 (mk_B2 a1))) == g (f (mk_C2 (mk_B1 (y a2)))) :=
+by cc
+
+example : a1 == y a2 → tr_B (mk_B1 a1) == mk_B2 (y a2) → g (f (mk_C1 (mk_B2 a1))) == g (f (mk_C2 (tr_B (mk_B1 (y a2))))) :=
+by cc
+
+example : a1 == y a2 → a2 == z a3 → a3 == x a1 → mk_B1 a1 == mk_B2 (y (z (x a1))) →
+          f (mk_C1 (mk_B2 (y (z (x a1))))) == f' (mk_C2 (mk_B1 a1)) →
+          g (f (mk_C1 (mk_B2 (y (z (x a1)))))) == g (f' (mk_C2 (mk_B1 a1))) :=
+by cc
+
+example : a1 == y a2 → a2 == z a3 → a3 == x a1 → mk_B1 a1 == mk_B2 (y (z (x a1))) →
+          f (mk_C1 (mk_B2 (y (z (x a1))))) == f' (mk_C2 (mk_B1 a1)) →
+          f' (mk_C1 (mk_B1 a1)) == f (mk_C2 (mk_B2 (y (z (x a1))))) →
+          g (f (mk_C1 (mk_B1 (y (z (x a1)))))) == g (f' (mk_C2 (mk_B2 a1))) :=
+by cc
+
+example : a1 == y a2 → a2 == z a3 → a3 == x a1 → tr_B (mk_B1 a1) == mk_B2 (y (z (x a1))) →
+          f (mk_C1 (mk_B2 (y (z (x a1))))) == f' (mk_C2 (tr_B (mk_B1 a1))) →
+          f' (mk_C1 (tr_B (mk_B1 a1))) == f (mk_C2 (mk_B2 (y (z (x a1))))) →
+          g (f (mk_C1 (tr_B (mk_B1 (y (z (x a1))))))) == g (f' (mk_C2 (mk_B2 a1))) :=
+by cc