diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index 12007a57f4..fac05f569a 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -372,6 +372,8 @@ struct app_builder::imp { } else if (n == get_iff_name()) { return mk_iff(lhs, rhs); } else { + // TODO(Leo): for some relations (e.g., heq), the lhs and rhs are not necessarily + // the last two arguments. expr args[2] = {lhs, rhs}; return mk_app(n, 2, args); } diff --git a/src/library/app_builder.h b/src/library/app_builder.h index 690314a56a..ed52da54a1 100644 --- a/src/library/app_builder.h +++ b/src/library/app_builder.h @@ -40,7 +40,6 @@ public: app_builder(environment const & env, reducible_behavior b = UnfoldReducible); app_builder(tmp_type_context & ctx); ~app_builder(); - /** \brief Create an application (d.{_ ... _} _ ... _ args[0] ... args[nargs-1]). The missing arguments and universes levels are inferred using type inference. diff --git a/src/library/congr_lemma_manager.cpp b/src/library/congr_lemma_manager.cpp index 1dc2291ca1..61d7a4002b 100644 --- a/src/library/congr_lemma_manager.cpp +++ b/src/library/congr_lemma_manager.cpp @@ -10,9 +10,15 @@ Author: Leonardo de Moura #include "library/locals.h" #include "library/constants.h" #include "library/replace_visitor.h" +#include "library/relation_manager.h" #include "library/congr_lemma_manager.h" namespace lean { +bool congr_lemma::all_eq_kind() const { + return std::all_of(m_arg_kinds.begin(), m_arg_kinds.end(), + [](congr_arg_kind k) { return k == congr_arg_kind::Eq; }); +} + struct congr_lemma_manager::imp { app_builder & m_builder; fun_info_manager & m_fmanager; @@ -37,9 +43,12 @@ struct congr_lemma_manager::imp { std::unordered_map m_simp_cache; std::unordered_map m_cache; + std::unordered_map m_rel_cache[2]; + relation_info_getter m_relation_info_getter; expr infer(expr const & e) { return m_ctx.infer(e); } expr whnf(expr const & e) { return m_ctx.whnf(e); } + expr relaxed_whnf(expr const & e) { return m_ctx.relaxed_whnf(e); } /** \brief (Try to) cast expression \c e to the given type using the equations \c eqs. \c deps contains the indices of the relevant equalities. @@ -289,7 +298,8 @@ struct congr_lemma_manager::imp { public: imp(app_builder & b, fun_info_manager & fm): - m_builder(b), m_fmanager(fm), m_ctx(fm.ctx()) {} + m_builder(b), m_fmanager(fm), m_ctx(fm.ctx()), + m_relation_info_getter(mk_relation_info_getter(fm.ctx().env())) {} optional mk_congr_simp(expr const & fn) { fun_info finfo = m_fmanager.get(fn); @@ -393,6 +403,86 @@ public: m_cache.insert(mk_pair(key(fn, nargs), *new_r)); return new_r; } + + optional mk_rel_congr(expr const & R, bool is_iff) { + try { + if (!is_constant(R)) + return optional(); + name const & R_name = const_name(R); + auto info = m_relation_info_getter(R_name); + if (!info) + return optional(); + unsigned arity = info->get_arity(); + key k(R, arity); + auto r = m_rel_cache[is_iff].find(k); + if (r != m_rel_cache[is_iff].end()) + return optional(r->second); + buffer hyps; + buffer kinds; + expr a1, b1, a2, b2; + expr H1, H2; + expr R_type = infer(R); + for (unsigned i = 0; i < arity; i++) { + R_type = relaxed_whnf(R_type); + if (!is_pi(R_type)) + return optional(); + expr h = m_ctx.mk_tmp_local(binding_name(R_type), binding_domain(R_type)); + if (i == info->get_lhs_pos()) { + a1 = h; + a2 = m_ctx.mk_tmp_local(binding_name(R_type), binding_domain(R_type)); + H1 = m_ctx.mk_tmp_local("H1", m_builder.mk_rel(R_name, a1, a2)); + hyps.push_back(a1); + hyps.push_back(a2); + hyps.push_back(H1); + kinds.push_back(congr_arg_kind::Eq); + } else if (i == info->get_rhs_pos()) { + b1 = h; + b2 = m_ctx.mk_tmp_local(binding_name(R_type), binding_domain(R_type)); + H2 = m_ctx.mk_tmp_local("H2", m_builder.mk_rel(R_name, b1, b2)); + hyps.push_back(b1); + hyps.push_back(b2); + hyps.push_back(H2); + kinds.push_back(congr_arg_kind::Eq); + } else { + hyps.push_back(h); + kinds.push_back(congr_arg_kind::Fixed); + } + R_type = instantiate(binding_body(R_type), h); + } + expr lhs = m_builder.mk_rel(R_name, a1, b1); + expr rhs = m_builder.mk_rel(R_name, a2, b2); + // (H1 : R a1 a2) -> (H2 : R b1 b2) -> (R a1 b1 <-> R a2 b2) + expr type = is_iff ? m_builder.mk_iff(lhs, rhs) : m_builder.mk_eq(lhs, rhs); + type = Pi(hyps, type); + /* Proof: + iff.intro + (λ H : R a1 b1, trans (symm H1) (trans H H2)) + (λ H : R a2 b2, trans H1 (trans H (symm H2))) + */ + expr H; + H = m_ctx.mk_tmp_local(lhs); + expr p1 = Fun(H, m_builder.mk_trans(R_name, m_builder.mk_symm(R_name, H1), m_builder.mk_trans(R_name, H, H2))); + H = m_ctx.mk_tmp_local(rhs); + expr p2 = Fun(H, m_builder.mk_trans(R_name, H1, m_builder.mk_trans(R_name, H, m_builder.mk_symm(R_name, H2)))); + expr pr = m_builder.mk_app(get_iff_intro_name(), p1, p2); + if (!is_iff) + pr = m_builder.mk_app(get_propext_name(), pr); + pr = Fun(hyps, pr); + result res(type, pr, to_list(kinds)); + m_rel_cache[is_iff].insert(mk_pair(k, res)); + return optional(res); + } catch (app_builder_exception &) { + return optional(); + } + } + + optional mk_rel_iff_congr(expr const & R) { + return mk_rel_congr(R, true); + } + + optional mk_rel_eq_congr(expr const & R) { + return mk_rel_congr(R, false); + } }; congr_lemma_manager::congr_lemma_manager(app_builder & b, fun_info_manager & fm): @@ -414,4 +504,12 @@ auto congr_lemma_manager::mk_congr(expr const & fn) -> optional { auto congr_lemma_manager::mk_congr(expr const & fn, unsigned nargs) -> optional { return m_ptr->mk_congr(fn, nargs); } + +auto congr_lemma_manager::mk_rel_iff_congr(expr const & R) -> optional { + return m_ptr->mk_rel_iff_congr(R); +} + +auto congr_lemma_manager::mk_rel_eq_congr(expr const & R) -> optional { + return m_ptr->mk_rel_eq_congr(R); +} } diff --git a/src/library/congr_lemma_manager.h b/src/library/congr_lemma_manager.h index 30be8ed2a6..37461ad67e 100644 --- a/src/library/congr_lemma_manager.h +++ b/src/library/congr_lemma_manager.h @@ -22,6 +22,7 @@ public: expr const & get_type() const { return m_type; } expr const & get_proof() const { return m_proof; } list const & get_arg_kinds() const { return m_arg_kinds; } + bool all_eq_kind() const; }; class congr_lemma_manager { @@ -37,5 +38,16 @@ public: optional mk_congr(expr const & fn); optional mk_congr(expr const & fn, unsigned nargs); + + /** \brief If R is an equivalence relation, construct the congruence lemma + + R a1 a2 -> R b1 b2 -> (R a1 b1) <-> (R a2 b2) */ + optional mk_rel_iff_congr(expr const & R); + + /** \brief Similar to previous one. + It returns none if propext is not available. + + R a1 a2 -> R b1 b2 -> (R a1 b1) = (R a2 b2) */ + optional mk_rel_eq_congr(expr const & R); }; } diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 7051c8401e..26400d5afa 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -58,6 +58,7 @@ name const * g_iff_symm = nullptr; name const * g_iff_trans = nullptr; name const * g_iff_mp = nullptr; name const * g_iff_mpr = nullptr; +name const * g_iff_intro = nullptr; name const * g_iff_elim_left = nullptr; name const * g_iff_elim_right = nullptr; name const * g_iff_false_intro = nullptr; @@ -231,6 +232,7 @@ void initialize_constants() { g_iff_trans = new name{"iff", "trans"}; g_iff_mp = new name{"iff", "mp"}; g_iff_mpr = new name{"iff", "mpr"}; + g_iff_intro = new name{"iff", "intro"}; g_iff_elim_left = new name{"iff", "elim_left"}; g_iff_elim_right = new name{"iff", "elim_right"}; g_iff_false_intro = new name{"iff_false_intro"}; @@ -405,6 +407,7 @@ void finalize_constants() { delete g_iff_trans; delete g_iff_mp; delete g_iff_mpr; + delete g_iff_intro; delete g_iff_elim_left; delete g_iff_elim_right; delete g_iff_false_intro; @@ -578,6 +581,7 @@ name const & get_iff_symm_name() { return *g_iff_symm; } name const & get_iff_trans_name() { return *g_iff_trans; } name const & get_iff_mp_name() { return *g_iff_mp; } name const & get_iff_mpr_name() { return *g_iff_mpr; } +name const & get_iff_intro_name() { return *g_iff_intro; } name const & get_iff_elim_left_name() { return *g_iff_elim_left; } name const & get_iff_elim_right_name() { return *g_iff_elim_right; } name const & get_iff_false_intro_name() { return *g_iff_false_intro; } diff --git a/src/library/constants.h b/src/library/constants.h index b5e88e9e25..b86ba17321 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -60,6 +60,7 @@ name const & get_iff_symm_name(); name const & get_iff_trans_name(); name const & get_iff_mp_name(); name const & get_iff_mpr_name(); +name const & get_iff_intro_name(); name const & get_iff_elim_left_name(); name const & get_iff_elim_right_name(); name const & get_iff_false_intro_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index f4208ff294..2e82c8e7fb 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -53,6 +53,7 @@ iff.symm iff.trans iff.mp iff.mpr +iff.intro iff.elim_left iff.elim_right iff_false_intro