From d0fe59ef8acdcb3e9bf30a487c7699119de4c141 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 3 Jan 2016 15:10:07 -0800 Subject: [PATCH] feat(library/congr_lemma_manager): add new kind of congr_arg --- src/library/blast/congruence_closure.cpp | 8 ++++ src/library/blast/simplifier/simplifier.cpp | 47 ++++++++++++++------- src/library/congr_lemma_manager.cpp | 6 +++ src/library/congr_lemma_manager.h | 10 ++++- 4 files changed, 55 insertions(+), 16 deletions(-) diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp index 2a8814e17..4da18f492 100644 --- a/src/library/blast/congruence_closure.cpp +++ b/src/library/blast/congruence_closure.cpp @@ -192,6 +192,7 @@ static optional to_ext_congr_lemma(name const & R, expr const & Rcs.resize(lhs_args.size(), optional()); r_hyps.resize(lhs_args.size(), none_expr()); // Set Fixed args + // TODO(Leo): handle FixedNoParam case? for (unsigned i = 0; i < lhs_args.size(); i++) { if (lhs_args[i] == rhs_args[i]) kinds[i] = congr_arg_kind::Fixed; @@ -241,6 +242,9 @@ static optional to_ext_congr_lemma(name const & R, expr const & return optional(); } switch (kinds[i]) { + case congr_arg_kind::FixedNoParam: + // TODO(Leo): revise this code + break; case congr_arg_kind::Fixed: break; case congr_arg_kind::Eq: { @@ -431,6 +435,7 @@ int congruence_closure::congr_key_cmp::operator()(congr_key const & k1, congr_ke if (r != 0) return r; break; case congr_arg_kind::Fixed: + case congr_arg_kind::FixedNoParam: r = expr_quick_cmp()(args1[i], args2[i]); if (r != 0) return r; break; @@ -491,6 +496,7 @@ auto congruence_closure::mk_congr_key(ext_congr_lemma const & lemma, expr const h = hash(h, get_root(*head(*it1), args[i]).hash()); break; case congr_arg_kind::Fixed: + case congr_arg_kind::FixedNoParam: h = hash(h, args[i].hash()); break; case congr_arg_kind::Cast: @@ -967,6 +973,8 @@ expr congruence_closure::mk_congr_proof_core(name const & R, expr const & lhs, e case congr_arg_kind::Fixed: lemma_args.push_back(lhs_args[i]); break; + case congr_arg_kind::FixedNoParam: + break; case congr_arg_kind::Cast: lemma_args.push_back(lhs_args[i]); lemma_args.push_back(rhs_args[i]); diff --git a/src/library/blast/simplifier/simplifier.cpp b/src/library/blast/simplifier/simplifier.cpp index 2c2c03786..93977f65d 100644 --- a/src/library/blast/simplifier/simplifier.cpp +++ b/src/library/blast/simplifier/simplifier.cpp @@ -277,22 +277,26 @@ optional simplifier::cache_lookup(expr const & e) { unsigned i = 0; for_each(congr_lemma->get_arg_kinds(), [&](congr_arg_kind const & ckind) { - if (ckind != congr_arg_kind::Cast) { - lean_assert(new_args[i] == old_args[i]); - } - proof = mk_app(proof, new_args[i]); - type = instantiate(binding_body(type), new_args[i]); + lean_assert(ckind == congr_arg_kind::Cast || new_args[i] == old_args[i]); expr rfl; switch (ckind) { case congr_arg_kind::Fixed: + proof = mk_app(proof, new_args[i]); + type = instantiate(binding_body(type), new_args[i]); + break; + case congr_arg_kind::FixedNoParam: break; case congr_arg_kind::Eq: + proof = mk_app(proof, new_args[i]); + type = instantiate(binding_body(type), new_args[i]); rfl = get_app_builder().mk_eq_refl(old_args[i]); proof = mk_app(proof, old_args[i], rfl); type = instantiate(binding_body(type), old_args[i]); type = instantiate(binding_body(type), rfl); break; case congr_arg_kind::Cast: + proof = mk_app(proof, new_args[i]); + type = instantiate(binding_body(type), new_args[i]); proof = mk_app(proof, old_args[i]); type = instantiate(binding_body(type), old_args[i]); break; @@ -807,17 +811,30 @@ optional simplifier::synth_congr(expr const & e, F && simp) { bool has_cast = false; buffer locals; for_each(congr_lemma->get_arg_kinds(), [&](congr_arg_kind const & ckind) { - proof = mk_app(proof, args[i]); - type = instantiate(binding_body(type), args[i]); - if (ckind == congr_arg_kind::Eq) { - result r_arg = simp(args[i]); - if (r_arg.has_proof()) has_proof = true; - r_arg = finalize(r_arg); - proof = mk_app(proof, r_arg.get_new(), r_arg.get_proof()); - type = instantiate(binding_body(type), r_arg.get_new()); - type = instantiate(binding_body(type), r_arg.get_proof()); - } else if (ckind == congr_arg_kind::Cast) { + switch (ckind) { + case congr_arg_kind::Fixed: + proof = mk_app(proof, args[i]); + type = instantiate(binding_body(type), args[i]); + break; + case congr_arg_kind::FixedNoParam: + break; + case congr_arg_kind::Eq: + proof = mk_app(proof, args[i]); + type = instantiate(binding_body(type), args[i]); + { + result r_arg = simp(args[i]); + if (r_arg.has_proof()) has_proof = true; + r_arg = finalize(r_arg); + proof = mk_app(proof, r_arg.get_new(), r_arg.get_proof()); + type = instantiate(binding_body(type), r_arg.get_new()); + type = instantiate(binding_body(type), r_arg.get_proof()); + } + break; + case congr_arg_kind::Cast: + proof = mk_app(proof, args[i]); + type = instantiate(binding_body(type), args[i]); has_cast = true; + break; } i++; }); diff --git a/src/library/congr_lemma_manager.cpp b/src/library/congr_lemma_manager.cpp index 00fc76675..1ee7b2c4a 100644 --- a/src/library/congr_lemma_manager.cpp +++ b/src/library/congr_lemma_manager.cpp @@ -199,6 +199,9 @@ struct congr_lemma_manager::imp { rhss.push_back(lhs); eqs.push_back(none_expr()); break; + case congr_arg_kind::FixedNoParam: + lean_unreachable(); // TODO(Leo): not implemented yet + break; case congr_arg_kind::Cast: { expr rhs_type = mlocal_type(lhs); rhs_type = instantiate_rev(abstract_locals(rhs_type, lhss.size()-1, lhss.data()), rhss.size(), rhss.data()); @@ -274,6 +277,9 @@ struct congr_lemma_manager::imp { rhss.push_back(rhs); eqs.push_back(none_expr()); break; + case congr_arg_kind::FixedNoParam: + lean_unreachable(); // TODO(Leo): not implemented yet + break; case congr_arg_kind::Cast: { rhs = m_ctx.mk_tmp_local(binding_name(fn_type2), binding_domain(fn_type2)); rhss.push_back(rhs); diff --git a/src/library/congr_lemma_manager.h b/src/library/congr_lemma_manager.h index 6ea1581b7..4d84602fb 100644 --- a/src/library/congr_lemma_manager.h +++ b/src/library/congr_lemma_manager.h @@ -10,7 +10,15 @@ Author: Leonardo de Moura #include "library/fun_info_manager.h" namespace lean { -enum class congr_arg_kind { Fixed, Eq, Cast }; +enum class congr_arg_kind { + Fixed, /* It is a parameter for the congruence lemma, the parit occurs in the left and right hand sides. */ + FixedNoParam, /* It is not a parameter for the congruence lemma, the lemma was specialized for this parameter. + This only happens if the parameter is a subsingleton/proposition, and other parameters depend on it. */ + Eq, /* The lemma contains three parameters for this kind of argument a_i, b_i and (eq_i : a_i = b_i). + a_i and b_i represent the left and right hand sides, and eq_i is a proof for their equality. */ + Cast /* congr-simp lemma contains only one parameter for this kind of argument, and congr-lemmas contains two. + They correspond to arguments that are subsingletons/propositions. */ +}; class congr_lemma { expr m_type;