From 297ef106114bf477631d72b56cf76011d9c39c3f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 24 Jan 2016 14:28:43 -0800
Subject: [PATCH] fix(library/blast/congruence_closure): subsingleton
 propagation in the congruence closure module

We must normalize inferred type.
---
 src/library/blast/congruence_closure.cpp      |  6 +++---
 ...t_cc_subsingleton_normalization_issue.lean | 19 +++++++++++++++++++
 2 files changed, 22 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/blast_cc_subsingleton_normalization_issue.lean

diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp
index 7723d867b..5505f18ff 100644
--- a/src/library/blast/congruence_closure.cpp
+++ b/src/library/blast/congruence_closure.cpp
@@ -161,8 +161,8 @@ void congruence_closure::initialize() {
 }
 
 void congruence_closure::push_subsingleton_eq(expr const & a, expr const & b) {
-    expr A = infer_type(a);
-    expr B = infer_type(b);
+    expr A = normalize(infer_type(a));
+    expr B = normalize(infer_type(b));
     if (is_def_eq(A, B)) {
         // TODO(Leo): to improve performance we can create the following proof lazily
         bool heq_proof = false;
@@ -192,7 +192,7 @@ void congruence_closure::check_new_subsingleton_eq(expr const & old_root, expr c
 void congruence_closure::process_subsingleton_elem(expr const & e) {
     if (!g_propagate_subsingletons)
         return;
-    expr type = infer_type(e);
+    expr type = normalize(infer_type(e));
     optional<expr> ss = mk_subsingleton_instance(type);
     if (!ss)
         return; /* type is not a subsingleton */
diff --git a/tests/lean/run/blast_cc_subsingleton_normalization_issue.lean b/tests/lean/run/blast_cc_subsingleton_normalization_issue.lean
new file mode 100644
index 000000000..32f5b69de
--- /dev/null
+++ b/tests/lean/run/blast_cc_subsingleton_normalization_issue.lean
@@ -0,0 +1,19 @@
+import data.real
+open real
+
+namespace safe
+
+definition pos (x : ℝ) := x > 0
+constants (safe_log : Π (x : ℝ), pos x → ℝ)
+
+lemma pos_add {x y : ℝ} : pos x →  pos y → pos (x + y) := sorry
+lemma pos_mul {x y : ℝ} : pos x →  pos y → pos (x * y) := sorry
+
+set_option blast.strategy "cc"
+
+example (x y z w : ℝ)
+  (x_pos : pos x) (y_pos : pos y) (z_pos : pos z) (w_pos : pos w) :
+  x * y = z + w →  @safe_log (z + w) (pos_add z_pos w_pos) = @safe_log (x * y) (pos_mul x_pos y_pos) :=
+by blast -- fails
+
+end safe