From 799317c43eed9f5b3382da1c098efbe73dd2a59c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 10 Jan 2016 18:03:35 -0800
Subject: [PATCH] fix(library/blast/congruence_closure): add missing eq => heq
 lifting

---
 src/library/blast/congruence_closure.cpp |  2 ++
 tests/lean/run/blast_cc_heq4.lean        | 34 +++++++++++++++++++++---
 2 files changed, 33 insertions(+), 3 deletions(-)

diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp
index 6b9795a029..7fdce1e420 100644
--- a/src/library/blast/congruence_closure.cpp
+++ b/src/library/blast/congruence_closure.cpp
@@ -1379,6 +1379,8 @@ expr congruence_closure::mk_congr_proof_core(name const & R, expr const & lhs, e
         }
         if (lemma->m_lift_needed)
             r = b.lift_from_eq(R, *r);
+        if (g_heq_based && heq_proofs)
+            r = b.mk_heq_of_eq(*r);
         return *r;
     }
 }
diff --git a/tests/lean/run/blast_cc_heq4.lean b/tests/lean/run/blast_cc_heq4.lean
index 708286a2ba..c42325d607 100644
--- a/tests/lean/run/blast_cc_heq4.lean
+++ b/tests/lean/run/blast_cc_heq4.lean
@@ -32,6 +32,34 @@ by blast
 example : a1 == x a2 → a2 == y a1 → mk_B1 (x (y a1)) == mk_B1 (x (y (x a2))) :=
 by blast
 
--- The following one needs subsingleton support
--- 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 blast
+-- The following examples need subsingleton equality propagation
+set_option blast.cc.subsingleton true
+
+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 blast
+
+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 blast
+
+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 blast
+
+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 blast
+
+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 blast
+
+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 blast
+
+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 blast