Add casting propagation and normalization

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

src/kernel/builtin.cpp

@@ -141,6 +141,99 @@ public:
 MK_BUILTIN(if_fn, if_fn_value);
 // =======================================
 
+// =======================================
+// cast builtin operator
+static name   g_cast_name("Cast");
+static format g_cast_fmt(g_cast_name);
+expr mk_Cast_fn();
+class cast_fn_value : public value {
+    expr m_type;
+public:
+    cast_fn_value() {
+        expr A    = Const("A");
+        expr B    = Const("B");
+        // Cast: Pi (A : Type u) (B : Type u) (H : A = B) (a : A), B
+        m_type = Pi({{A, TypeU}, {B, TypeU}}, Eq(A,B) >> (A >> B));
+    }
+    virtual ~cast_fn_value() {}
+    virtual expr get_type() const { return m_type; }
+    virtual name get_name() const { return g_cast_name; }
+    virtual bool normalize(unsigned num_as, expr const * as, expr & r) const {
+        if (num_as > 4 && as[1] == as[2]) {
+            // Cast T T H a == a
+            if (num_as == 5)
+                r = as[4];
+            else
+                r = mk_app(num_as - 4, as + 4);
+            return true;
+        } else if (is_app(as[4]) &&
+                   arg(as[4], 0) == mk_Cast_fn() &&
+                   num_args(as[4]) == 5 &&
+                   as[1] == arg(as[4], 2)) {
+            // Cast T1 T2 H1 (Cast T3 T1 H2 a) == Cast T3 T2 (Trans H1 H2) a
+            expr const & nested = as[4];
+            expr const & T1 = as[1];
+            expr const & T2 = as[2];
+            expr const & T3 = arg(nested, 1);
+            expr const & H1 = as[3];
+            expr const & H2 = arg(nested, 3);
+            expr const & a  = arg(nested, 4);
+            expr c = Cast(T3, T2, Trans(TypeU, T3, T1, T2, H1, H2), a);
+            if (num_as == 5) {
+                r = c;
+            } else {
+                buffer<expr> new_as;
+                new_as.push_back(c);
+                new_as.append(num_as - 5, as + 5);
+                r = mk_app(new_as.size(), new_as.data());
+            }
+            return true;
+        } else if (num_as > 5 && is_pi(as[1]) && is_pi(as[2])) {
+            // cast T1 T2 H f a_1 ... a_k
+            // Propagate application over cast.
+            // Remark: we check if T1 is a Pi to prevent non-termination
+            // For example, H can be a bogus hypothesis that shows
+            // that A == A -> A
+
+            // Since T1 and T2 are Pi's, we decompose them
+            expr const & T1  = as[1]; // Pi x : A1, B1
+            expr const & T2  = as[2]; // Pi x : A2, B2
+            expr const & H   = as[3];
+            expr const & f   = as[4];
+            expr const & a_1 = as[5]; // has type A2
+            expr const & A1  = abst_domain(T1);
+            expr const & B1  = abst_body(T1);
+            expr const & A2  = abst_domain(T2);
+            expr const & B2  = abst_body(T2);
+            expr B1f         = mk_lambda(abst_name(T1), A1, B1);
+            expr B2f         = mk_lambda(abst_name(T2), A2, B2);
+            expr A1_eq_A2    = DomInj(A1, A2, B1f, B2f, H);
+            name t("t");
+            expr A2_eq_A1    = Symm(TypeU, A1, A2, A1_eq_A2);
+            expr a_1p        = Cast(A2, A1, A2_eq_A1, a_1);
+            expr fa_1        = f(a_1p);
+            // Cast fa_1 back to B2 since the type of cast T1 T2 H f a_1
+            // is in B2 a_1p
+            expr B1_eq_B2_at_a_1p = RanInj(A1, A2, B1f, B2f, H, a_1p);
+            expr fa_1_B2     = Cast(B1, B2, B1_eq_B2_at_a_1p, fa_1);
+            if (num_as == 6) {
+                r = fa_1_B2;
+            } else {
+                buffer<expr> new_as;
+                new_as.push_back(fa_1_B2);
+                new_as.append(num_as - 6, as + 6);
+                r = mk_app(new_as.size(), new_as.data());
+            }
+            return true;
+        } else {
+            return false;
+        }
+    }
+};
+MK_BUILTIN(Cast_fn, cast_fn_value);
+// =======================================
+
+
 MK_CONSTANT(implies_fn, name("implies"));
 MK_CONSTANT(iff_fn,     name("iff"));
 MK_CONSTANT(and_fn,     name("and"));
@@ -162,6 +255,11 @@ MK_CONSTANT(imp_antisym_fn, name("ImpAntisym"));
 MK_CONSTANT(dom_inj_fn,     name("DomInj"));
 MK_CONSTANT(ran_inj_fn,     name("RanInj"));
 
+// Basic theorems
+MK_CONSTANT(symm_fn,            name("Symm"));
+MK_CONSTANT(trans_fn,           name("Trans"));
+MK_CONSTANT(trans_ext_fn,       name("TransExt"));
+
 void add_basic_theory(environment & env) {
     env.add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION);
     env.add_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION);
@@ -171,6 +269,7 @@ void add_basic_theory(environment & env) {
     expr f         = Const("f");
     expr a         = Const("a");
     expr b         = Const("b");
+    expr c         = Const("c");
     expr x         = Const("x");
     expr y         = Const("y");
     expr A         = Const("A");
@@ -191,6 +290,7 @@ void add_basic_theory(environment & env) {
     env.add_builtin(mk_bool_value(true));
     env.add_builtin(mk_bool_value(false));
     env.add_builtin(mk_if_fn());
+    env.add_builtin(mk_Cast_fn());
 
     // implies(x, y) := if x y True
     env.add_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True)));
@@ -215,8 +315,9 @@ void add_basic_theory(environment & env) {
     // homogeneous equality
     env.add_definition(homo_eq_fn_name, Pi({{A,TypeU},{x,A},{y,A}}, Bool), Fun({{A,TypeU}, {x,A}, {y,A}}, Eq(x, y)));
 
-    // Cast: Pi (A : Type u) (B : Type u) (H : A = B) (a : A), B
+    // Alias for Cast operator. We create the alias to be able to mark
-    env.add_var(cast_fn_name, Pi({{A, TypeU}, {B, TypeU}, {H, Eq(A,B)}, {a, A}}, B));
+    // implicit arguments.
+    env.add_definition(cast_fn_name, Pi({{A, TypeU}, {B, TypeU}}, Eq(A,B) >> (A >> B)), mk_Cast_fn());
 
     // MP : Pi (a b : Bool) (H1 : a => b) (H2 : a), b
     env.add_axiom(mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, a}}, b));
@@ -246,5 +347,20 @@ void add_basic_theory(environment & env) {
     //                     B a = B' (cast A A' (DomInj A A' B B' H) a)
     env.add_axiom(ran_inj_fn_name, Pi({{A, TypeU}, {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H, Eq(piABx, piApBpx)}, {a, A}},
                                       Eq(B(a), Bp(Cast(A, Ap, DomInj(A, Ap, B, Bp, H), a)))));
+
+    // Symm : Pi (A : Type u) (a b : A) (H : a = b), b = a
+    env.add_theorem(symm_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}}, Eq(b, a)),
+                    Fun({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}},
+                        Subst(A, a, b, Fun({x, A}, Eq(x,a)), Refl(A, a), H)));
+
+    // Trans: Pi (A: Type u) (a b c : A) (H1 : a = b) (H2 : b = c), a = c
+    env.add_theorem(trans_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)),
+                    Fun({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a,b)}, {H2, Eq(b,c)}},
+                        Subst(A, b, c, Fun({x, A}, Eq(a, x)), H1, H2)));
+
+    // TransExt: Pi (A: Type u) (B : Type u) (a : A) (b c : B) (H1 : a = b) (H2 : b = c), a = c
+    env.add_theorem(trans_ext_fn_name, Pi({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {c, B}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)),
+                    Fun({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {c, B}, {H1, Eq(a, b)}, {H2, Eq(b, c)}},
+                        Subst(B, b, c, Fun({x, B}, Eq(a, x)), H1, H2)));
 }
 }

src/kernel/builtin.h

@@ -168,6 +168,19 @@ expr mk_ran_inj_fn();
 inline expr mk_ran_inj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H, expr const & a) { return mk_app({mk_ran_inj_fn(), A, Ap, B, Bp, H, a}); }
 inline expr RanInj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H, expr const & a) { return mk_ran_inj(A, Ap, B, Bp, H, a); }
 
+expr mk_symm_fn();
+/** \brief (Theorem) {A : Type u}, {a b : A}, H : a = b |- Symm(A, a, b, H) : b = a */
+inline expr Symm(expr const & A, expr const & a, expr const & b, expr const & H) { return mk_app(mk_symm_fn(), A, a, b, H); }
+
+expr mk_trans_fn();
+/** \brief (Theorem) {A : Type u}, {a b c : A}, H1 : a = b, H2 : b = c |- Trans(A, a, b, c, H1, H2) : a = c */
+inline expr Trans(expr const & A, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) { return mk_app({mk_trans_fn(), A, a, b, c, H1, H2}); }
+
+expr mk_trans_ext_fn();
+/** \brief (Theorem) {A : Type u}, {B : Type u}, {a : A}, {b c : B}, H1 : a = b, H2 : b = c |- TransExt(A, B, a, b, c, H1, H2) : a = c */
+inline expr TransExt(expr const & A, expr const & B, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) { return mk_app({mk_trans_ext_fn(), A, B, a, b, c, H1, H2}); }
+
+
 class environment;
 /** \brief Initialize the environment with basic builtin declarations and axioms */
 void add_basic_theory(environment & env);

src/kernel/normalizer.cpp

@@ -184,7 +184,7 @@ class normalizer::imp {
                     if (is_value(new_f)) {
                         expr m;
                         if (to_value(new_f).normalize(new_args.size(), new_args.data(), m)) {
-                            r = svalue(m);
+                            r = normalize(m, s, k);
                             break;
                         }
                     }

src/library/basic_thms.cpp

@@ -30,9 +30,6 @@ MK_CONSTANT(conjunct2_fn,       name("Conjunct2"));
 MK_CONSTANT(disj1_fn,           name("Disj1"));
 MK_CONSTANT(disj2_fn,           name("Disj2"));
 MK_CONSTANT(disj_cases_fn,      name("DisjCases"));
-MK_CONSTANT(symm_fn,            name("Symm"));
-MK_CONSTANT(trans_fn,           name("Trans"));
-MK_CONSTANT(trans_ext_fn,       name("TransExt"));
 MK_CONSTANT(congr1_fn,          name("Congr1"));
 MK_CONSTANT(congr2_fn,          name("Congr2"));
 MK_CONSTANT(congr_fn,           name("Congr"));
@@ -197,21 +194,6 @@ void add_basic_thms(environment & env) {
                                                         MT(a, c, Discharge(a, c, H2), H))),
                                                   H))))));
 
-    // Symm : Pi (A : Type u) (a b : A) (H : a = b), b = a
-    env.add_theorem(symm_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}}, Eq(b, a)),
-                    Fun({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}},
-                        Subst(A, a, b, Fun({x, A}, Eq(x,a)), Refl(A, a), H)));
-
-    // Trans: Pi (A: Type u) (a b c : A) (H1 : a = b) (H2 : b = c), a = c
-    env.add_theorem(trans_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)),
-                    Fun({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a,b)}, {H2, Eq(b,c)}},
-                        Subst(A, b, c, Fun({x, A}, Eq(a, x)), H1, H2)));
-
-    // TransExt: Pi (A: Type u) (B : Type u) (a : A) (b c : B) (H1 : a = b) (H2 : b = c), a = c
-    env.add_theorem(trans_ext_fn_name, Pi({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {c, B}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)),
-                    Fun({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {c, B}, {H1, Eq(a, b)}, {H2, Eq(b, c)}},
-                        Subst(B, b, c, Fun({x, B}, Eq(a, x)), H1, H2)));
-
     // EqTElim : Pi (a : Bool) (H : a = True), a
     env.add_theorem(eqt_elim_fn_name, Pi({{a, Bool}, {H, Eq(a, True)}}, a),
                     Fun({{a, Bool}, {H, Eq(a, True)}},

src/library/basic_thms.h

@@ -84,18 +84,6 @@ expr mk_disj_cases_fn();
 /** \brief (Theorem) {a b c : Bool}, H1 : Or(a,b), H2 : a -> c, H3 : b -> c |- DisjCases(a, b, c, H1, H2, H3) : c */
 inline expr DisjCases(expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2, expr const & H3) { return mk_app({mk_disj_cases_fn(), a, b, c, H1, H2, H3}); }
 
-expr mk_symm_fn();
-/** \brief (Theorem) {A : Type u}, {a b : A}, H : a = b |- Symm(A, a, b, H) : b = a */
-inline expr Symm(expr const & A, expr const & a, expr const & b, expr const & H) { return mk_app(mk_symm_fn(), A, a, b, H); }
-
-expr mk_trans_fn();
-/** \brief (Theorem) {A : Type u}, {a b c : A}, H1 : a = b, H2 : b = c |- Trans(A, a, b, c, H1, H2) : a = c */
-inline expr Trans(expr const & A, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) { return mk_app({mk_trans_fn(), A, a, b, c, H1, H2}); }
-
-expr mk_trans_ext_fn();
-/** \brief (Theorem) {A : Type u}, {B : Type u}, {a : A}, {b c : B}, H1 : a = b, H2 : b = c |- TransExt(A, B, a, b, c, H1, H2) : a = c */
-inline expr TransExt(expr const & A, expr const & B, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) { return mk_app({mk_trans_ext_fn(), A, B, a, b, c, H1, H2}); }
-
 expr mk_eqt_elim_fn();
 /** \brief (Theorem) {a : Bool}, H : a = True |- EqTElim(a, H) : a */
 inline expr EqTElim(expr const & a, expr const & H) { return mk_app(mk_eqt_elim_fn(), a, H); }

tests/lean/cast3.lean

@@ -0,0 +1,23 @@
+Variables A A' B B' : Type
+Variable x : A
+Eval cast (Refl A) x
+Eval x = (cast (Refl A) x)
+Variable b : B
+Definition f (x : A) : B := b
+Axiom H : A -> B = A' -> B
+Variable a' : A'
+Eval (cast H f) a'
+Axiom H2 : A -> B = A' -> B'
+Definition g (x : B') : Nat := 0
+Eval g ((cast H2 f) a')
+Check g ((cast H2 f) a')
+
+Eval (cast H2 f) a'
+
+Variables A1 A2 A3 : Type
+Axiom Ha : A1 = A2
+Axiom Hb : A2 = A3
+Variable a : A1
+Eval (cast Hb (cast Ha a))
+Check (cast Hb (cast Ha a))
+

tests/lean/cast3.lean.expected.out

@@ -0,0 +1,27 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: A
+  Assumed: A'
+  Assumed: B
+  Assumed: B'
+  Assumed: x
+x
+⊤
+  Assumed: b
+  Defined: f
+  Assumed: H
+  Assumed: a'
+b
+  Assumed: H2
+  Defined: g
+0
+ℕ
+Cast B B' (RanInj H2 (Cast A' A (Symm (DomInj H2)) a')) b
+  Assumed: A1
+  Assumed: A2
+  Assumed: A3
+  Assumed: Ha
+  Assumed: Hb
+  Assumed: a
+Cast A1 A3 (Trans Hb Ha) a
+A3