From b92bbeb83b840a90e391e31f114c58877cfc3440 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Sep 2013 20:45:26 -0700 Subject: [PATCH] Add casting propagation and normalization Signed-off-by: Leonardo de Moura --- src/kernel/builtin.cpp | 120 ++++++++++++++++++++++++++++- src/kernel/builtin.h | 13 ++++ src/kernel/normalizer.cpp | 2 +- src/library/basic_thms.cpp | 18 ----- src/library/basic_thms.h | 12 --- tests/lean/cast3.lean | 23 ++++++ tests/lean/cast3.lean.expected.out | 27 +++++++ 7 files changed, 182 insertions(+), 33 deletions(-) create mode 100644 tests/lean/cast3.lean create mode 100644 tests/lean/cast3.lean.expected.out diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index 33faba62a..570cee0f7 100644 --- a/src/kernel/builtin.cpp +++ b/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 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 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 - env.add_var(cast_fn_name, Pi({{A, TypeU}, {B, TypeU}, {H, Eq(A,B)}, {a, A}}, B)); + // Alias for Cast operator. We create the alias to be able to mark + // 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))); } } diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h index afda22779..bab09ef62 100644 --- a/src/kernel/builtin.h +++ b/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); diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index 419de2218..0c28ef73e 100644 --- a/src/kernel/normalizer.cpp +++ b/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; } } diff --git a/src/library/basic_thms.cpp b/src/library/basic_thms.cpp index 06d45cf65..b00cd78bb 100644 --- a/src/library/basic_thms.cpp +++ b/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)}}, diff --git a/src/library/basic_thms.h b/src/library/basic_thms.h index 4c45d92f6..281582897 100644 --- a/src/library/basic_thms.h +++ b/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); } diff --git a/tests/lean/cast3.lean b/tests/lean/cast3.lean new file mode 100644 index 000000000..dd536e07f --- /dev/null +++ b/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)) + diff --git a/tests/lean/cast3.lean.expected.out b/tests/lean/cast3.lean.expected.out new file mode 100644 index 000000000..7c20a4f07 --- /dev/null +++ b/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