From 0f631889b798e0f381349eea3a783dec2ee7dad4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 1 Nov 2015 16:25:14 -0800 Subject: [PATCH] feat(library/app_builder): add helper methods for creating binary relations, and refl/symm/trans proofs --- src/library/app_builder.cpp | 176 ++++++++++++++++++++++++++++++- src/library/app_builder.h | 20 ++++ src/library/constants.cpp | 8 ++ src/library/constants.h | 2 + src/library/constants.txt | 2 + src/library/relation_manager.cpp | 21 ++++ src/library/relation_manager.h | 8 ++ src/library/util.cpp | 7 ++ src/library/util.h | 1 + 9 files changed, 244 insertions(+), 1 deletion(-) diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index 869b8c94e..07266eba4 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -8,9 +8,11 @@ Author: Leonardo de Moura #include "util/name_map.h" #include "kernel/instantiate.h" #include "library/match.h" +#include "library/constants.h" #include "library/app_builder.h" #include "library/kernel_bindings.h" #include "library/tmp_type_context.h" +#include "library/relation_manager.h" namespace lean { struct app_builder::imp { @@ -94,7 +96,10 @@ struct app_builder::imp { typedef std::unordered_map map; - map m_map; + map m_map; + refl_info_getter m_refl_getter; + trans_info_getter m_trans_getter; + symm_info_getter m_symm_getter; imp(environment const & env, io_state const & ios, reducible_behavior b): m_ctx(new tmp_type_context(env, ios, b)) { @@ -203,6 +208,127 @@ struct app_builder::imp { optional mk_app(name const & /* c */, unsigned /* mask_sz */, bool const * /* mask */, expr const * /* args */) { return none_expr(); } + + optional get_level(expr const & A) { + expr Type = m_ctx->whnf(m_ctx->infer(A)); + if (!is_sort(Type)) + return none_level(); + return some_level(sort_level(Type)); + } + + optional mk_eq(expr const & a, expr const & b) { + expr A = m_ctx->infer(a); + auto lvl = get_level(A); + if (!lvl) + return none_expr(); + return some_expr(::lean::mk_app(mk_constant(get_eq_name(), {*lvl}), A, a, b)); + } + + optional mk_iff(expr const & a, expr const & b) { + return some_expr(::lean::mk_app(mk_constant(get_iff_name()), a, b)); + } + + optional mk_eq_refl(expr const & a) { + expr A = m_ctx->infer(a); + auto lvl = get_level(A); + if (!lvl) + return none_expr(); + return some_expr(::lean::mk_app(mk_constant(get_eq_refl_name(), {*lvl}), A, a)); + } + + optional mk_iff_refl(expr const & a) { + return some_expr(::lean::mk_app(mk_constant(get_iff_refl_name()), a)); + } + + optional mk_eq_symm(expr const & H) { + expr p = m_ctx->whnf(m_ctx->infer(H)); + expr lhs, rhs; + if (!is_eq(p, lhs, rhs)) + return none_expr(); + expr A = m_ctx->infer(lhs); + auto lvl = get_level(A); + if (!lvl) + return none_expr(); + return some_expr(::lean::mk_app(mk_constant(get_eq_symm_name(), {*lvl}), A, lhs, rhs, H)); + } + + optional mk_iff_symm(expr const & H) { + expr p = m_ctx->whnf(m_ctx->infer(H)); + expr lhs, rhs; + if (!is_iff(p, lhs, rhs)) + return none_expr(); + return some_expr(::lean::mk_app(mk_constant(get_iff_symm_name()), lhs, rhs, H)); + } + + optional mk_eq_trans(expr const & H1, expr const & H2) { + expr p1 = m_ctx->whnf(m_ctx->infer(H1)); + expr p2 = m_ctx->whnf(m_ctx->infer(H2)); + expr lhs1, rhs1, lhs2, rhs2; + if (!is_eq(p1, lhs1, rhs1) || !is_eq(p2, lhs2, rhs2)) + return none_expr(); + expr A = m_ctx->infer(lhs1); + auto lvl = get_level(A); + if (!lvl) + return none_expr(); + return some_expr(::lean::mk_app({mk_constant(get_eq_trans_name(), {*lvl}), A, lhs1, rhs1, rhs2, H1, H2})); + } + + optional mk_iff_trans(expr const & H1, expr const & H2) { + expr p1 = m_ctx->whnf(m_ctx->infer(H1)); + expr p2 = m_ctx->whnf(m_ctx->infer(H2)); + expr lhs1, rhs1, lhs2, rhs2; + if (!is_iff(p1, lhs1, rhs1) || !is_iff(p2, lhs2, rhs2)) + return none_expr(); + return some_expr(::lean::mk_app({mk_constant(get_iff_trans_name()), lhs1, rhs1, rhs2, H1, H2})); + } + + optional mk_rel(name const & n, expr const & lhs, expr const & rhs) { + if (n == get_eq_name()) { + return mk_eq(lhs, rhs); + } else if (n == get_iff_name()) { + return mk_iff(lhs, rhs); + } else { + expr args[2] = {lhs, rhs}; + return mk_app(n, 2, args); + } + } + + optional mk_refl(name const & relname, expr const & a) { + if (relname == get_eq_name()) { + return mk_eq_refl(a); + } else if (relname == get_iff_name()) { + return mk_iff_refl(a); + } else if (auto info = m_refl_getter(relname)) { + return mk_app(info->m_name, 1, &a); + } else { + return none_expr(); + } + } + + optional mk_symm(name const & relname, expr const & H) { + if (relname == get_eq_name()) { + return mk_eq_symm(H); + } else if (relname == get_iff_name()) { + return mk_iff_symm(H); + } else if (auto info = m_symm_getter(relname)) { + return mk_app(info->m_name, 1, &H); + } else { + return none_expr(); + } + } + + optional mk_trans(name const & relname, expr const & H1, expr const & H2) { + if (relname == get_eq_name()) { + return mk_eq_trans(H1, H2); + } else if (relname == get_iff_name()) { + return mk_iff_trans(H1, H2); + } else if (auto info = m_trans_getter(relname, relname)) { + expr args[2] = {H1, H2}; + return mk_app(info->m_name, 2, args); + } else { + return none_expr(); + } + } }; app_builder::app_builder(environment const & env, io_state const & ios, reducible_behavior b): @@ -227,6 +353,54 @@ optional app_builder::mk_app(name const & c, unsigned mask_sz, bool const return m_ptr->mk_app(c, mask_sz, mask, args); } +optional app_builder::mk_rel(name const & n, expr const & lhs, expr const & rhs) { + return m_ptr->mk_rel(n, lhs, rhs); +} + +optional app_builder::mk_eq(expr const & lhs, expr const & rhs) { + return m_ptr->mk_eq(lhs, rhs); +} + +optional app_builder::mk_iff(expr const & lhs, expr const & rhs) { + return m_ptr->mk_iff(lhs, rhs); +} + +optional app_builder::mk_refl(name const & relname, expr const & a) { + return m_ptr->mk_refl(relname, a); +} + +optional app_builder::mk_eq_refl(expr const & a) { + return m_ptr->mk_eq_refl(a); +} + +optional app_builder::mk_iff_refl(expr const & a) { + return m_ptr->mk_iff_refl(a); +} + +optional app_builder::mk_symm(name const & relname, expr const & H) { + return m_ptr->mk_symm(relname, H); +} + +optional app_builder::mk_eq_symm(expr const & H) { + return m_ptr->mk_eq_symm(H); +} + +optional app_builder::mk_iff_symm(expr const & H) { + return m_ptr->mk_iff_symm(H); +} + +optional app_builder::mk_trans(name const & relname, expr const & H1, expr const & H2) { + return m_ptr->mk_trans(relname, H1, H2); +} + +optional app_builder::mk_eq_trans(expr const & H1, expr const & H2) { + return m_ptr->mk_eq_trans(H1, H2); +} + +optional app_builder::mk_iff_trans(expr const & H1, expr const & H2) { + return m_ptr->mk_iff_trans(H1, H2); +} + void app_builder::set_context(list const & ctx) { m_ptr->m_ctx->set_context(ctx); } diff --git a/src/library/app_builder.h b/src/library/app_builder.h index 995bc89a3..c721898da 100644 --- a/src/library/app_builder.h +++ b/src/library/app_builder.h @@ -63,6 +63,26 @@ public: optional mk_app(name const & c, unsigned mask_sz, bool const * mask, expr const * args); + /** \brief Similar to mk_app(n, lhs, rhs), but handles eq and iff more efficiently. */ + optional mk_rel(name const & n, expr const & lhs, expr const & rhs); + optional mk_eq(expr const & lhs, expr const & rhs); + optional mk_iff(expr const & lhs, expr const & rhs); + + /** \brief Similar a reflexivity proof for the given relation */ + optional mk_refl(name const & relname, expr const & a); + optional mk_eq_refl(expr const & a); + optional mk_iff_refl(expr const & a); + + /** \brief Similar a symmetry proof for the given relation */ + optional mk_symm(name const & relname, expr const & H); + optional mk_eq_symm(expr const & H); + optional mk_iff_symm(expr const & H); + + /** \brief Similar a transitivity proof for the given relation */ + optional mk_trans(name const & relname, expr const & H1, expr const & H2); + optional mk_eq_trans(expr const & H1, expr const & H2); + optional mk_iff_trans(expr const & H1, expr const & H2); + /** \brief Set the local context. This method is relevant when we want to expose local class instances to the app_builder. diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 572efa273..792d6a5eb 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -44,6 +44,8 @@ name const * g_heq_refl = nullptr; name const * g_heq_to_eq = nullptr; name const * g_iff = nullptr; name const * g_iff_refl = nullptr; +name const * g_iff_symm = nullptr; +name const * g_iff_trans = nullptr; name const * g_iff_false_intro = nullptr; name const * g_iff_true_intro = nullptr; name const * g_implies = nullptr; @@ -198,6 +200,8 @@ void initialize_constants() { g_heq_to_eq = new name{"heq", "to_eq"}; g_iff = new name{"iff"}; g_iff_refl = new name{"iff", "refl"}; + g_iff_symm = new name{"iff", "symm"}; + g_iff_trans = new name{"iff", "trans"}; g_iff_false_intro = new name{"iff_false_intro"}; g_iff_true_intro = new name{"iff_true_intro"}; g_implies = new name{"implies"}; @@ -353,6 +357,8 @@ void finalize_constants() { delete g_heq_to_eq; delete g_iff; delete g_iff_refl; + delete g_iff_symm; + delete g_iff_trans; delete g_iff_false_intro; delete g_iff_true_intro; delete g_implies; @@ -507,6 +513,8 @@ name const & get_heq_refl_name() { return *g_heq_refl; } name const & get_heq_to_eq_name() { return *g_heq_to_eq; } name const & get_iff_name() { return *g_iff; } name const & get_iff_refl_name() { return *g_iff_refl; } +name const & get_iff_symm_name() { return *g_iff_symm; } +name const & get_iff_trans_name() { return *g_iff_trans; } name const & get_iff_false_intro_name() { return *g_iff_false_intro; } name const & get_iff_true_intro_name() { return *g_iff_true_intro; } name const & get_implies_name() { return *g_implies; } diff --git a/src/library/constants.h b/src/library/constants.h index 85a89eeec..ca8f490da 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -46,6 +46,8 @@ name const & get_heq_refl_name(); name const & get_heq_to_eq_name(); name const & get_iff_name(); name const & get_iff_refl_name(); +name const & get_iff_symm_name(); +name const & get_iff_trans_name(); name const & get_iff_false_intro_name(); name const & get_iff_true_intro_name(); name const & get_implies_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 153873db9..906637bf3 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -39,6 +39,8 @@ heq.refl heq.to_eq iff iff.refl +iff.symm +iff.trans iff_false_intro iff_true_intro implies diff --git a/src/library/relation_manager.cpp b/src/library/relation_manager.cpp index 6b012b6ae..b509ecfa1 100644 --- a/src/library/relation_manager.cpp +++ b/src/library/relation_manager.cpp @@ -256,6 +256,27 @@ optional get_trans_info(environment const & env, name const & op) { return optional(); } +refl_info_getter mk_refl_info_getter(environment const & env) { + auto t = rel_ext::get_state(env).m_refl_table; + return [=](name const & n) { return get_info(t, n); }; +} + +trans_info_getter mk_trans_info_getter(environment const & env) { + auto t = rel_ext::get_state(env).m_trans_table; + return [=](name const & op1, name const & op2) { + if (auto it = t.find(mk_pair(op1, op2))) { + return optional(*it); + } else { + return optional(); + } + }; +} + +symm_info_getter mk_symm_info_getter(environment const & env) { + auto t = rel_ext::get_state(env).m_symm_table; + return [=](name const & n) { return get_info(t, n); }; +} + bool is_equivalence(environment const & env, name const & rop) { return rel_ext::get_state(env).is_equivalence(rop); } diff --git a/src/library/relation_manager.h b/src/library/relation_manager.h index 35e4c868a..65b76c76f 100644 --- a/src/library/relation_manager.h +++ b/src/library/relation_manager.h @@ -71,6 +71,14 @@ optional get_refl_info(environment const & env, name const & op); optional get_symm_info(environment const & env, name const & op); optional get_trans_info(environment const & env, name const & op); +typedef std::function(name const &)> refl_info_getter; +typedef std::function(name const &, name const &)> trans_info_getter; +typedef std::function(name const &)> symm_info_getter; + +refl_info_getter mk_refl_info_getter(environment const & env); +trans_info_getter mk_trans_info_getter(environment const & env); +symm_info_getter mk_symm_info_getter(environment const & env); + bool is_subst_relation(environment const & env, name const & op); inline bool is_trans_relation(environment const & env, name const & op) { return static_cast(get_trans_info(env, op)); } inline bool is_symm_relation(environment const & env, name const & op) { return static_cast(get_symm_info(env, op)); } diff --git a/src/library/util.cpp b/src/library/util.cpp index b75adee67..332c95bd5 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -486,6 +486,13 @@ bool is_iff(expr const & e) { expr const & fn = get_app_fn(e); return is_constant(fn) && const_name(fn) == get_iff_name(); } +bool is_iff(expr const & e, expr & lhs, expr & rhs) { + if (!is_iff(e) || !is_app(app_fn(e))) + return false; + lhs = app_arg(app_fn(e)); + rhs = app_arg(e); + return true; +} expr mk_iff(expr const & lhs, expr const & rhs) { return mk_app(mk_constant(get_iff_name()), lhs, rhs); } diff --git a/src/library/util.h b/src/library/util.h index a0f315112..6195965b8 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -173,6 +173,7 @@ bool is_heq(expr const & e, expr & A, expr & lhs, expr & B, expr & rhs); bool is_ite(expr const & e, expr & c, expr & H, expr & A, expr & t, expr & f); bool is_iff(expr const & e); +bool is_iff(expr const & e, expr & lhs, expr & rhs); expr mk_iff(expr const & lhs, expr const & rhs); expr mk_iff_refl(expr const & a); /** \brief Given iff_pr : iff_term, where \c iff_term is of the form l <-> r,