feat(library/app_builder): add helper methods for creating binary relations, and refl/symm/trans proofs

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<key, entry, key_hash_fn> 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<expr> mk_app(name const & /* c */, unsigned /* mask_sz */, bool const * /* mask */, expr const * /* args */) {
         return none_expr();
     }
+
+    optional<level> 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<expr> 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<expr> mk_iff(expr const & a, expr const & b) {
+        return some_expr(::lean::mk_app(mk_constant(get_iff_name()), a, b));
+    }
+
+    optional<expr> 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<expr> mk_iff_refl(expr const & a) {
+        return some_expr(::lean::mk_app(mk_constant(get_iff_refl_name()), a));
+    }
+
+    optional<expr> 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<expr> 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<expr> 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<expr> 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<expr> 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<expr> 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<expr> 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<expr> 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<expr> app_builder::mk_app(name const & c, unsigned mask_sz, bool const
     return m_ptr->mk_app(c, mask_sz, mask, args);
 }
 
+optional<expr> app_builder::mk_rel(name const & n, expr const & lhs, expr const & rhs) {
+    return m_ptr->mk_rel(n, lhs, rhs);
+}
+
+optional<expr> app_builder::mk_eq(expr const & lhs, expr const & rhs) {
+    return m_ptr->mk_eq(lhs, rhs);
+}
+
+optional<expr> app_builder::mk_iff(expr const & lhs, expr const & rhs) {
+    return m_ptr->mk_iff(lhs, rhs);
+}
+
+optional<expr> app_builder::mk_refl(name const & relname, expr const & a) {
+    return m_ptr->mk_refl(relname, a);
+}
+
+optional<expr> app_builder::mk_eq_refl(expr const & a) {
+    return m_ptr->mk_eq_refl(a);
+}
+
+optional<expr> app_builder::mk_iff_refl(expr const & a) {
+    return m_ptr->mk_iff_refl(a);
+}
+
+optional<expr> app_builder::mk_symm(name const & relname, expr const & H) {
+    return m_ptr->mk_symm(relname, H);
+}
+
+optional<expr> app_builder::mk_eq_symm(expr const & H) {
+    return m_ptr->mk_eq_symm(H);
+}
+
+optional<expr> app_builder::mk_iff_symm(expr const & H) {
+    return m_ptr->mk_iff_symm(H);
+}
+
+optional<expr> app_builder::mk_trans(name const & relname, expr const & H1, expr const & H2) {
+    return m_ptr->mk_trans(relname, H1, H2);
+}
+
+optional<expr> app_builder::mk_eq_trans(expr const & H1, expr const & H2) {
+    return m_ptr->mk_eq_trans(H1, H2);
+}
+
+optional<expr> 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<expr> const & ctx) {
     m_ptr->m_ctx->set_context(ctx);
 }

src/library/app_builder.h

@@ -63,6 +63,26 @@ public:
 
     optional<expr> 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<expr> mk_rel(name const & n, expr const & lhs, expr const & rhs);
+    optional<expr> mk_eq(expr const & lhs, expr const & rhs);
+    optional<expr> mk_iff(expr const & lhs, expr const & rhs);
+
+    /** \brief Similar a reflexivity proof for the given relation */
+    optional<expr> mk_refl(name const & relname, expr const & a);
+    optional<expr> mk_eq_refl(expr const & a);
+    optional<expr> mk_iff_refl(expr const & a);
+
+    /** \brief Similar a symmetry proof for the given relation */
+    optional<expr> mk_symm(name const & relname, expr const & H);
+    optional<expr> mk_eq_symm(expr const & H);
+    optional<expr> mk_iff_symm(expr const & H);
+
+    /** \brief Similar a transitivity proof for the given relation */
+    optional<expr> mk_trans(name const & relname, expr const & H1, expr const & H2);
+    optional<expr> mk_eq_trans(expr const & H1, expr const & H2);
+    optional<expr> 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.
 

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; }

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();

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

src/library/relation_manager.cpp

@@ -256,6 +256,27 @@ optional<name> get_trans_info(environment const & env, name const & op) {
         return optional<name>();
 }
 
+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<trans_info>(*it);
+        } else {
+            return optional<trans_info>();
+        }
+    };
+}
+
+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);
 }

src/library/relation_manager.h

@@ -71,6 +71,14 @@ optional<name> get_refl_info(environment const & env, name const & op);
 optional<name> get_symm_info(environment const & env, name const & op);
 optional<name> get_trans_info(environment const & env, name const & op);
 
+typedef std::function<optional<refl_info>(name const &)>  refl_info_getter;
+typedef std::function<optional<trans_info>(name const &, name const &)> trans_info_getter;
+typedef std::function<optional<symm_info>(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<bool>(get_trans_info(env, op)); }
 inline bool is_symm_relation(environment const & env, name const & op) { return static_cast<bool>(get_symm_info(env, op)); }

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);
 }

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 <tt>iff_pr : iff_term</tt>, where \c iff_term is of the form <tt>l <-> r</tt>,