From 21c54755a974fce0c4cfd15d880e8d5e9216f5a9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Jun 2014 14:09:12 -0700
Subject: [PATCH] fix(kernel/converter): bug in is_def_eq

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/converter.cpp          |  7 ++++---
 tests/lean/bug1.lean              | 24 ++++++++++++++++++++++++
 tests/lean/bug1.lean.expected.out | 13 +++++++++++++
 3 files changed, 41 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/bug1.lean
 create mode 100644 tests/lean/bug1.lean.expected.out

diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp
index 8b880bb71..f28e299f4 100644
--- a/src/kernel/converter.cpp
+++ b/src/kernel/converter.cpp
@@ -279,15 +279,16 @@ struct default_converter : public converter {
         expr_kind k = t.kind();
         buffer<expr> subst;
         do {
-            expr var_t_type = instantiate(binding_domain(t), subst.size(), subst.data());
-            expr var_s_type = instantiate(binding_domain(s), subst.size(), subst.data());
+            expr var_t_type = instantiate_rev(binding_domain(t), subst.size(), subst.data());
+            expr var_s_type = instantiate_rev(binding_domain(s), subst.size(), subst.data());
             if (!is_def_eq(var_t_type, var_s_type, c, jst))
                 return false;
             subst.push_back(mk_local(c.mk_fresh_name(), binding_name(s), var_s_type));
             t = binding_body(t);
             s = binding_body(s);
         } while (t.kind() == k && s.kind() == k);
-        return is_def_eq(instantiate(t, subst.size(), subst.data()), instantiate(s, subst.size(), subst.data()), c, jst);
+        return is_def_eq(instantiate_rev(t, subst.size(), subst.data()),
+                         instantiate_rev(s, subst.size(), subst.data()), c, jst);
     }
 
     /** \brief This is an auxiliary method for is_def_eq. It handles the "easy cases". */
diff --git a/tests/lean/bug1.lean b/tests/lean/bug1.lean
new file mode 100644
index 000000000..a0421b26e
--- /dev/null
+++ b/tests/lean/bug1.lean
@@ -0,0 +1,24 @@
+definition [inline] bool : Type.{1}           := Type.{0}
+definition [inline] and  (p q : bool) : bool  := ∀ c : bool, (p → q → c) → c
+infixl `∧` 25 := and
+
+variable a : bool
+
+-- Error
+theorem and_intro (p q : bool) (H1 : p) (H2 : q) : a
+:= fun (c : bool) (H : p -> q -> c), H H1 H2
+
+-- Error
+theorem and_intro (p q : bool) (H1 : p) (H2 : q) : p ∧ p
+:= fun (c : bool) (H : p -> q -> c), H H1 H2
+
+-- Error
+theorem and_intro (p q : bool) (H1 : p) (H2 : q) : q ∧ p
+:= fun (c : bool) (H : p -> q -> c), H H1 H2
+
+-- Correct
+theorem and_intro (p q : bool) (H1 : p) (H2 : q) : p ∧ q
+:= fun (c : bool) (H : p -> q -> c), H H1 H2
+
+check and_intro
+
diff --git a/tests/lean/bug1.lean.expected.out b/tests/lean/bug1.lean.expected.out
new file mode 100644
index 000000000..962bdf903
--- /dev/null
+++ b/tests/lean/bug1.lean.expected.out
@@ -0,0 +1,13 @@
+bug1.lean:9:7: error: type mismatch at definition 'and_intro', expected type
+    Pi (p : bool) (q : bool) (H1 : p) (H2 : q), a
+given type:
+    Pi (p : bool) (q : bool) (H1 : p) (H2 : q) (c : bool) (H : p -> q -> c), c
+bug1.lean:13:7: error: type mismatch at definition 'and_intro', expected type
+    Pi (p : bool) (q : bool) (H1 : p) (H2 : q), (and p p)
+given type:
+    Pi (p : bool) (q : bool) (H1 : p) (H2 : q) (c : bool) (H : p -> q -> c), c
+bug1.lean:17:7: error: type mismatch at definition 'and_intro', expected type
+    Pi (p : bool) (q : bool) (H1 : p) (H2 : q), (and q p)
+given type:
+    Pi (p : bool) (q : bool) (H1 : p) (H2 : q) (c : bool) (H : p -> q -> c), c
+and_intro : Pi (p : bool) (q : bool) (H1 : p) (H2 : q), (and p q)