feat(library/congr_lemma_manager): handle simple congruence lemmas

src/library/app_builder.cpp

@@ -260,6 +260,10 @@ struct app_builder::imp {
         return some_expr(m_ctx->instantiate_uvars_mvars(e->m_app));
     }
 
+    optional<expr> mk_app(name const & c, std::initializer_list<expr> const & it) {
+        return mk_app(c, it.size(), it.begin());
+    }
+
     static unsigned get_nargs(unsigned mask_sz, bool const * mask) {
         unsigned nargs = 0;
         for (unsigned i = 0; i < mask_sz; i++) {
@@ -447,6 +451,22 @@ struct app_builder::imp {
         name const & eqrec = is_standard(m_ctx->env()) ? get_eq_drec_name() : get_eq_rec_name();
         return some_expr(::lean::mk_app({mk_constant(eqrec, {l_1, *A_lvl}), A, lhs, motive, H1, rhs, H2}));
     }
+
+    optional<expr> mk_congr_arg(expr const & f, expr const & H) {
+        // TODO(Leo): efficient version
+
+        return mk_app(get_congr_arg_name(), {f, H});
+    }
+
+    optional<expr> mk_congr_fun(expr const & H, expr const & a) {
+        // TODO(Leo): efficient version
+        return mk_app(get_congr_fun_name(), {H, a});
+    }
+
+    optional<expr> mk_congr(expr const & H1, expr const & H2) {
+        // TODO(Leo): efficient version
+        return mk_app(get_congr_name(), {H1, H2});
+    }
 };
 
 app_builder::app_builder(environment const & env, io_state const & ios, reducible_behavior b):
@@ -527,6 +547,18 @@ optional<expr> app_builder::mk_eq_drec(expr const & C, expr const & H1, expr con
     return m_ptr->mk_eq_drec(C, H1, H2);
 }
 
+optional<expr> app_builder::mk_congr_arg(expr const & f, expr const & H) {
+    return m_ptr->mk_congr_arg(f, H);
+}
+
+optional<expr> app_builder::mk_congr_fun(expr const & H, expr const & a) {
+    return m_ptr->mk_congr_fun(H, a);
+}
+
+optional<expr> app_builder::mk_congr(expr const & H1, expr const & H2) {
+    return m_ptr->mk_congr(H1, H2);
+}
+
 optional<expr> app_builder::mk_sorry(expr const & type) {
     return mk_app(get_sorry_name(), type);
 }

src/library/app_builder.h

@@ -106,6 +106,10 @@ public:
         because eq.rec is a dependent eliminator in HoTT. */
     optional<expr> mk_eq_drec(expr const & C, expr const & H1, expr const & H2);
 
+    optional<expr> mk_congr_arg(expr const & f, expr const & H);
+    optional<expr> mk_congr_fun(expr const & H, expr const & a);
+    optional<expr> mk_congr(expr const & H1, expr const & H2);
+
     /** \brief Create (@sorry type) */
     optional<expr> mk_sorry(expr const & type);
 

src/library/congr_lemma_manager.cpp

@@ -16,6 +16,7 @@ class congr_lemma_manager::imp {
     app_builder &      m_builder;
     fun_info_manager & m_fmanager;
     type_context &     m_ctx;
+    bool               m_ignore_inst_implicit;
     struct key {
         expr const & m_fn;
         unsigned     m_nargs;
@@ -94,6 +95,37 @@ class congr_lemma_manager::imp {
         }
     }
 
+    bool has_cast(buffer<congr_arg_kind> const & kinds) {
+        return std::find(kinds.begin(), kinds.end(), congr_arg_kind::Cast) != kinds.end();
+    }
+
+    optional<expr> mk_simple_congr_proof(expr const & fn, buffer<expr> const & lhss,
+                                         buffer<optional<expr>> const & eqs, buffer<congr_arg_kind> const & kinds) {
+        unsigned i = 0;
+        for (; i < kinds.size(); i++) {
+            if (kinds[i] != congr_arg_kind::Fixed)
+                break;
+        }
+        expr g = mk_app(fn, i, lhss.data());
+        if (i == kinds.size())
+            return m_builder.mk_eq_refl(g);
+        lean_assert(kinds[i] == congr_arg_kind::Eq);
+        lean_assert(eqs[i]);
+        optional<expr> pr = m_builder.mk_congr_arg(g, *eqs[i]);
+        if (!pr) return none_expr();
+        i++;
+        for (; i < kinds.size(); i++) {
+            if (kinds[i] == congr_arg_kind::Eq) {
+                pr = m_builder.mk_congr(*pr, *eqs[i]);
+            } else {
+                lean_assert(kinds[i] == congr_arg_kind::Fixed);
+                pr = m_builder.mk_congr_fun(*pr, lhss[i]);
+            }
+            if (!pr) return none_expr();
+        }
+        return pr;
+    }
+
     optional<result> mk_congr_simp(expr const & fn, buffer<param_info> const & pinfos, buffer<congr_arg_kind> const & kinds) {
         expr fn_type = whnf(infer(fn));
         name e_name("e");
@@ -146,15 +178,21 @@ class congr_lemma_manager::imp {
         if (!eq)
             return optional<result>();
         expr congr_type  = Pi(hyps, *eq);
-        auto congr_proof = m_builder.mk_sorry(congr_type);
+        optional<expr> congr_proof;
-        if (!congr_proof)
+        if (has_cast(kinds)) {
-            return optional<result>();
+            // TODO(Leo):
+            congr_proof = m_builder.mk_sorry(congr_type);
+        } else {
+            congr_proof = mk_simple_congr_proof(fn, lhss, eqs, kinds);
+        }
+        if (!congr_proof) return optional<result>();
+        congr_proof = Fun(hyps, *congr_proof);
         return optional<result>(congr_type, *congr_proof, to_list(kinds));
     }
 
 public:
-    imp(app_builder & b, fun_info_manager & fm):
+    imp(app_builder & b, fun_info_manager & fm, bool ignore_inst_implicit):
-        m_builder(b), m_fmanager(fm), m_ctx(fm.ctx()) {}
+        m_builder(b), m_fmanager(fm), m_ctx(fm.ctx()), m_ignore_inst_implicit(ignore_inst_implicit) {}
 
     optional<result> mk_congr_simp(expr const & fn) {
         fun_info finfo = m_fmanager.get(fn);
@@ -179,6 +217,9 @@ public:
                     kinds[i] = congr_arg_kind::Fixed;
                 else
                     kinds[i] = congr_arg_kind::Cast;
+            } else if (pinfos[i].is_inst_implicit()) {
+                lean_assert(!pinfos[i].is_subsingleton());
+                kinds[i] = congr_arg_kind::Fixed;
             }
         }
         for (unsigned i = 0; i < pinfos.size(); i++) {
@@ -206,8 +247,8 @@ public:
     }
 };
 
-congr_lemma_manager::congr_lemma_manager(app_builder & b, fun_info_manager & fm):
+congr_lemma_manager::congr_lemma_manager(app_builder & b, fun_info_manager & fm, bool ignore_inst_implicit):
-    m_ptr(new imp(b, fm)) {
+    m_ptr(new imp(b, fm, ignore_inst_implicit)) {
 }
 
 congr_lemma_manager::~congr_lemma_manager() {

src/library/congr_lemma_manager.h

@@ -14,7 +14,14 @@ class congr_lemma_manager {
     struct imp;
     std::unique_ptr<imp> m_ptr;
 public:
-    congr_lemma_manager(app_builder & b, fun_info_manager & fm);
+    /** \brief When ignore_inst_implicit is set to true, then
+        for type class instance implicit arguments that are *not* subsingletons,
+        the mananger will create congruence lemmas where these arguments remain fixed.
+        This is the behavior we want most of the time. For example, when creating a
+        congruence for
+             add : Pi {A : Type} [s : has_add A], A -> A -> A
+        we want the argumet s to remain fixed. */
+    congr_lemma_manager(app_builder & b, fun_info_manager & fm, bool ignore_inst_implicit = true);
     ~congr_lemma_manager();
 
     enum class congr_arg_kind { Fixed, Eq, Cast };

src/library/constants.cpp

@@ -16,6 +16,8 @@ name const * g_bool_tt = nullptr;
 name const * g_char = nullptr;
 name const * g_char_mk = nullptr;
 name const * g_congr = nullptr;
+name const * g_congr_arg = nullptr;
+name const * g_congr_fun = nullptr;
 name const * g_dite = nullptr;
 name const * g_div = nullptr;
 name const * g_empty = nullptr;
@@ -174,6 +176,8 @@ void initialize_constants() {
     g_char = new name{"char"};
     g_char_mk = new name{"char", "mk"};
     g_congr = new name{"congr"};
+    g_congr_arg = new name{"congr_arg"};
+    g_congr_fun = new name{"congr_fun"};
     g_dite = new name{"dite"};
     g_div = new name{"div"};
     g_empty = new name{"empty"};
@@ -333,6 +337,8 @@ void finalize_constants() {
     delete g_char;
     delete g_char_mk;
     delete g_congr;
+    delete g_congr_arg;
+    delete g_congr_fun;
     delete g_dite;
     delete g_div;
     delete g_empty;
@@ -491,6 +497,8 @@ name const & get_bool_tt_name() { return *g_bool_tt; }
 name const & get_char_name() { return *g_char; }
 name const & get_char_mk_name() { return *g_char_mk; }
 name const & get_congr_name() { return *g_congr; }
+name const & get_congr_arg_name() { return *g_congr_arg; }
+name const & get_congr_fun_name() { return *g_congr_fun; }
 name const & get_dite_name() { return *g_dite; }
 name const & get_div_name() { return *g_div; }
 name const & get_empty_name() { return *g_empty; }

src/library/constants.h

@@ -18,6 +18,8 @@ name const & get_bool_tt_name();
 name const & get_char_name();
 name const & get_char_mk_name();
 name const & get_congr_name();
+name const & get_congr_arg_name();
+name const & get_congr_fun_name();
 name const & get_dite_name();
 name const & get_div_name();
 name const & get_empty_name();

src/library/constants.txt

@@ -11,6 +11,8 @@ bool.tt
 char
 char.mk
 congr
+congr_arg
+congr_fun
 dite
 div
 empty

tests/lean/extra/congr.lean

@@ -2,8 +2,18 @@ section
 variables p : nat → Prop
 variables q : nat → nat → Prop
 variables f : Π (x y : nat), p x → q x y → nat
+example : (0:nat) = 0 := sorry
+
+#congr @add
+
+#congr p
+
+#congr iff
+
 end
 
+exit
+
 
 section
 variables p : nat → Prop