fix(kernel/converter): bug in is_def_eq

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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". */

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
+

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)