From 844572c382ade148ce3c0ad7ee7571c5b8967bce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 26 Jan 2014 00:32:05 -0800 Subject: [PATCH] feat(library/simplifier): support for dependent simplification in Pi/forall expressions Signed-off-by: Leonardo de Moura --- src/builtin/heq.lean | 20 +- src/builtin/obj/heq.olean | Bin 2795 -> 3371 bytes src/library/heq_decls.cpp | 3 + src/library/heq_decls.h | 9 + src/library/simplifier/simplifier.cpp | 547 +++++++++++++++++--------- tests/lean/simp28.lean | 14 + tests/lean/simp28.lean.expected.out | 5 + tests/lean/simp30.lean | 35 ++ tests/lean/simp30.lean.expected.out | 15 + 9 files changed, 461 insertions(+), 187 deletions(-) create mode 100644 tests/lean/simp30.lean create mode 100644 tests/lean/simp30.lean.expected.out diff --git a/src/builtin/heq.lean b/src/builtin/heq.lean index 6a15497cc..23fac1732 100644 --- a/src/builtin/heq.lean +++ b/src/builtin/heq.lean @@ -41,12 +41,16 @@ theorem hsfunext {A : TypeM} {B B' : A → TypeU} {f : ∀ x, B x} {f' : ∀ x, in htrans s1 s2) axiom hpiext {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM} : - A = A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) == (∀ x, B' x) + A = A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) = (∀ x, B' x) -theorem hallext {A A' : TypeM} {B : A → Bool} {B' : A' → Bool} : - A = A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) == (∀ x, B' x) --- We can't just invoke hpiext because the equality B x = B' x' is actually (@eq Bool (B x) (B' x')), --- and hpiext expects (@eq TypeM (B x) (B' x')). --- We move (@eq Bool (B x) (B' x')) to (@eq TypeM (B x) (B' x')) by using --- the following trick. We say it is a "universe" bump. -:= λ H1 H2, hpiext H1 (λ x x' Heq, subst (refl (B x)) (H2 x x' Heq)) \ No newline at end of file +axiom hallext {A A' : TypeM} {B : A → Bool} {B' : A' → Bool} : + A = A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) = (∀ x, B' x) + +theorem eq_hcongr {A A' : TypeM} (H : A = A') : (@eq A) == (@eq A') +:= substp (λ x : TypeM, (@eq A) == (@eq x)) (hrefl (@eq A)) H + +theorem neq_hcongr {A A' : TypeM} (H : A = A') : (@neq A) == (@neq A') +:= substp (λ x : TypeM, (@neq A) == (@neq x)) (hrefl (@neq A)) H + +theorem exists_hcongr {A A' : TypeM} (H : A = A') : (Exists A) == (Exists A') +:= substp (λ x : TypeM, (Exists A) == (Exists x)) (hrefl (Exists A)) H diff --git a/src/builtin/obj/heq.olean b/src/builtin/obj/heq.olean index 75a4733802e192ef6ca43014990c424030e949d9..b3dd9064688d1e88bb73b9537872c361356a0619 100644 GIT binary patch delta 836 zcmZ{i%TB^T6o#i$sfD;A(S=*o;F`pxaih_=@eK@W10-677A0N+ULL@tFW}w{?|^t& z8C~lWX!I4FZ>FVSLX-aUotZN;=RfV&^!;qNly&BXdZwb~?4m5UqFUB3nHi=f(m}c# z2S<#eqTUHhJz-TyufAQ~J@hM$=+2#KuZwi2N3Mmq3+SXH%ZwtIK%PiCXcMtC9)meV z7HqlV)j>5=K%WsSgEkOPV-RCojUn7C+A?VF1fi)|=vwrdRz|kS5MEpqtZ&b!w=Xd{ zRG3R_rv>Cwbmv&RMf!pxUqCnM6~#-_DgS?~NbH#^z&`SXWt9mhoeKRvmzA4hHxiATgV@&>eZ ztUQ|iM2X8E(73z=jmxVPufee{PgouKsQSVOX5#{q-%fu`{a;Jn1bwq8tw diff --git a/src/library/heq_decls.cpp b/src/library/heq_decls.cpp index 2425f5364..438e6d719 100644 --- a/src/library/heq_decls.cpp +++ b/src/library/heq_decls.cpp @@ -19,4 +19,7 @@ MK_CONSTANT(hfunext_fn, name("hfunext")); MK_CONSTANT(hsfunext_fn, name("hsfunext")); MK_CONSTANT(hpiext_fn, name("hpiext")); MK_CONSTANT(hallext_fn, name("hallext")); +MK_CONSTANT(eq_hcongr_fn, name("eq_hcongr")); +MK_CONSTANT(neq_hcongr_fn, name("neq_hcongr")); +MK_CONSTANT(exists_hcongr_fn, name("exists_hcongr")); } diff --git a/src/library/heq_decls.h b/src/library/heq_decls.h index e0b798cb4..bb5aab053 100644 --- a/src/library/heq_decls.h +++ b/src/library/heq_decls.h @@ -44,4 +44,13 @@ inline expr mk_hpiext_th(expr const & e1, expr const & e2, expr const & e3, expr expr mk_hallext_fn(); bool is_hallext_fn(expr const & e); inline expr mk_hallext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hallext_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_eq_hcongr_fn(); +bool is_eq_hcongr_fn(expr const & e); +inline expr mk_eq_hcongr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eq_hcongr_fn(), e1, e2, e3}); } +expr mk_neq_hcongr_fn(); +bool is_neq_hcongr_fn(expr const & e); +inline expr mk_neq_hcongr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_neq_hcongr_fn(), e1, e2, e3}); } +expr mk_exists_hcongr_fn(); +bool is_exists_hcongr_fn(expr const & e); +inline expr mk_exists_hcongr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_hcongr_fn(), e1, e2, e3}); } } diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp index 722a12b2a..967533504 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -107,16 +107,24 @@ static name g_unique = name::mk_internal_unique_name(); class simplifier_fn { struct result { - expr m_expr; // the result of a simplification step - optional m_proof; // a proof that the result is equal to the input (when m_proofs_enabled) - bool m_heq_proof; // true if the proof is for heterogeneous equality + expr m_expr; // the result of a simplification step + optional m_proof; // a proof that the result is equal to the input (when m_proofs_enabled) + bool m_heq_proof; // true if the proof has type lhs == rhs (i.e., it is a heterogeneous equality) + bool m_typem; // theorem lifted equality to (Type M) even if m_expr is from a lower universe. result() {} explicit result(expr const & out, bool heq_proof = false): - m_expr(out), m_heq_proof(heq_proof) {} - result(expr const & out, expr const & pr, bool heq_proof = false): - m_expr(out), m_proof(pr), m_heq_proof(heq_proof) {} - result(expr const & out, optional const & pr, bool heq_proof = false): - m_expr(out), m_proof(pr), m_heq_proof(heq_proof) {} + m_expr(out), m_heq_proof(heq_proof), m_typem(false) {} + result(expr const & out, expr const & pr, bool heq_proof = false, bool typem = false): + m_expr(out), m_proof(pr), m_heq_proof(heq_proof), m_typem(typem) { + lean_assert(!heq_proof || !typem); + } + result(expr const & out, optional const & pr, bool heq_proof = false, bool typem = false): + m_expr(out), m_proof(pr), m_heq_proof(heq_proof), m_typem(typem) { + lean_assert(!heq_proof || !typem); + } + bool is_heq_proof() const { return m_heq_proof; } + bool is_typem() const { return m_typem; } + result update_expr(expr const & new_e) const { return result(new_e, m_proof, m_heq_proof, m_typem); } }; typedef std::vector rule_sets; @@ -226,10 +234,22 @@ class simplifier_fn { 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) { - if (A != B) + if (A != 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); - else + } else { return H; + } + } + + expr translate_eq_typem_proof(expr const & A, expr const & a, expr const & b, expr const & H) { + return translate_eq_proof(A, a, b, H, mk_TypeM()); + } + + expr translate_eq_typem_proof(expr const & a, result const & b) { + if (b.is_typem()) + return get_proof(b); + else + return translate_eq_proof(infer_type(a), a, b.m_expr, get_proof(b), mk_TypeM()); } expr mk_congr1_th(expr const & f_type, expr const & f, expr const & new_f, expr const & a, expr const & Heq_f) { @@ -243,7 +263,7 @@ class simplifier_fn { 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); + Heq_a = translate_eq_proof(a_type, a, new_a, Heq_a, A); // CHECK return ::lean::mk_congr2_th(A, B, a, new_a, f, Heq_a); } @@ -253,36 +273,106 @@ class simplifier_fn { 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); + Heq_a = translate_eq_proof(a_type, a, new_a, Heq_a, A); // CHECK return ::lean::mk_congr_th(A, B, 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_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)) { - 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 + expr get_proof(result const & rhs) { + if (rhs.m_proof) { + return *rhs.m_proof; + } else { + // lhs and rhs are definitionally equal + return mk_refl_th(infer_type(rhs.m_expr), rhs.m_expr); + } + } + + /** + \brief Return the type of equality. + */ + expr get_eq_type(result const & rhs) { + if (rhs.is_typem()) { + return mk_TypeM(); + } else { + #if LEAN_DEBUG + if (rhs.m_proof) { + expr type = infer_type(*rhs.m_proof); + if (is_eq(type)) { + lean_assert_eq(arg(type, 1), infer_type(rhs.m_expr)); } } - Heq_a = translate_eq_proof(a_type, a, new_a, Heq_a, A); + #endif + return infer_type(rhs.m_expr); + } + } + + /** + \brief Some builtin constants (e.g., eq, neq and exists) have arguments of type (Type U). + The congruence axiom cannot be directly used in this constants. Since, they are in (Type U+1) and the congruence + axioms expect arguments from (Type U). We address this issue by creating custom congruence theorems + for these constants. The constant theorems can only be applied if the argument is actually in (Type M). + + \remark M is a universe smaller than U + + For example, the custom congruence theorem for equality is + + theorem eq_hcongr {A A' : TypeM} (H : A = A') : (@eq A) == (@eq A') + */ + optional mk_typem_congr_th(expr const & cgr_thm, expr const & a, result const & new_a) { + expr Heq_a = get_proof(new_a); + expr a_type = infer_type(a); + if (new_a.is_heq_proof()) + Heq_a = mk_to_eq_th(a_type, a, new_a.m_expr, Heq_a); + + if (!new_a.is_typem()) { + if (!is_convertible(a_type, mk_TypeM())) + return none_expr(); // failed + Heq_a = translate_eq_typem_proof(a_type, a, new_a.m_expr, Heq_a); + } + + return some_expr(cgr_thm(a, new_a.m_expr, Heq_a)); + } + + /** + \brief Create heterogeneous congruence proof. + */ + optional mk_hcongr_th(expr const & f_type, expr const & new_f_type, expr const & f, expr const & new_f, + expr const & Heq_f, expr const & a, result const & new_a) { + // TODO: make the following code more "customizable". + // We should be able to "install" new custom congruence theorem + if (is_eq_fn(f) && is_eq_fn(new_f)) { + return mk_typem_congr_th(mk_eq_hcongr_fn(), a, new_a); + } else if (is_exists_fn(f) && is_exists_fn(new_f)) { + return mk_typem_congr_th(mk_exists_hcongr_fn(), a, new_a); + } else if (is_neq_fn(f) && is_neq_fn(new_f)) { + return mk_typem_congr_th(mk_neq_hcongr_fn(), a, new_a); + } else { + 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.m_expr); + if (!is_convertible(new_a_type, new_A)) + return none_expr(); // failed + expr Heq_a = get_proof(new_a); + bool is_heq_proof = new_a.is_heq_proof(); + if (!is_definitionally_equal(A, a_type)|| !is_definitionally_equal(new_A, new_a_type)) { + if (is_heq_proof) { + 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.m_expr, Heq_a); + is_heq_proof = false; + } else { + return none_expr(); // we don't know how to handle this case + } + } + Heq_a = translate_eq_proof(get_eq_type(new_a), a, new_a.m_expr, Heq_a, A); + } + if (!is_heq_proof) + Heq_a = mk_to_heq_th(A, a, new_a.m_expr, 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.m_expr, Heq_f, Heq_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)); } /** @@ -291,7 +381,7 @@ class simplifier_fn { b_res.m_expr = c with proof H_bc This method returns a new result r s.t. r.m_expr == c and a proof of a = c */ - result mk_trans_result(expr const & a, result const & b_res, expr const & c, expr const & H_bc) { + result mk_trans_result(expr const & a, result const & b_res, expr const & c, expr H_bc) { if (m_proofs_enabled) { if (!b_res.m_proof) { // The proof of a = b is reflexivity @@ -300,15 +390,17 @@ class simplifier_fn { expr const & b = b_res.m_expr; expr new_proof; bool heq_proof = false; - if (b_res.m_heq_proof) { + if (b_res.is_heq_proof()) { expr b_type = infer_type(b); new_proof = ::lean::mk_htrans_th(infer_type(a), b_type, b_type, /* b and c must have the same type */ a, b, c, *b_res.m_proof, mk_to_heq_th(b_type, b, c, H_bc)); heq_proof = true; } else { - new_proof = ::lean::mk_trans_th(infer_type(a), a, b, c, *b_res.m_proof, H_bc); + if (b_res.is_typem()) + H_bc = translate_eq_typem_proof(infer_type(b), b, c, H_bc); + new_proof = ::lean::mk_trans_th(get_eq_type(b_res), a, b, c, *b_res.m_proof, H_bc); } - return result(c, new_proof, heq_proof); + return result(c, new_proof, heq_proof, b_res.is_typem()); } } else { return result(c); @@ -329,27 +421,39 @@ class simplifier_fn { return c_res; } else if (!c_res.m_proof) { // the proof of b == c is reflexivity - return result(c_res.m_expr, *b_res.m_proof, b_res.m_heq_proof); + return b_res.update_expr(c_res.m_expr); } else { - bool heq_proof = b_res.m_heq_proof || c_res.m_heq_proof; + bool heq_proof = b_res.is_heq_proof() || c_res.is_heq_proof(); expr new_proof; expr const & b = b_res.m_expr; expr const & c = c_res.m_expr; + bool typem = false; if (heq_proof) { expr a_type = infer_type(a); expr b_type = infer_type(b); expr c_type = infer_type(c); expr H_ab = *b_res.m_proof; - if (!b_res.m_heq_proof) + if (!b_res.is_heq_proof()) H_ab = mk_to_heq_th(a_type, a, b, H_ab); expr H_bc = *c_res.m_proof; - if (!c_res.m_heq_proof) + if (!c_res.is_heq_proof()) H_bc = mk_to_heq_th(b_type, b, c, H_bc); new_proof = ::lean::mk_htrans_th(a_type, b_type, c_type, a, b, c, H_ab, H_bc); + } else if (b_res.is_typem() && c_res.is_typem()) { + new_proof = ::lean::mk_trans_th(mk_TypeM(), a, b, c, *b_res.m_proof, *c_res.m_proof); + typem = true; + } else if (b_res.is_typem()) { + expr H_bc = translate_eq_typem_proof(infer_type(b), b, c, *c_res.m_proof); + new_proof = ::lean::mk_trans_th(mk_TypeM(), a, b, c, *b_res.m_proof, H_bc); + typem = true; + } else if (c_res.is_typem()) { + expr H_ab = translate_eq_typem_proof(infer_type(a), a, b, *b_res.m_proof); + new_proof = ::lean::mk_trans_th(mk_TypeM(), a, b, c, H_ab, *c_res.m_proof); + typem = true; } else { new_proof = ::lean::mk_trans_th(infer_type(a), a, b, c, *b_res.m_proof, *c_res.m_proof); } - return result(c, new_proof, heq_proof); + return result(c, new_proof, heq_proof, typem); } } else { // proof generation is disabled @@ -388,7 +492,7 @@ class simplifier_fn { if (res_a.m_proof) { expr Hec; expr Hac = *res_a.m_proof; - if (!res_a.m_heq_proof) { + if (!res_a.is_heq_proof()) { 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 @@ -423,7 +527,7 @@ class simplifier_fn { If it is not possible to transform it in a homogeneous equality proof, then return false. */ bool ensure_homogeneous(expr const & lhs, result & rhs) { - if (rhs.m_heq_proof) { + if (rhs.is_heq_proof()) { // try to convert back to homogeneous lean_assert(rhs.m_proof); expr lhs_type = infer_type(lhs); @@ -441,21 +545,15 @@ class simplifier_fn { } void ensure_heterogeneous(expr const & lhs, result & rhs) { - if (!rhs.m_heq_proof) { - rhs.m_proof = mk_to_heq_th(infer_type(lhs), lhs, rhs.m_expr, get_proof(rhs)); + if (!rhs.is_heq_proof()) { + if (rhs.is_typem()) + rhs.m_proof = mk_to_heq_th(mk_TypeM(), lhs, rhs.m_expr, get_proof(rhs)); + else + rhs.m_proof = mk_to_heq_th(infer_type(lhs), lhs, rhs.m_expr, get_proof(rhs)); rhs.m_heq_proof = true; } } - expr get_proof(result const & rhs) { - if (rhs.m_proof) { - return *rhs.m_proof; - } else { - // lhs and rhs are definitionally equal - return mk_refl_th(infer_type(rhs.m_expr), rhs.m_expr); - } - } - /** \brief Simplify \c e under the new assumption \c H. @@ -554,6 +652,7 @@ class simplifier_fn { buffer> proofs; // used only if m_proofs_enabled buffer f_types, new_f_types; // used only if m_proofs_enabled buffer heq_proofs; // used only if m_has_heq && m_proofs_enabled + buffer typem_flags; bool changed = false; expr f = arg(e, 0); expr f_type = infer_type(f); @@ -566,10 +665,12 @@ class simplifier_fn { if (m_proofs_enabled) { proofs.push_back(res_f.m_proof); f_types.push_back(f_type); - new_f_type = res_f.m_heq_proof ? infer_type(new_f) : f_type; + new_f_type = res_f.is_heq_proof() ? infer_type(new_f) : f_type; new_f_types.push_back(new_f_type); - if (m_has_heq) - heq_proofs.push_back(res_f.m_heq_proof); + if (m_has_heq) { + heq_proofs.push_back(res_f.is_heq_proof()); + typem_flags.push_back(res_f.is_typem()); + } } unsigned num = num_args(e); for (unsigned i = 1; i < num; i++) { @@ -586,8 +687,10 @@ class simplifier_fn { new_args.push_back(new_a); if (m_proofs_enabled) { proofs.push_back(res_a.m_proof); - if (m_has_heq) - heq_proofs.push_back(res_a.m_heq_proof); + if (m_has_heq) { + heq_proofs.push_back(res_a.is_heq_proof()); + typem_flags.push_back(res_a.is_typem()); + } bool changed_f_type = !is_eqp(f_type, new_f_type); if (f_arrow) { f_type = lower_free_vars(abst_body(f_type), 1, 1); @@ -625,8 +728,8 @@ 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]; - 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]); + auto new_pr = mk_hcongr_th(f_types[i-1], f_types[i-1], f, f, mk_hrefl_th(f_types[i-1], f), + arg(e, i), result(new_args[i], pr_i, heq_proofs[i], typem_flags[i])); if (!new_pr) return rewrite_app(e, result(e)); // failed to create congruence proof pr = *new_pr; @@ -644,13 +747,16 @@ 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); - 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); + auto new_pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, pr, + arg(e, i), result(new_args[i], 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) { - 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]); + lean_assert(!heq_proofs[i]); + auto new_pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, pr, + arg(e, i), result(new_args[i], pr_i, false, typem_flags[i])); if (!new_pr) return rewrite_app(e, result(e)); // failed to create congruence proof pr = *new_pr; @@ -658,8 +764,8 @@ class simplifier_fn { pr = mk_congr_th(f_types[i-1], f, new_f, arg(e, i), new_args[i], pr, pr_i); } } else if (heq_proof) { - 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); + auto new_pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, pr, + arg(e, i), result(arg(e, i))); if (!new_pr) return rewrite_app(e, result(e)); // failed to create congruence proof pr = *new_pr; @@ -722,7 +828,7 @@ class simplifier_fn { if (is_value(new_rhs)) { // We don't need to create a new proof term since rhs.m_expr and new_rhs are // definitionally equal. - return rewrite(lhs, result(new_rhs, rhs.m_proof, rhs.m_heq_proof)); + return rewrite(lhs, rhs.update_expr(new_rhs)); } } @@ -730,9 +836,8 @@ class simplifier_fn { if (m_beta && is_lambda(f)) { expr new_rhs = head_beta_reduce(rhs.m_expr); // rhs.m_expr and new_rhs are also definitionally equal - return rewrite(lhs, result(new_rhs, rhs.m_proof, rhs.m_heq_proof)); + return rewrite(lhs, rhs.update_expr(new_rhs)); } - return rewrite(lhs, rhs); } @@ -954,7 +1059,7 @@ class simplifier_fn { expr new_e = mk_lambda(e, abstract(new_bi, fresh_const)); if (!m_proofs_enabled || !res_bi.m_proof) return rewrite_lambda(e, result(new_e)); - if (res_bi.m_heq_proof) { + if (res_bi.is_heq_proof()) { lean_assert(m_has_heq); // Using // theorem hsfunext {A : TypeM} {B B' : A → TypeU} {f : ∀ x, B x} {f' : ∀ x, B' x} : @@ -976,125 +1081,209 @@ class simplifier_fn { } } + /** + \brief Simplify a lambda abstraction when the heq module is available. + In this case, we can simplify the domain and body of the lambda expression. + */ + result simplify_lambda_with_heq(expr const & e) { + expr const & d = abst_domain(e); + result res_d = simplify(d); + expr new_d = res_d.m_expr; + if (is_eqp(d, new_d)) + return simplify_lambda_body(e); + if (is_definitionally_equal(d, new_d)) + return simplify_lambda_body(update_lambda(e, new_d, abst_body(e))); + // d and new_d are only provably equal, so we need to use hfunext + expr x_old = mk_fresh_const(d); + expr x_new = mk_fresh_const(new_d); + expr x_old_eq_x_new = mk_heq(d, new_d, x_old, x_new); + expr H_x_old_eq_x_new = mk_fresh_const(x_old_eq_x_new); + expr bi = instantiate(abst_body(e), x_old); + result res_bi = simplify_remapping_constant(bi, x_old, x_new, H_x_old_eq_x_new); + expr new_bi = res_bi.m_expr; + if (occurs(x_old, new_bi)) { + // failed, simplifier didn't manage to replace x_old with x_new + return rewrite(e, result(e)); + } + expr new_e = update_lambda(e, new_d, abstract(new_bi, x_new)); + if (!m_proofs_enabled) + return rewrite(e, result(new_e)); + ensure_homogeneous(d, res_d); + ensure_heterogeneous(bi, res_bi); + // Using + // axiom hfunext {A A' : TypeM} {B : A → TypeU} {B' : A' → TypeU} {f : ∀ x, B x} {f' : ∀ x, B' x} : + // A = A' → (∀ x x', x == x' → f x == f' x') → f == f' + // Remark: the argument with type A = A' is actually @eq TypeM A A', + // so we need to translate the proof d_eq_new_d_proof : d = new_d to a TypeM equality proof + expr d_eq_new_d_proof = translate_eq_typem_proof(d, res_d); + expr new_proof = mk_hfunext_th(d, // A + new_d, // A' + Fun(x_old, d, infer_type(bi)), // B + Fun(x_new, new_d, infer_type(new_bi)), // B' + e, // f + new_e, // f' + d_eq_new_d_proof, // A = A' + // fun (x_old : d) (x_new : new_d) (H : x_old == x_new), bi == new_bi + mk_lambda(abst_name(e), d, + mk_lambda(name(abst_name(e), 1), lift_free_vars(new_d, 0, 1), + mk_lambda(name(g_H, m_next_idx++), abstract(x_old_eq_x_new, {x_old, x_new}), + abstract(*res_bi.m_proof, {x_old, x_new, H_x_old_eq_x_new}))))); + return rewrite(e, result(new_e, new_proof, true)); + } + result simplify_lambda(expr const & e) { lean_assert(is_lambda(e)); if (m_has_heq) { - expr const & d = abst_domain(e); - result res_d = simplify(d); - expr new_d = res_d.m_expr; - if (is_eqp(d, new_d)) - return simplify_lambda_body(e); - if (is_definitionally_equal(d, new_d)) - return simplify_lambda_body(update_lambda(e, new_d, abst_body(e))); - // d and new_d are only provably equal, so we need to use hfunext - expr x_old = mk_fresh_const(d); - expr x_new = mk_fresh_const(new_d); - expr x_old_eq_x_new = mk_heq(d, new_d, x_old, x_new); - expr H_x_old_eq_x_new = mk_fresh_const(x_old_eq_x_new); - expr bi = instantiate(abst_body(e), x_old); - result res_bi = simplify_remapping_constant(bi, x_old, x_new, H_x_old_eq_x_new); - expr new_bi = res_bi.m_expr; - if (occurs(x_old, new_bi)) { - // failed, simplifier didn't manage to replace x_old with x_new - return rewrite(e, result(e)); - } - expr new_e = update_lambda(e, new_d, abstract(new_bi, x_new)); - if (!m_proofs_enabled) - return rewrite(e, result(new_e)); - ensure_homogeneous(d, res_d); - ensure_heterogeneous(bi, res_bi); - expr d_eq_new_d_proof = *res_d.m_proof; - // Using - // axiom hfunext {A A' : TypeM} {B : A → TypeU} {B' : A' → TypeU} {f : ∀ x, B x} {f' : ∀ x, B' x} : - // A = A' → (∀ x x', x == x' → f x == f' x') → f == f' - // Remark: the argument with type A = A' is actually @eq TypeM A A', - // so we need to translate the proof d_eq_new_d_proof : d = new_d to a TypeM equality proof - d_eq_new_d_proof = translate_eq_proof(infer_type(d), d, new_d, d_eq_new_d_proof, mk_TypeM()); - expr new_proof = mk_hfunext_th(d, // A - new_d, // A' - Fun(x_old, d, infer_type(bi)), // B - Fun(x_new, new_d, infer_type(new_bi)), // B' - e, // f - new_e, // f' - d_eq_new_d_proof, // A = A' - // fun (x_old : d) (x_new : new_d) (H : x_old == x_new), bi == new_bi - mk_lambda(abst_name(e), d, - mk_lambda(name(abst_name(e), 1), lift_free_vars(new_d, 0, 1), - mk_lambda(name(g_H, m_next_idx++), abstract(x_old_eq_x_new, {x_old, x_new}), - abstract(*res_bi.m_proof, {x_old, x_new, H_x_old_eq_x_new}))))); - return rewrite(e, result(new_e, new_proof, true)); + return simplify_lambda_with_heq(e); } else { return simplify_lambda_body(e); } } - result simplify_pi(expr const & e) { - lean_assert(is_pi(e)); + /** + \brief Simplify A -> B + */ + result simplify_implication(expr const & e) { expr const & d = abst_domain(e); expr b = abst_body(e); - bool is_prop = is_proposition(e); - bool is_d_prop = is_proposition(d); - bool is_arr = is_arrow(e); - if (is_d_prop && is_arr) { - if (m_contextual) { - // Contextual simplification for A -> B - // Rewrite A to A' - // And rewrite B to B' using A' - result res_d = simplify(d); - ensure_homogeneous(d, res_d); - expr new_d = res_d.m_expr; - expr H = mk_fresh_const(new_d); - expr bi = lower_free_vars(b, 1, 1); - result res_bi = simplify_using(bi, H); - expr new_bi = res_bi.m_expr; - ensure_homogeneous(bi, res_bi); - if (is_eqp(new_d, d) && is_eqp(new_bi, bi)) - return rewrite(e, result(e)); - expr new_e = update_pi(e, new_d, lift_free_vars(new_bi, 0, 1)); - if (!m_proofs_enabled) - return rewrite(e, result(new_e)); - name C_name(g_C, m_next_idx++); - expr new_proof = mk_imp_congr_th(d, bi, new_d, new_bi, - get_proof(res_d), mk_lambda(C_name, new_d, abstract(get_proof(res_bi), H))); - return rewrite(e, result(new_e, new_proof)); - } else { - // Simplify A -> B (when m_contextual == false) - result res_d = simplify(d); - expr new_d = res_d.m_expr; - ensure_homogeneous(d, res_d); - expr bi = lower_free_vars(b, 1, 1); - result res_bi = simplify(bi); - expr new_bi = res_bi.m_expr; - ensure_homogeneous(bi, res_bi); - if (is_eqp(new_d, d) && is_eqp(new_bi, bi)) - return rewrite(e, result(e)); - expr new_e = update_pi(e, new_d, lift_free_vars(new_bi, 0, 1)); - if (!m_proofs_enabled) - return rewrite(e, result(new_e)); - expr new_proof = mk_imp_congr_th(d, bi, new_d, new_bi, - get_proof(res_d), mk_lambda(g_H, new_d, lift_free_vars(get_proof(res_bi), 0, 1))); - return rewrite(e, result(new_e, new_proof)); - } - } else if (m_has_heq) { - // TODO(Leo) - return result(e); - } else if (is_prop) { - // Simplify (forall x : A, P x) - expr fresh_const = mk_fresh_const(abst_domain(e)); - expr bi = instantiate(b, fresh_const); - result res_bi = simplify(bi); - expr new_bi = res_bi.m_expr; - lean_assert(!res_bi.m_heq_proof); - if (is_eqp(new_bi, bi)) + if (m_contextual) { + // Contextual simplification for A -> B + // Rewrite A to A' + // And rewrite B to B' using A' + result res_d = simplify(d); + ensure_homogeneous(d, res_d); + expr new_d = res_d.m_expr; + expr H = mk_fresh_const(new_d); + expr bi = lower_free_vars(b, 1, 1); + result res_bi = simplify_using(bi, H); + expr new_bi = res_bi.m_expr; + ensure_homogeneous(bi, res_bi); + if (is_eqp(new_d, d) && is_eqp(new_bi, bi)) return rewrite(e, result(e)); - expr new_e = mk_pi(abst_name(e), d, abstract(new_bi, fresh_const)); - if (!m_proofs_enabled || !res_bi.m_proof) + expr new_e = update_pi(e, new_d, lift_free_vars(new_bi, 0, 1)); + if (!m_proofs_enabled) return rewrite(e, result(new_e)); - expr new_proof = mk_allext_th(d, - mk_lambda(e, b), - mk_lambda(e, abst_body(new_e)), - mk_lambda(e, abstract(*res_bi.m_proof, fresh_const))); + name C_name(g_C, m_next_idx++); + expr new_proof = mk_imp_congr_th(d, bi, new_d, new_bi, + get_proof(res_d), mk_lambda(C_name, new_d, abstract(get_proof(res_bi), H))); return rewrite(e, result(new_e, new_proof)); + } else { + // Simplify A -> B (when m_contextual == false) + result res_d = simplify(d); + expr new_d = res_d.m_expr; + ensure_homogeneous(d, res_d); + expr bi = lower_free_vars(b, 1, 1); + result res_bi = simplify(bi); + expr new_bi = res_bi.m_expr; + ensure_homogeneous(bi, res_bi); + if (is_eqp(new_d, d) && is_eqp(new_bi, bi)) + return rewrite(e, result(e)); + expr new_e = update_pi(e, new_d, lift_free_vars(new_bi, 0, 1)); + if (!m_proofs_enabled) + return rewrite(e, result(new_e)); + expr new_proof = mk_imp_congr_th(d, bi, new_d, new_bi, + get_proof(res_d), mk_lambda(g_H, new_d, lift_free_vars(get_proof(res_bi), 0, 1))); + return rewrite(e, result(new_e, new_proof)); + } + } + + /** + \brief Simplify the body of (forall x : A, P x), when P x is a proposition. + */ + result simplify_forall_body(expr const & e) { + expr fresh_const = mk_fresh_const(abst_domain(e)); + expr const & d = abst_domain(e); + expr b = abst_body(e); + expr bi = instantiate(b, fresh_const); + result res_bi = simplify(bi); + expr new_bi = res_bi.m_expr; + if (is_eqp(new_bi, bi)) + return rewrite(e, result(e)); + expr new_e = mk_pi(abst_name(e), d, abstract(new_bi, fresh_const)); + if (!m_proofs_enabled || !res_bi.m_proof) + return rewrite(e, result(new_e)); + ensure_homogeneous(bi, res_bi); + expr new_proof = mk_allext_th(d, + mk_lambda(e, b), + mk_lambda(e, abst_body(new_e)), + mk_lambda(e, abstract(*res_bi.m_proof, fresh_const))); + return rewrite(e, result(new_e, new_proof)); + } + + /** + \brief Simplify (forall x : A, P x) when the heq module is available. + In this case, we can simplify the domain and body of the Pi/forall expression. + */ + result simplify_pi_with_heq(expr const & e) { + expr const & d = abst_domain(e); + result res_d = simplify(d); + expr new_d = res_d.m_expr; + bool is_prop = is_proposition(e); + if (is_eqp(d, new_d) && is_prop) + return simplify_forall_body(e); + if (is_definitionally_equal(d, new_d) && is_prop) + return simplify_forall_body(update_pi(e, new_d, abst_body(e))); + // d and new_d are only provably equal, so we need to use hpiext or hallext + expr x_old = mk_fresh_const(d); + expr x_new = mk_fresh_const(new_d); + expr x_old_eq_x_new = mk_heq(d, new_d, x_old, x_new); + expr H_x_old_eq_x_new = mk_fresh_const(x_old_eq_x_new); + expr bi = instantiate(abst_body(e), x_old); + result res_bi = simplify_remapping_constant(bi, x_old, x_new, H_x_old_eq_x_new); + expr new_bi = res_bi.m_expr; + if (occurs(x_old, new_bi)) { + // failed, simplifier didn't manage to replace x_old with x_new + return rewrite(e, result(e)); + } + expr new_e = update_pi(e, new_d, abstract(new_bi, x_new)); + if (!m_proofs_enabled || is_definitionally_equal(e, new_e)) + return rewrite(e, result(new_e)); + ensure_homogeneous(d, res_d); + ensure_homogeneous(bi, res_bi); + // Remark: the argument with type A = A' in hallext and hpiext is actually @eq TypeM A A', + // so we need to translate the proof d_eq_new_d_proof : d = new_d to a TypeM equality proof + expr d_eq_new_d_proof = translate_eq_typem_proof(d, res_d); + expr bi_eq_new_bi_proof; + if (is_prop) + bi_eq_new_bi_proof = get_proof(res_bi); + else + bi_eq_new_bi_proof = translate_eq_typem_proof(bi, res_bi); + // Heqb : (∀ x x', x == x' → B x = B' x') + expr Heqb = mk_lambda(abst_name(e), d, + mk_lambda(name(abst_name(e), 1), lift_free_vars(new_d, 0, 1), + mk_lambda(name(g_H, m_next_idx++), abstract(x_old_eq_x_new, {x_old, x_new}), + abstract(bi_eq_new_bi_proof, {x_old, x_new, H_x_old_eq_x_new})))); + if (is_prop) { + // Using + // theorem hallext {A A' : TypeM} {B : A → Bool} {B' : A' → Bool} : + // A = A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) = (∀ x, B' x) + expr new_proof = mk_hallext_th(d, new_d, + Fun(x_old, d, bi), // B + Fun(x_new, new_d, new_bi), // B' + d_eq_new_d_proof, // A = A' + Heqb); + return rewrite(e, result(new_e, new_proof)); + } else { + // Using + // axiom hpiext {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM} : + // A = A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) = (∀ x, B' x) + expr new_proof = mk_hpiext_th(d, new_d, + Fun(x_old, d, bi), // B + Fun(x_new, new_d, new_bi), // B' + d_eq_new_d_proof, // A = A' + Heqb); + return rewrite(e, result(new_e, new_proof, false, true)); + } + } + + result simplify_pi(expr const & e) { + lean_assert(is_pi(e)); + if (is_proposition(abst_domain(e)) && is_arrow(e)) { + return simplify_implication(e); + } else if (m_has_heq) { + return simplify_pi_with_heq(e); + } else if (is_proposition(e)) { + return simplify_forall_body(e); } else { // if the environment does not contain heq axioms, then we don't simplify Pi's that are not forall's return result(e); @@ -1103,7 +1292,7 @@ class simplifier_fn { result save(expr const & e, result const & r) { if (m_memoize) { - result new_r(m_max_sharing(r.m_expr), r.m_proof, r.m_heq_proof); + result new_r = r.update_expr(m_max_sharing(r.m_expr)); m_cache.insert(mk_pair(e, new_r)); return new_r; } else { diff --git a/tests/lean/simp28.lean b/tests/lean/simp28.lean index c4bdca6a7..1e4693e4f 100644 --- a/tests/lean/simp28.lean +++ b/tests/lean/simp28.lean @@ -31,3 +31,17 @@ print(t2) -- print(pr) get_environment():type_check(pr) *) + +print "" + +variable lheq {A B : TypeM} : A → B → Bool +infixl 50 === : lheq +(* +local t = parse_lean('λ val : Nat, (λ n : Nat, λ v : vec (n + 0), (f v) ; empty) val === (λ n : Nat, λ v : vec (n + 0), v) val') +print(t) +print("=====>") +local t2, pr = simplify(t, "simple") +print(t2) +-- print(pr) +get_environment():type_check(pr) +*) diff --git a/tests/lean/simp28.lean.expected.out b/tests/lean/simp28.lean.expected.out index 0f18e118c..242982b1d 100644 --- a/tests/lean/simp28.lean.expected.out +++ b/tests/lean/simp28.lean.expected.out @@ -9,3 +9,8 @@ λ (n : ℕ) (v : vec n), v Assumed: f λ n : ℕ, f + + Assumed: lheq +λ val : ℕ, (λ (n : ℕ) (v : vec (n + 0)), f v ; empty) val === (λ (n : ℕ) (v : vec (n + 0)), v) val +=====> +λ val : ℕ, f === (λ v : vec val, v) diff --git a/tests/lean/simp30.lean b/tests/lean/simp30.lean new file mode 100644 index 000000000..dd71d6d44 --- /dev/null +++ b/tests/lean/simp30.lean @@ -0,0 +1,35 @@ +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 Nat::add_assoc Nat::add_zeror eq_id : simple +add_rewrite concat_assoc concat_empty Nat::add_assoc Nat::add_zeror : simple + +(* +local t = parse_lean('∀ (n : Nat) (v : vec (n + 0)) (w : vec n), v = w ; empty') +print(t) +local t2, pr = simplify(t, "simple") +print("====>") +print(t2) +get_environment():type_check(pr) +*) + +print "" + +(* +local t = parse_lean('λ n : Nat, ∃ (v : vec (n + 0)) (w : vec n), v ≠ w ; empty') +print(t) +local t2, pr = simplify(t, "simple") +print("====>") +print(t2) +get_environment():type_check(pr) +*) diff --git a/tests/lean/simp30.lean.expected.out b/tests/lean/simp30.lean.expected.out new file mode 100644 index 000000000..f2433ceb2 --- /dev/null +++ b/tests/lean/simp30.lean.expected.out @@ -0,0 +1,15 @@ + Set: pp::colors + Set: pp::unicode + Imported 'cast' + Assumed: vec + Assumed: concat + Assumed: concat_assoc + Assumed: empty + Assumed: concat_empty +∀ (n : ℕ) (v : vec (n + 0)) (w : vec n), v = w ; empty +====> +∀ (n : ℕ) (v w : vec n), v = w + +λ n : ℕ, ∃ (v : vec (n + 0)) (w : vec n), v ≠ w ; empty +====> +λ n : ℕ, ∃ v x : vec n, v ≠ x