From e42b616438be39258c6c8e4347e2e34aed5b4e3c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 8 Jan 2014 19:06:28 -0800
Subject: [PATCH] fix(kernel/normalizer): equality between semantic attachments

Given a heterogenous equality:  a == b
The normalizer will only reduce it if a and b are objects of the same kind.
Now, 1 == true is not reduced to false anymore.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 doc/lean/expr.md                 | 13 ++++++-------
 src/kernel/normalizer.cpp        |  2 +-
 tests/lean/eq4.lean              |  8 ++++++++
 tests/lean/eq4.lean.expected.out | 10 ++++++++++
 4 files changed, 25 insertions(+), 8 deletions(-)
 create mode 100644 tests/lean/eq4.lean
 create mode 100644 tests/lean/eq4.lean.expected.out

diff --git a/doc/lean/expr.md b/doc/lean/expr.md
index eb0e3e731..95752bb4d 100644
--- a/doc/lean/expr.md
+++ b/doc/lean/expr.md
@@ -69,18 +69,17 @@ eval 1 == 2
 eval 2 == 2
 ```
 
-Since we can compare elements of different types, the following expression is type correct and evaluates to `false`.
+Since we can compare elements of different types, the following
+expression is type correct, but Lean normalizer/evaluator will *not*
+reduce it.
 
 ```lean
-eval 1 == true
+eval 2 == true
 ```
 
-This is consistent with the set theoretic semantics used in Lean, where the interpretation of all expressions are sets.
-The interpretation of heterogeneous equality is just set equality in the Lean seamtics.
-
 We strongly discourage users from directly using heterogeneous equality. The main problem is that it is very easy to
-write expressions that are false like the one above. The expression `t = s` is a homogeneous equality.
-It expects `t` and `s` to have the same type. Thus, the expression `1 = true` is type incorrect in Lean.
+write nonsensical expressions like the one above. The expression `t = s` is a homogeneous equality.
+It expects `t` and `s` to have the same type. Thus, the expression `2 = true` is type incorrect in Lean.
 The symbol `=` is just notation. Internally, homogeneous equality is defined as:
 
 ```
diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp
index 4ca30d523..56924293c 100644
--- a/src/kernel/normalizer.cpp
+++ b/src/kernel/normalizer.cpp
@@ -312,7 +312,7 @@ class normalizer::imp {
         case expr_kind::Eq: {
             expr new_lhs = normalize(eq_lhs(a), s, k);
             expr new_rhs = normalize(eq_rhs(a), s, k);
-            if (is_value(new_lhs) && is_value(new_rhs) && !is_closure(new_lhs) && !is_closure(new_rhs)) {
+            if (is_value(new_lhs) && is_value(new_rhs) && !is_closure(new_lhs) && !is_closure(new_rhs) && typeid(to_value(new_lhs)) == typeid(to_value(new_rhs))) {
                 r = mk_bool_value(new_lhs == new_rhs);
             } else {
                 r = mk_eq(new_lhs, new_rhs);
diff --git a/tests/lean/eq4.lean b/tests/lean/eq4.lean
new file mode 100644
index 000000000..bc350f2dc
--- /dev/null
+++ b/tests/lean/eq4.lean
@@ -0,0 +1,8 @@
+import Int
+eval 1 == true
+eval 1 == 1.0
+eval 1 == nat_to_int 1
+eval true == 1.0
+eval Nat::add == 1
+eval Nat::add == Nat::mul
+eval Int::add == Int::mul
diff --git a/tests/lean/eq4.lean.expected.out b/tests/lean/eq4.lean.expected.out
new file mode 100644
index 000000000..f825c0158
--- /dev/null
+++ b/tests/lean/eq4.lean.expected.out
@@ -0,0 +1,10 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'Int'
+1 == ⊤
+1 == 1
+1 == 1
+⊤ == 1
+Nat::add == 1
+Nat::add == Nat::mul
+Int::add == Int::mul