feat(library/congr_lemma_manager): add congr_lemma_manager skeleton and compute type of congruence lemma

proof is still missing

src/library/CMakeLists.txt

@@ -17,4 +17,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   composition_manager.cpp tc_multigraph.cpp noncomputable.cpp
   aux_recursors.cpp norm_num.cpp decl_stats.cpp meng_paulson.cpp
   norm_num.cpp class_instance_resolution.cpp type_context.cpp
-  tmp_type_context.cpp fun_info_manager.cpp)
+  tmp_type_context.cpp fun_info_manager.cpp congr_lemma_manager.cpp)

src/library/congr_lemma_manager.cpp

@@ -0,0 +1,198 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/instantiate.h"
+#include "kernel/abstract.h"
+#include "library/util.h"
+#include "library/locals.h"
+#include "library/replace_visitor.h"
+#include "library/congr_lemma_manager.h"
+
+namespace lean {
+class congr_lemma_manager::imp {
+    app_builder &      m_builder;
+    fun_info_manager & m_fmanager;
+    type_context &     m_ctx;
+    expr_map<result>   m_cache;
+
+    struct failure {
+        unsigned m_arg_idx;
+        failure(unsigned i):m_arg_idx(i) {}
+    };
+
+    expr infer(expr const & e) { return m_ctx.infer(e); }
+    expr whnf(expr const & e) { return m_ctx.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.
+        \remark deps is sorted. */
+    optional<expr> cast(expr const & e, expr const & type, list<unsigned> const & deps, buffer<optional<expr>> const & eqs) {
+        if (!deps)
+            return some_expr(e);
+        unsigned d = head(deps);
+        auto major = eqs[d];
+        if (!major) {
+            return cast(e, type, tail(deps), eqs);
+        } else {
+            expr lhs, rhs;
+            lean_verify(is_eq(mlocal_type(*major), lhs, rhs));
+            lean_assert(is_local(lhs));
+            lean_assert(is_local(rhs));
+            // We compute the motive by replacing rhs with the fresh local x,
+            // and major with fresh local H.
+            // We compute the new type by replacing rhs with lhs, and major with (refl lhs).
+            expr motive, new_type;
+            bool use_drec;
+            if (depends_on(type, *major)) {
+                // Since the type depends on the major, we must use dependent elimination.
+                // and the motive just abstract rhs and *major
+                use_drec  = true;
+                motive    = Fun(rhs, Fun(*major, type));
+                // We compute new_type by replacing rhs with lhs and *major with eq.refl(lhs) in type.
+                new_type  = instantiate(abstract(type, rhs), lhs);
+                auto refl = m_builder.mk_eq_refl(lhs);
+                if (!refl)
+                    return none_expr();
+                new_type  = instantiate(abstract(new_type, *major), *refl);
+            } else {
+                // type does not depend on the *major.
+                // So, the motive is just (fun rhs, type), and
+                // new_type just replaces rhs with lhs.
+                use_drec = false;
+                motive   = Fun(rhs, type);
+                new_type = instantiate(abstract(type, rhs), lhs);
+            }
+            auto minor = cast(e, new_type, tail(deps), eqs);
+            if (!minor)
+                return none_expr();
+            if (use_drec) {
+                return m_builder.mk_eq_drec(motive, *minor, *major);
+            } else {
+                return m_builder.mk_eq_rec(motive, *minor, *major);
+            }
+        }
+    }
+
+    optional<result> mk_congr_simp(expr const & fn, buffer<param_info> const & pinfos, buffer<congr_arg_kind> const & kinds) {
+        for (unsigned i = 0; i < kinds.size(); i++)
+            std::cout << (unsigned)kinds[i] << " ";
+        std::cout << "\n";
+
+        expr fn_type = whnf(infer(fn));
+        name e_name("e");
+        buffer<expr> lhss;
+        buffer<expr> rhss;          // it contains the right-hand-side argument
+        buffer<optional<expr>> eqs; // for Eq args, it contains the equality
+        buffer<expr> hyps;          // contains lhss + rhss + eqs
+        for (unsigned i = 0; i < pinfos.size(); i++) {
+            if (!is_pi(fn_type)) {
+                return optional<result>();
+            }
+            expr lhs = m_ctx.mk_tmp_local(binding_name(fn_type), binding_domain(fn_type));
+            lhss.push_back(lhs);
+            hyps.push_back(lhs);
+            switch (kinds[i]) {
+            case congr_arg_kind::Eq: {
+                expr rhs = m_ctx.mk_tmp_local(binding_name(fn_type), binding_domain(fn_type));
+                expr eq_type;
+                if (auto it = m_builder.mk_eq(lhs, rhs))
+                    eq_type = *it;
+                else
+                    return optional<result>();
+                rhss.push_back(rhs);
+                expr eq = m_ctx.mk_tmp_local(e_name.append_after(eqs.size()+1), eq_type);
+                eqs.push_back(some_expr(eq));
+                hyps.push_back(rhs);
+                hyps.push_back(eq);
+                break;
+            }
+            case congr_arg_kind::Fixed:
+                rhss.push_back(lhs);
+                eqs.push_back(none_expr());
+                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());
+                auto rhs = cast(lhs, rhs_type, pinfos[i].get_dependencies(), eqs);
+                if (!rhs) {
+                    return optional<result>();
+                }
+                rhss.push_back(*rhs);
+                eqs.push_back(none_expr());
+                break;
+            }}
+            // std::cout << lhss.back() << "\n";
+            // std::cout << rhss.back() << "\n\n";
+            fn_type  = whnf(instantiate(binding_body(fn_type), lhs));
+        }
+        expr lhs = mk_app(fn, lhss);
+        expr rhs = mk_app(fn, rhss);
+        auto eq  = m_builder.mk_eq(lhs, rhs);
+        if (!eq)
+            return optional<result>();
+        expr congr_type = Pi(hyps, *eq);
+        std::cout << congr_type << "\n";
+        // TODO(Leo): create proof
+        lean_unreachable();
+    }
+
+public:
+    imp(app_builder & b, fun_info_manager & fm):
+        m_builder(b), m_fmanager(fm), m_ctx(fm.ctx()) {}
+
+    optional<result> mk_congr_simp(expr const & fn) {
+        auto r = m_cache.find(fn);
+        if (r != m_cache.end())
+            return optional<result>(r->second);
+        fun_info finfo = m_fmanager.get(fn);
+        buffer<congr_arg_kind> kinds;
+        buffer<param_info>     pinfos;
+        to_buffer(finfo.get_params_info(), pinfos);
+        kinds.resize(pinfos.size(), congr_arg_kind::Eq);
+        for (unsigned i = 0; i < pinfos.size(); i++) {
+            if (pinfos[i].is_subsingleton()) {
+                if (empty(pinfos[i].get_dependencies()))
+                    kinds[i] = congr_arg_kind::Fixed;
+                else
+                    kinds[i] = congr_arg_kind::Cast;
+            }
+        }
+        for (unsigned i = 0; i < pinfos.size(); i++) {
+            for (unsigned j = i+1; j < pinfos.size(); j++) {
+                auto j_deps = pinfos[j].get_dependencies();
+                if (std::find(j_deps.begin(), j_deps.end(), i) != j_deps.end() &&
+                    kinds[j] == congr_arg_kind::Eq) {
+                    // We must fix i because there is a j that depends on i,
+                    // and j is not fixed nor a cast-fixed.
+                    kinds[i] = congr_arg_kind::Fixed;
+                    break;
+                }
+            }
+        }
+        while (true) {
+            try {
+                auto new_r = mk_congr_simp(fn, pinfos, kinds);
+                if (new_r)
+                    m_cache.insert(mk_pair(fn, *new_r));
+                return new_r;
+            } catch (failure & ex) {
+                kinds[ex.m_arg_idx] = congr_arg_kind::Fixed;
+            }
+        }
+    }
+};
+
+congr_lemma_manager::congr_lemma_manager(app_builder & b, fun_info_manager & fm):
+    m_ptr(new imp(b, fm)) {
+}
+
+congr_lemma_manager::~congr_lemma_manager() {
+}
+
+auto congr_lemma_manager::mk_congr_simp(expr const & fn) -> optional<result> {
+    return m_ptr->mk_congr_simp(fn);
+}
+}

src/library/congr_lemma_manager.h

@@ -0,0 +1,25 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <memory>
+#include "library/app_builder.h"
+#include "library/fun_info_manager.h"
+
+namespace lean {
+class congr_lemma_manager {
+    struct imp;
+    std::unique_ptr<imp> m_ptr;
+public:
+    congr_lemma_manager(app_builder & b, fun_info_manager & fm);
+    ~congr_lemma_manager();
+
+    enum class congr_arg_kind { Fixed, Eq, Cast };
+
+    typedef pair<expr, list<congr_arg_kind>> result;
+    optional<result> mk_congr_simp(expr const & fn);
+};
+}