From 8e0888828d6040d2c1887808709032e440007442 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 23 Jan 2014 22:31:02 -0800
Subject: [PATCH] fix(library/simplifier): missing check in mk_hcongr_th

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/simplifier/simplifier.cpp |  6 ++++
 tests/lean/simp22.lean                | 46 +++++++++++++++++++++++++++
 tests/lean/simp22.lean.expected.out   | 32 +++++++++++++++++++
 3 files changed, 84 insertions(+)
 create mode 100644 tests/lean/simp22.lean
 create mode 100644 tests/lean/simp22.lean.expected.out

diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp
index d496eb45f..58b544f42 100644
--- a/src/library/simplifier/simplifier.cpp
+++ b/src/library/simplifier/simplifier.cpp
@@ -174,6 +174,10 @@ class simplifier_fn {
         return m_tc.is_proposition(e, m_ctx);
     }
 
+    bool is_convertible(expr const & t1, expr const & t2) {
+        return m_tc.is_convertible(t1, t2, m_ctx);
+    }
+
     bool is_definitionally_equal(expr const & t1, expr const & t2) {
         return m_tc.is_definitionally_equal(t1, t2, m_ctx);
     }
@@ -230,6 +234,8 @@ class simplifier_fn {
         expr const & new_A = abst_domain(new_f_type);
         expr a_type        = infer_type(a);
         expr new_a_type    = infer_type(new_a);
+        if (!is_convertible(new_a_type, new_A))
+            return none_expr(); // failed
         if (!is_definitionally_equal(A, a_type) || !is_definitionally_equal(new_A, new_a_type)) {
             if (Heq_a_is_heq) {
                 if (is_definitionally_equal(a_type, new_a_type) && is_definitionally_equal(A, new_A)) {
diff --git a/tests/lean/simp22.lean b/tests/lean/simp22.lean
new file mode 100644
index 000000000..c459e69e1
--- /dev/null
+++ b/tests/lean/simp22.lean
@@ -0,0 +1,46 @@
+import   cast
+variable vec    : Nat → Type
+variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
+infixl   65 ; : concat
+axiom    concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) :
+             (v1 ; v2) ; v3 = cast (congr2 vec (symm (Nat::add_assoc n1 n2 n3)))
+                              (v1 ; (v2 ; v3))
+variable empty : vec 0
+axiom    concat_empty {n : Nat} (v : vec n) :
+             v ; empty = cast (congr2 vec (symm (Nat::add_zeror n)))
+                         v
+
+rewrite_set simple
+-- The simplification rules used for Nat and Vectors should "mirror" each other.
+-- Concatenation is not commutative. So, by adding Nat::add_comm to the
+-- rewrite set, we prevent the simplifier from reducing the following example
+add_rewrite concat_assoc concat_empty Nat::add_assoc Nat::add_zeror Nat::add_comm : simple
+
+variable n : Nat
+variable v : vec n
+variable w : vec n
+variable f {A : TypeM} : A → A
+
+(*
+local t = parse_lean([[ f ((v ; w) ; empty ; (v ; empty)) ]])
+print(t)
+print("===>")
+local t2, pr = simplify(t, "simple")
+print(t2)
+print(pr)
+get_environment():type_check(pr)
+*)
+
+-- Now, if we disable Nat::add_comm, the simplifier works
+disable_rewrite Nat::add_comm : simple
+print "After disabling Nat::add_comm"
+
+(*
+local t = parse_lean([[ f ((v ; w) ; empty ; (v ; empty)) ]])
+print(t)
+print("===>")
+local t2, pr = simplify(t, "simple")
+print(t2)
+print(pr)
+get_environment():type_check(pr)
+*)
diff --git a/tests/lean/simp22.lean.expected.out b/tests/lean/simp22.lean.expected.out
new file mode 100644
index 000000000..45756fdd4
--- /dev/null
+++ b/tests/lean/simp22.lean.expected.out
@@ -0,0 +1,32 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'cast'
+  Assumed: vec
+  Assumed: concat
+  Assumed: concat_assoc
+  Assumed: empty
+  Assumed: concat_empty
+  Assumed: n
+  Assumed: v
+  Assumed: w
+  Assumed: f
+f (v ; w ; empty ; (v ; empty))
+===>
+f (v ; w ; empty ; (v ; empty))
+refl (f (v ; w ; empty ; (v ; empty)))
+After disabling Nat::add_comm
+f (v ; w ; empty ; (v ; empty))
+===>
+f (v ; (w ; v))
+hcongr (hcongr (hrefl @f)
+               (to_heq (subst (refl (vec (n + n + 0 + (n + 0))))
+                              (congr2 vec
+                                      (trans (congr (congr2 Nat::add (Nat::add_zeror (n + n))) (Nat::add_zeror n))
+                                             (Nat::add_assoc n n n))))))
+       (htrans (htrans (hcongr (hcongr (hcongr (hcongr (hrefl @concat) (to_heq (Nat::add_zeror (n + n))))
+                                               (to_heq (Nat::add_zeror n)))
+                                       (htrans (to_heq (concat_empty (v ; w)))
+                                               (cast_heq (congr2 vec (symm (Nat::add_zeror (n + n)))) (v ; w))))
+                               (htrans (to_heq (concat_empty v)) (cast_heq (congr2 vec (symm (Nat::add_zeror n))) v)))
+                       (to_heq (concat_assoc v w v)))
+               (cast_heq (congr2 vec (symm (Nat::add_assoc n n n))) (v ; (w ; v))))