From c1afefb87363f9e4e3095729f7b33dc193e93949 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 5 Dec 2013 19:00:31 -0800
Subject: [PATCH] feat(library/fo_unify): unify heterogeneous - homogeneous
 equality

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/expr.cpp      | 10 ++++++++++
 src/kernel/expr.h        |  2 ++
 src/library/fo_unify.cpp | 13 ++++++++++---
 3 files changed, 22 insertions(+), 3 deletions(-)

diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 3b7933bb7..ceb92a2cf 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -232,6 +232,16 @@ bool is_arrow(expr const & t) {
     return is_pi(t) && !has_free_var(abst_body(t), 0);
 }
 
+bool is_eq(expr const & e, expr & lhs, expr & rhs) {
+    if (is_eq(e)) {
+        lhs = eq_lhs(e);
+        rhs = eq_rhs(e);
+        return true;
+    } else {
+        return false;
+    }
+}
+
 expr copy(expr const & a) {
     switch (a.kind()) {
     case expr_kind::Var:      return mk_var(var_idx(a));
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 4fd952b55..7fe13d27a 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -504,6 +504,8 @@ inline name const &  metavar_name(expr const & e)         { return to_metavar(e)
 inline local_context const & metavar_lctx(expr const & e) { return to_metavar(e)->get_lctx(); }
 
 inline bool has_metavar(expr const & e) { return e.has_metavar(); }
+
+bool is_eq(expr const & e, expr & lhs, expr & rhs);
 // =======================================
 
 // =======================================
diff --git a/src/library/fo_unify.cpp b/src/library/fo_unify.cpp
index 32aec3ac3..a5a65b3ac 100644
--- a/src/library/fo_unify.cpp
+++ b/src/library/fo_unify.cpp
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <utility>
+#include "kernel/builtin.h"
 #include "library/fo_unify.h"
 #include "library/expr_pair.h"
 #include "library/kernel_bindings.h"
@@ -19,11 +20,16 @@ static bool is_metavar_wo_local_context(expr const & e) {
     return is_metavar(e) && !metavar_lctx(e);
 }
 
+static bool is_eq_heq(expr const & e, expr & lhs, expr & rhs) {
+    return is_eq(e, lhs, rhs) || is_homo_eq(e, lhs, rhs);
+}
+
 optional<substitution> fo_unify(expr e1, expr e2) {
     lean_assert(e1);
     lean_assert(e2);
     substitution s;
     unsigned i;
+    expr lhs1, rhs1, lhs2, rhs2;
     buffer<expr_pair> todo;
     todo.emplace_back(e1, e2);
     while (!todo.empty()) {
@@ -36,6 +42,9 @@ optional<substitution> fo_unify(expr e1, expr e2) {
                 assign(s, e1, e2);
             } else if (is_metavar_wo_local_context(e2)) {
                 assign(s, e2, e1);
+            } else if (is_eq_heq(e1, lhs1, rhs1) && is_eq_heq(e2, lhs2, rhs2)) {
+                todo.emplace_back(lhs1, lhs2);
+                todo.emplace_back(rhs1, rhs2);
             } else {
                 if (e1.kind() != e2.kind())
                     return optional<substitution>();
@@ -52,9 +61,7 @@ optional<substitution> fo_unify(expr e1, expr e2) {
                     }
                     break;
                 case expr_kind::Eq:
-                    todo.emplace_back(eq_rhs(e1), eq_rhs(e2));
-                    todo.emplace_back(eq_lhs(e1), eq_lhs(e2));
-                    break;
+                    lean_unreachable(); break; // LCOV_EXCL_LINE
                 case expr_kind::Lambda: case expr_kind::Pi:
                     todo.emplace_back(abst_body(e1), abst_body(e2));
                     todo.emplace_back(abst_domain(e1), abst_domain(e2));