fix(library/simplifier): bug in cast elimination

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

src/library/simplifier/simplifier.cpp

@@ -347,6 +347,8 @@ class simplifier_fn {
     result simplify_app(expr const & e) {
         if (m_has_cast && is_cast(e)) {
             // e is of the form (cast A B H a)
+            //   a : A
+            //   e : B
             expr A = arg(e, 1);
             expr B = arg(e, 2);
             expr H = arg(e, 3);
@@ -358,11 +360,11 @@ class simplifier_fn {
                     expr Hec;
                     expr Hac = *res_a.m_proof;
                     if (!res_a.m_heq_proof) {
-                        Hec = ::lean::mk_htrans_th(A, B, B, e, a, c,
+                        Hec = ::lean::mk_htrans_th(B, A, A, e, a, c,
                                                    update_app(e, 0, mk_cast_heq_fn()),  // cast A B H a == a
                                                    mk_to_heq_th(B, a, c, Hac));         // a == c
                     } else {
-                        Hec = ::lean::mk_htrans_th(A, B, infer_type(c), e, a, c,
+                        Hec = ::lean::mk_htrans_th(B, A, infer_type(c), e, a, c,
                                                    update_app(e, 0, mk_cast_heq_fn()),  // cast A B H a == a
                                                    Hac);                                // a == c
                     }

tests/lean/simp23.lean

@@ -0,0 +1,32 @@
+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
+add_rewrite concat_assoc concat_empty Nat::add_assoc Nat::add_zeror and_truer eq_id : simple
+
+variable n : Nat
+variable v : vec n
+variable w : vec n
+variable f {A : TypeM} : A → A
+variable p {A : TypeM} : A → Bool
+axiom fax {n m : Nat} (v : vec n) (w : vec m) : f (v; (w; v)) = v; (w; v)
+add_rewrite fax : simple
+
+(*
+local t = parse_lean([[ p (f ((v ; w) ; empty ; (v ; empty))) ∧ v = cast (congr2 vec (Nat::add_zeror n)) (v ; empty) ]])
+print(t)
+print("===>")
+local t2, pr = simplify(t, "simple")
+print(t2)
+print("checking proof")
+print (get_environment():type_check(pr))
+*)

tests/lean/simp23.lean.expected.out

@@ -0,0 +1,19 @@
+  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
+  Assumed: p
+  Assumed: fax
+p (f (v ; w ; empty ; (v ; empty))) ∧ v = cast (congr2 vec (Nat::add_zeror n)) (v ; empty)
+===>
+p (v ; (w ; v))
+checking proof
+(p (f (v ; w ; empty ; (v ; empty))) ∧ v = cast (congr2 vec (Nat::add_zeror n)) (v ; empty)) == p (v ; (w ; v))