From 26bea7772109d17d44ded14812ffceec2b79df76 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 Jan 2014 19:02:17 -0800 Subject: [PATCH] fix(library/simplifier): bug in heterogeneous equality support, and universe commutativity support in the simplifier Signed-off-by: Leonardo de Moura --- src/kernel/type_checker.cpp | 6 +- src/kernel/type_checker.h | 7 +- src/library/simplifier/simplifier.cpp | 94 ++++++++++++++++++++------- tests/lean/simp19.lean | 29 +++++++++ tests/lean/simp19.lean.expected.out | 27 ++++++++ tests/lean/simp20.lean | 20 ++++++ tests/lean/simp20.lean.expected.out | 13 ++++ 7 files changed, 165 insertions(+), 31 deletions(-) create mode 100644 tests/lean/simp19.lean create mode 100644 tests/lean/simp19.lean.expected.out create mode 100644 tests/lean/simp20.lean create mode 100644 tests/lean/simp20.lean.expected.out diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index bee563c993..dead83e808 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -407,7 +407,7 @@ public: return is_convertible(t1, t2, ctx, mk_justification); } - bool is_eq_convertible(expr const & t1, expr const & t2, context const & ctx) { + bool is_definitionally_equal(expr const & t1, expr const & t2, context const & ctx) { set_ctx(ctx); update_menv(none_menv()); if (t1 == t2) @@ -500,8 +500,8 @@ expr type_checker::check(expr const & e, context const & ctx) { bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx) { return m_ptr->is_convertible(t1, t2, ctx); } -bool type_checker::is_eq_convertible(expr const & t1, expr const & t2, context const & ctx) { - return m_ptr->is_eq_convertible(t1, t2, ctx); +bool type_checker::is_definitionally_equal(expr const & t1, expr const & t2, context const & ctx) { + return m_ptr->is_definitionally_equal(t1, t2, ctx); } void type_checker::check_type(expr const & e, context const & ctx) { m_ptr->check_type(e, ctx); diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 2edb24f746..d91b52f452 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -86,12 +86,11 @@ public: /** \brief Return true iff \c t1 is convertible to \c t2 in the context \c ctx. */ bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context()); - /** \brief Return true iff \c t1 is convertible to \c t2 in the context \c ctx, but does not consider - universe commutativity. + /** \brief Return true iff \c t1 definitionally equal to \c t2 in the context \c ctx. - \remark is_eq_convertible(t1, t2, ctx) implies is_convertible(t1, t2, ctx) + \remark is_definitionally_equal(t1, t2, ctx) implies is_convertible(t1, t2, ctx) */ - bool is_eq_convertible(expr const & t1, expr const & t2, context const & ctx = context()); + bool is_definitionally_equal(expr const & t1, expr const & t2, context const & ctx = context()); /** \brief Return true iff \c e is a proposition (i.e., it has type Bool) */ bool is_proposition(expr const & e, context const & ctx, optional const & menv); diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp index 4c47156c27..d496eb45f2 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -100,6 +100,7 @@ unsigned get_simplifier_max_steps(options const & opts) { return opts.get_unsign static name g_local("local"); static name g_C("C"); +static name g_x("x"); static name g_unique = name::mk_internal_unique_name(); class simplifier_fn { @@ -157,19 +158,24 @@ class simplifier_fn { ~updt_rule_set() { m_rs = m_old; } }; + + static expr mk_lambda(name const & n, expr const & d, expr const & b) { + return ::lean::mk_lambda(n, d, b); + } + /** \brief Return a lambda with body \c new_body, and name and domain from abst. */ static expr mk_lambda(expr const & abst, expr const & new_body) { - return ::lean::mk_lambda(abst_name(abst), abst_domain(abst), new_body); + return mk_lambda(abst_name(abst), abst_domain(abst), new_body); } bool is_proposition(expr const & e) { return m_tc.is_proposition(e, m_ctx); } - bool is_eq_convertible(expr const & t1, expr const & t2) { - return m_tc.is_eq_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); } expr infer_type(expr const & e) { @@ -185,32 +191,63 @@ class simplifier_fn { return proc(e, m_ctx, true); } + /** + \brief Auxiliary method for converting a proof H of (@eq A a b) into (@eq B a b) when + type A is convertible to B, but not definitionally equal. + */ + expr translate_eq_proof(expr const & A, expr const & a, expr const & b, expr const & H, expr const & B) { + return mk_subst_th(A, a, b, mk_lambda(g_x, A, mk_eq(B, a, mk_var(0))), mk_refl_th(B, a), H); + } + expr mk_congr1_th(expr const & f_type, expr const & f, expr const & new_f, expr const & a, expr const & Heq_f) { expr const & A = abst_domain(f_type); expr B = lower_free_vars(abst_body(f_type), 1, 1); return ::lean::mk_congr1_th(A, B, f, new_f, a, Heq_f); } - expr mk_congr2_th(expr const & f_type, expr const & a, expr const & new_a, expr const & f, expr const & Heq_a) { + expr mk_congr2_th(expr const & f_type, expr const & a, expr const & new_a, expr const & f, expr Heq_a) { expr const & A = abst_domain(f_type); expr B = lower_free_vars(abst_body(f_type), 1, 1); + expr a_type = infer_type(a); + if (!is_definitionally_equal(A, a_type)) + Heq_a = translate_eq_proof(a_type, a, new_a, Heq_a, A); return ::lean::mk_congr2_th(A, B, a, new_a, f, Heq_a); } expr mk_congr_th(expr const & f_type, expr const & f, expr const & new_f, expr const & a, expr const & new_a, - expr const & Heq_f, expr const & Heq_a) { + expr const & Heq_f, expr Heq_a) { expr const & A = abst_domain(f_type); expr B = lower_free_vars(abst_body(f_type), 1, 1); + expr a_type = infer_type(a); + if (!is_definitionally_equal(A, a_type)) + Heq_a = translate_eq_proof(a_type, a, new_a, Heq_a, A); return ::lean::mk_congr_th(A, B, f, new_f, a, new_a, Heq_f, Heq_a); } - expr mk_hcongr_th(expr const & f_type, expr const & new_f_type, expr const & f, expr const & new_f, - expr const & a, expr const & new_a, expr const & Heq_f, expr const & Heq_a) { - return ::lean::mk_hcongr_th(abst_domain(f_type), - abst_domain(new_f_type), - mk_lambda(f_type, abst_body(f_type)), - mk_lambda(new_f_type, abst_body(new_f_type)), - f, new_f, a, new_a, Heq_f, Heq_a); + optional mk_hcongr_th(expr const & f_type, expr const & new_f_type, expr const & f, expr const & new_f, + expr const & a, expr const & new_a, expr const & Heq_f, expr Heq_a, bool Heq_a_is_heq) { + expr const & A = abst_domain(f_type); + 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_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)) { + Heq_a = mk_to_eq_th(a_type, a, new_a, Heq_a); + Heq_a_is_heq = false; + } else { + return none_expr(); // we don't know how to handle this case + } + } + Heq_a = translate_eq_proof(a_type, a, new_a, Heq_a, A); + } + if (!Heq_a_is_heq) + Heq_a = mk_to_heq_th(A, a, new_a, Heq_a); + return some_expr(::lean::mk_hcongr_th(A, + new_A, + mk_lambda(f_type, abst_body(f_type)), + mk_lambda(new_f_type, abst_body(new_f_type)), + f, new_f, a, new_a, Heq_f, Heq_a)); } /** @@ -354,7 +391,7 @@ class simplifier_fn { lean_assert(rhs.m_proof); expr lhs_type = infer_type(lhs); expr rhs_type = infer_type(rhs.m_out); - if (is_eq_convertible(lhs_type, rhs_type)) { + if (is_definitionally_equal(lhs_type, rhs_type)) { // move back to homogeneous equality using to_eq rhs.m_proof = mk_to_eq_th(lhs_type, lhs, rhs.m_out, *rhs.m_proof); return true; @@ -434,7 +471,7 @@ class simplifier_fn { proof_args[info.get_pos_at_proof()] = a; proof_args[*info.get_new_pos_at_proof()] = new_args[pos]; name C_name(g_C, m_contextual_depth); // H_name is a cryptic unique name - proof_args[*info.get_proof_pos_at_proof()] = ::lean::mk_lambda(C_name, H, abstract(get_proof(res_a), H_proof)); + proof_args[*info.get_proof_pos_at_proof()] = mk_lambda(C_name, H, abstract(get_proof(res_a), H_proof)); } } if (new_args[pos] != a) @@ -533,10 +570,11 @@ class simplifier_fn { } else if (m_has_heq && (heq_proofs[i] || !is_arrow(f_types[i-1]))) { expr f = mk_app_prefix(i, new_args); expr pr_i = *proofs[i]; - if (!heq_proofs[i]) - pr_i = mk_to_heq_th(abst_domain(f_types[i-1]), arg(e, i), new_args[i], pr_i); - pr = mk_hcongr_th(f_types[i-1], f_types[i-1], f, f, arg(e, i), new_args[i], - mk_hrefl_th(f_types[i-1], f), pr_i); + auto new_pr = mk_hcongr_th(f_types[i-1], f_types[i-1], f, f, arg(e, i), new_args[i], + mk_hrefl_th(f_types[i-1], f), pr_i, heq_proofs[i]); + if (!new_pr) + return rewrite_app(e, result(e)); // failed to create congruence proof + pr = *new_pr; heq_proof = true; } else { expr f = mk_app_prefix(i, new_args); @@ -551,17 +589,25 @@ class simplifier_fn { if (m_has_heq && heq_proofs[i]) { if (!heq_proof) pr = mk_to_heq_th(f_types[i], f, new_f, pr); - pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, arg(e, i), new_args[i], pr, pr_i); + auto new_pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, arg(e, i), new_args[i], pr, pr_i, true); + if (!new_pr) + return rewrite_app(e, result(e)); // failed to create congruence proof + pr = *new_pr; heq_proof = true; } else if (heq_proof) { - pr_i = mk_to_heq_th(abst_domain(f_types[i-1]), arg(e, i), new_args[i], pr_i); - pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, arg(e, i), new_args[i], pr, pr_i); + auto new_pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, arg(e, i), new_args[i], pr, pr_i, heq_proofs[i]); + if (!new_pr) + return rewrite_app(e, result(e)); // failed to create congruence proof + pr = *new_pr; } else { pr = mk_congr_th(f_types[i-1], f, new_f, arg(e, i), new_args[i], pr, pr_i); } } else if (heq_proof) { - pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, arg(e, i), arg(e, i), - pr, mk_hrefl_th(abst_domain(f_types[i-1]), arg(e, i))); + auto new_pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, arg(e, i), arg(e, i), + pr, mk_refl_th(infer_type(arg(e, i)), arg(e, i)), false); + if (!new_pr) + return rewrite_app(e, result(e)); // failed to create congruence proof + pr = *new_pr; } else { lean_assert(!heq_proof); pr = mk_congr1_th(f_types[i-1], f, new_f, arg(e, i), pr); @@ -828,7 +874,7 @@ class simplifier_fn { } new_rhs = lower_free_vars(new_rhs, 1, 1); expr new_rhs_type = ensure_pi(infer_type(new_rhs)); - if (m_tc.is_eq_convertible(abst_domain(new_rhs_type), abst_domain(rhs.m_out), m_ctx)) { + if (m_tc.is_definitionally_equal(abst_domain(new_rhs_type), abst_domain(rhs.m_out), m_ctx)) { if (m_proofs_enabled) { expr new_proof = mk_eta_th(abst_domain(rhs.m_out), mk_lambda(rhs.m_out, abst_body(new_rhs_type)), diff --git a/tests/lean/simp19.lean b/tests/lean/simp19.lean new file mode 100644 index 0000000000..24780bef37 --- /dev/null +++ b/tests/lean/simp19.lean @@ -0,0 +1,29 @@ +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 : 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) +*) diff --git a/tests/lean/simp19.lean.expected.out b/tests/lean/simp19.lean.expected.out new file mode 100644 index 0000000000..e9f7dd999e --- /dev/null +++ b/tests/lean/simp19.lean.expected.out @@ -0,0 +1,27 @@ + 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 ; 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)))) diff --git a/tests/lean/simp20.lean b/tests/lean/simp20.lean new file mode 100644 index 0000000000..f400ea93ce --- /dev/null +++ b/tests/lean/simp20.lean @@ -0,0 +1,20 @@ +import cast +rewrite_set simple + +set_option pp::implicit true + +variable g : TypeM → TypeM +variable B : Type +variable B' : Type +axiom H : B = B' +add_rewrite H : simple + +(* +local t = parse_lean([[ g B ]]) +print(t) +print("===>") +local t2, pr = simplify(t, "simple") +print(t2) +print(pr) +print(get_environment():type_check(pr)) +*) \ No newline at end of file diff --git a/tests/lean/simp20.lean.expected.out b/tests/lean/simp20.lean.expected.out new file mode 100644 index 0000000000..30526eb0ce --- /dev/null +++ b/tests/lean/simp20.lean.expected.out @@ -0,0 +1,13 @@ + Set: pp::colors + Set: pp::unicode + Imported 'cast' + Set: lean::pp::implicit + Assumed: g + Assumed: B + Assumed: B' + Assumed: H +g B +===> +g B' +@congr2 TypeM TypeM B B' g (@subst Type B B' (λ x : Type, @eq TypeM B x) (@refl TypeM B) H) +@eq TypeM (g B) (g B')