diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp
index e10799b574..5ebae2772f 100644
--- a/src/library/tactic/simplify.cpp
+++ b/src/library/tactic/simplify.cpp
@@ -1,7 +1,7 @@
 /*
 Copyright (c) 2015 Daniel Selsam. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Daniel Selsam
+Author: Daniel Selsam, Leonardo de Moura
 */
 #include <functional>
 #include <iostream>
@@ -58,6 +58,583 @@ Author: Daniel Selsam
 #endif
 
 namespace lean {
+#define lean_simp_trace(CTX, N, CODE) lean_trace(N, scope_trace_env _scope1(CTX.env(), CTX); CODE)
+
+simp_result simplify_core_fn::join(simp_result const & r1, simp_result const & r2) {
+    return ::lean::join(m_ctx, m_rel, r1, r2);
+}
+
+void simplify_core_fn::inc_num_steps() {
+    m_num_steps++;
+    if (m_num_steps > m_max_steps)
+        throw exception("simplify failed, maximum number of steps exceeded");
+}
+
+bool simplify_core_fn::is_dependent_fn(expr const & f) {
+    expr f_type = m_ctx.whnf(m_ctx.infer(f));
+    lean_assert(is_pi(f_type));
+    return !is_arrow(f_type);
+}
+
+bool simplify_core_fn::instantiate_emetas(tmp_type_context & tmp_ctx, unsigned num_emeta,
+                                          list<expr> const & emetas, list<bool> const & instances) {
+    bool failed = false;
+    unsigned i  = num_emeta;
+    for_each2(emetas, instances, [&](expr const & mvar, bool const & is_instance) {
+            i--;
+            if (failed) return;
+            expr mvar_type = tmp_ctx.instantiate_mvars(tmp_ctx.infer(mvar));
+            if (has_metavar(mvar_type)) {
+                failed = true;
+                return;
+            }
+
+            if (tmp_ctx.is_eassigned(i)) return;
+
+            if (is_instance) {
+                if (auto v = m_ctx.mk_class_instance(mvar_type)) {
+                    if (!tmp_ctx.is_def_eq(mvar, *v)) {
+                        lean_simp_trace(tmp_ctx, name({"simplify", "failure"}),
+                                        tout() << "unable to assign instance for: " << mvar_type << "\n";);
+                        failed = true;
+                        return;
+                    }
+                } else {
+                    lean_simp_trace(tmp_ctx, name({"simplify", "failure"}),
+                                    tout() << "unable to synthesize instance for: " << mvar_type << "\n";);
+                    failed = true;
+                    return;
+                }
+            }
+
+            if (tmp_ctx.is_eassigned(i)) return;
+
+            if (m_ctx.is_prop(mvar_type)) {
+                if (auto pf = prove(mvar_type)) {
+                    lean_verify(tmp_ctx.is_def_eq(mvar, *pf));
+                    return;
+                }
+            }
+
+            lean_simp_trace(tmp_ctx, name({"simplify", "failure"}),
+                            tout() << "failed to assign: " << mvar << " : " << mvar_type << "\n";);
+
+            failed = true;
+            return;
+        });
+    return !failed;
+}
+
+simp_result simplify_core_fn::lift_from_eq(simp_result const & r_eq) {
+    if (!r_eq.has_proof()) return r_eq;
+    expr new_pr = ::lean::lift_from_eq(m_ctx, m_rel, r_eq.get_proof());
+    return simp_result(r_eq.get_new(), new_pr);
+}
+
+simp_lemmas simplify_core_fn::add_to_slss(simp_lemmas const & _slss, buffer<expr> const & ls) {
+    simp_lemmas slss = _slss;
+    for (unsigned i = 0; i < ls.size(); i++) {
+        expr const & l = ls[i];
+        try {
+            slss = add(m_ctx, slss, mlocal_name(l), m_ctx.infer(l), l, LEAN_DEFAULT_PRIORITY);
+            lean_simp_trace(m_ctx, name({"simplify", "context"}),
+                            tout() << mlocal_name(l) << " : " << m_ctx.infer(l) << "\n";);
+        } catch (exception & e) {}
+    }
+    return slss;
+}
+
+/* Given the application 'e', remove unnecessary casts of the form (eq.nrec a rfl) and (eq.drec a rfl) */
+expr simplify_core_fn::remove_unnecessary_casts(expr const & e) {
+    buffer<expr> args;
+    expr f = get_app_args(e, args);
+    ss_param_infos ss_infos = get_specialized_subsingleton_info(m_ctx, e);
+    int i = -1;
+    bool modified = false;
+    for (ss_param_info const & ss_info : ss_infos) {
+        i++;
+        if (ss_info.is_subsingleton()) {
+            while (is_constant(get_app_fn(args[i]))) {
+                buffer<expr> cast_args;
+                expr f_cast = get_app_args(args[i], cast_args);
+                name n_f = const_name(f_cast);
+                if (n_f == get_eq_rec_name() || n_f == get_eq_drec_name() || n_f == get_eq_nrec_name()) {
+                    lean_assert(cast_args.size() == 6);
+                    expr major_premise = cast_args[5];
+                    expr f_major_premise = get_app_fn(major_premise);
+                    if (is_constant(f_major_premise) && const_name(f_major_premise) == get_eq_refl_name()) {
+                        args[i] = cast_args[3];
+                        modified = true;
+                    } else {
+                        break;
+                    }
+                } else {
+                    break;
+                }
+            }
+        }
+    }
+    return modified ? mk_app(f, args) : e;
+}
+
+expr simplify_core_fn::defeq_canonize_args_step(expr const & e) {
+    buffer<expr> args;
+    bool modified = false;
+    expr f        = get_app_args(e, args);
+    fun_info info = get_fun_info(m_ctx, f, args.size());
+    unsigned i    = 0;
+    for (param_info const & pinfo : info.get_params_info()) {
+        lean_assert(i < args.size());
+        expr new_a;
+        if ((m_canonize_instances && pinfo.is_inst_implicit()) || (m_canonize_proofs && pinfo.is_prop())) {
+            new_a = ::lean::defeq_canonize(m_ctx, args[i], m_need_restart);
+            lean_simp_trace(m_ctx, name({"simplify", "canonize"}),
+                            tout() << "\n" << args[i] << "\n==>\n" << new_a << "\n";);
+            if (new_a != args[i]) {
+                modified = true;
+                args[i] = new_a;
+            }
+        }
+        i++;
+    }
+
+    return modified ? mk_app(f, args) : e;
+}
+
+/* Try user defined congruence lemmas */
+simp_result simplify_core_fn::try_user_congrs(expr const & e) {
+    simp_lemmas_for const * sls = m_slss.find(m_rel);
+    if (!sls) return simp_result(e);
+
+    list<simp_lemma> const * cls = sls->find_congr(e);
+    if (!cls) return simp_result(e);
+
+    for (simp_lemma const & cl : *cls) {
+        simp_result r = try_user_congr(e, cl);
+        if (r.get_new() != e)
+            return r;
+    }
+    return simp_result(e);
+}
+
+simp_result simplify_core_fn::try_user_congr(expr const & e, simp_lemma const & cl) {
+    tmp_type_context tmp_ctx(m_ctx, cl.get_num_umeta(), cl.get_num_emeta());
+    if (!tmp_ctx.is_def_eq(e, cl.get_lhs()))
+        return simp_result(e);
+
+    lean_simp_trace(tmp_ctx, name({"debug", "simplify", "try_congruence"}),
+                    tout() << "(" << cl.get_id() << ") " << e << "\n";);
+
+    bool simplified = false;
+
+    buffer<expr> congr_hyps;
+    to_buffer(cl.get_congr_hyps(), congr_hyps);
+
+    buffer<simp_result> congr_hyp_results;
+    buffer<type_context::tmp_locals> factories;
+    buffer<name> relations;
+    for (expr const & m : congr_hyps) {
+        factories.emplace_back(m_ctx);
+        type_context::tmp_locals & local_factory = factories.back();
+        expr m_type = tmp_ctx.instantiate_mvars(tmp_ctx.infer(m));
+
+        while (is_pi(m_type)) {
+            expr d = instantiate_rev(binding_domain(m_type), local_factory.as_buffer().size(), local_factory.as_buffer().data());
+            expr l = local_factory.push_local(binding_name(m_type), d, binding_info(m_type));
+            lean_assert(!has_metavar(l));
+            m_type = binding_body(m_type);
+        }
+        m_type = instantiate_rev(m_type, local_factory.as_buffer().size(), local_factory.as_buffer().data());
+
+        expr h_rel, h_lhs, h_rhs;
+        lean_verify(is_simp_relation(tmp_ctx.env(), m_type, h_rel, h_lhs, h_rhs) && is_constant(h_rel));
+        {
+            relations.push_back(const_name(h_rel));
+            flet<simp_lemmas> set_slss(m_slss, m_contextual ? add_to_slss(m_slss, local_factory.as_buffer()) : m_slss);
+
+            h_lhs = tmp_ctx.instantiate_mvars(h_lhs);
+
+            if (m_contextual || m_rel != const_name(h_rel)) {
+                flet<name> set_name(m_rel, const_name(h_rel));
+                freset<simplify_cache> reset_cache(m_cache);
+                congr_hyp_results.emplace_back(visit(h_lhs, some_expr(e)));
+            } else {
+                congr_hyp_results.emplace_back(visit(h_lhs, some_expr(e)));
+            }
+            simp_result const & r_congr_hyp = congr_hyp_results.back();
+
+            if (r_congr_hyp.has_proof())
+                simplified = true;
+
+            lean_assert(is_meta(h_rhs));
+            buffer<expr> new_val_meta_args;
+            expr new_val_meta = get_app_args(h_rhs, new_val_meta_args);
+            lean_assert(is_metavar(new_val_meta));
+            expr new_val = tmp_ctx.mk_lambda(new_val_meta_args, r_congr_hyp.get_new());
+            tmp_ctx.assign(new_val_meta, new_val);
+        }
+    }
+
+    if (!simplified)
+        return simp_result(e);
+
+    lean_assert(congr_hyps.size() == congr_hyp_results.size());
+    for (unsigned i = 0; i < congr_hyps.size(); ++i) {
+        expr const & pf_meta = congr_hyps[i];
+        simp_result const & r_congr_hyp = congr_hyp_results[i];
+        name const & rel = relations[i];
+        type_context::tmp_locals & local_factory = factories[i];
+        expr hyp = finalize(m_ctx, rel, r_congr_hyp).get_proof();
+        // This is the current bottleneck
+        // Can address somewhat by keeping the proofs as small as possible using macros
+        expr pf = local_factory.mk_lambda(hyp);
+        tmp_ctx.assign(pf_meta, pf);
+    }
+
+    if (!instantiate_emetas(tmp_ctx, cl.get_num_emeta(), cl.get_emetas(), cl.get_instances()))
+        return simp_result(e);
+
+    for (unsigned i = 0; i < cl.get_num_umeta(); i++) {
+        if (!tmp_ctx.is_uassigned(i))
+            return simp_result(e);
+    }
+
+    expr e_s = tmp_ctx.instantiate_mvars(cl.get_rhs());
+    expr pf = tmp_ctx.instantiate_mvars(cl.get_proof());
+
+    simp_result r(e_s, pf);
+
+    lean_simp_trace(tmp_ctx, name({"simplify", "congruence"}),
+                    tout() << "(" << cl.get_id() << ") "
+                    << "[" << e << " ==> " << e_s << "]\n";);
+
+    return r;
+}
+
+/* Try to use congruence lemmas generated by the congr_lemma module.
+   \remark these lemmas are for the equality relation. */
+optional<simp_result> simplify_core_fn::try_auto_eq_congr(expr const & e) {
+    lean_assert(m_rel == get_eq_name());
+    lean_assert(is_app(e));
+    buffer<expr> args;
+    expr f = get_app_args(e, args);
+    auto congr_lemma = mk_specialized_congr_simp(m_ctx, e);
+    if (!congr_lemma) return optional<simp_result>();
+
+    buffer<simp_result> r_args;
+    buffer<expr>        new_args;
+    bool has_proof = false;
+    bool has_cast = false;
+    bool has_simplified = false;
+
+    unsigned i = 0;
+
+    // First pass, try to simplify all the Eq arguments
+    for (congr_arg_kind const & ckind : congr_lemma->get_arg_kinds()) {
+        switch (ckind) {
+        case congr_arg_kind::HEq:
+            lean_unreachable();
+        case congr_arg_kind::Fixed:
+        case congr_arg_kind::FixedNoParam:
+            new_args.emplace_back(args[i]);
+            break;
+        case congr_arg_kind::Eq:
+            {
+                r_args.emplace_back(visit(args[i], some_expr(e)));
+                simp_result & r_arg = r_args.back();
+                new_args.emplace_back(r_arg.get_new());
+                if (r_arg.has_proof())
+                    has_proof = true;
+                if (r_arg.get_new() != args[i])
+                    has_simplified = true;
+            }
+            break;
+        case congr_arg_kind::Cast:
+            has_cast = true;
+            new_args.emplace_back(args[i]);
+            break;
+        }
+        i++;
+    }
+
+    if (!has_simplified) {
+        simp_result r = simp_result(e);
+        return optional<simp_result>(r);
+    }
+
+    if (!has_proof) {
+        simp_result r = simp_result(mk_app(f, new_args));
+        return optional<simp_result>(r);
+    }
+
+    // We have a proof, so we need to build the congruence lemma
+    expr proof = congr_lemma->get_proof();
+    expr type = congr_lemma->get_type();
+    buffer<expr> subst;
+
+    i = 0;
+    unsigned i_eq = 0;
+    for (congr_arg_kind const & ckind : congr_lemma->get_arg_kinds()) {
+        switch (ckind) {
+        case congr_arg_kind::HEq:
+            lean_unreachable();
+        case congr_arg_kind::Fixed:
+            proof = mk_app(proof, args[i]);
+            subst.push_back(args[i]);
+            type = binding_body(type);
+            break;
+        case congr_arg_kind::FixedNoParam:
+            break;
+        case congr_arg_kind::Eq:
+            proof = mk_app(proof, args[i]);
+            subst.push_back(args[i]);
+            type = binding_body(type);
+            {
+                simp_result r_arg = finalize(m_ctx, m_rel, r_args[i_eq]);
+                proof = mk_app(proof, r_arg.get_new(), r_arg.get_proof());
+                subst.push_back(r_arg.get_new());
+                subst.push_back(r_arg.get_proof());
+            }
+            type = binding_body(binding_body(type));
+            i_eq++;
+            break;
+        case congr_arg_kind::Cast:
+            lean_assert(has_cast);
+            proof = mk_app(proof, args[i]);
+            subst.push_back(args[i]);
+            type = binding_body(type);
+            break;
+        }
+        i++;
+    }
+    lean_assert(is_eq(type));
+    expr rhs   = instantiate_rev(app_arg(type), subst.size(), subst.data());
+    simp_result r(rhs, proof);
+
+    if (has_cast) {
+        r.update(remove_unnecessary_casts(r.get_new()));
+    }
+
+    return optional<simp_result>(r);
+}
+
+simp_result simplify_core_fn::congr_fun_arg(simp_result const & r_f, simp_result const & r_arg) {
+    if (!r_f.has_proof() && !r_arg.has_proof()) return simp_result(mk_app(r_f.get_new(), r_arg.get_new()));
+    else if (!r_f.has_proof()) return congr_arg(r_f.get_new(), r_arg);
+    else if (!r_arg.has_proof()) return congr_fun(r_f, r_arg.get_new());
+    else return congr(r_f, r_arg);
+}
+
+simp_result simplify_core_fn::congr(simp_result const & r_f, simp_result const & r_arg) {
+    lean_assert(r_f.has_proof() && r_arg.has_proof());
+    // theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂
+    expr e  = mk_app(r_f.get_new(), r_arg.get_new());
+    expr pf = mk_congr(m_ctx, r_f.get_proof(), r_arg.get_proof());
+    return simp_result(e, pf);
+}
+
+simp_result simplify_core_fn::congr_fun(simp_result const & r_f, expr const & arg) {
+    lean_assert(r_f.has_proof());
+    // theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a
+    expr e  = mk_app(r_f.get_new(), arg);
+    expr pf = mk_congr_fun(m_ctx, r_f.get_proof(), arg);
+    return simp_result(e, pf);
+}
+
+simp_result simplify_core_fn::congr_arg(expr const & f, simp_result const & r_arg) {
+    lean_assert(r_arg.has_proof());
+    // theorem congr_arg {A B : Type} {a₁ a₂ : A} (f : A → B) : a₁ = a₂ → f a₁ = f a₂
+    expr e  = mk_app(f, r_arg.get_new());
+    expr pf = mk_congr_arg(m_ctx, f, r_arg.get_proof());
+    return simp_result(e, pf);
+}
+
+simp_result simplify_core_fn::congr_funs(simp_result const & r_f, buffer<expr> const & args) {
+    expr e = r_f.get_new();
+    for (unsigned i = 0; i < args.size(); ++i) {
+        e  = mk_app(e, args[i]);
+    }
+    if (!r_f.has_proof())
+        return simp_result(e);
+    expr pf = r_f.get_proof();
+    for (unsigned i = 0; i < args.size(); ++i) {
+        pf = mk_congr_fun(m_ctx, pf, args[i]);
+    }
+    return simp_result(e, pf);
+}
+
+simp_result simplify_core_fn::visit(expr const & e, optional<expr> const & parent) {
+    check_system("simplify");
+    inc_num_steps();
+    lean_trace_inc_depth("simplify");
+    lean_simp_trace(m_ctx, "simplify", tout() << m_rel << ": " << e << "\n";);
+
+    auto it = m_cache.find(e);
+    if (it != m_cache.end())
+        return it->second;
+
+    simp_result curr_result(e);
+    if (auto r1 = pre(e, parent)) {
+        if (!r1->second) {
+            m_cache.insert(mk_pair(e, r1->first));
+            return r1->first;
+        }
+        curr_result = r1->first;
+    }
+
+    while (true) {
+        simp_result new_result;
+        switch (curr_result.get_new().kind()) {
+        case expr_kind::Local:
+        case expr_kind::Meta:
+        case expr_kind::Sort:
+        case expr_kind::Constant:
+        case expr_kind::Macro:
+            new_result = curr_result;
+            break;
+        case expr_kind::Var:
+            lean_unreachable();
+        case expr_kind::Lambda:
+            new_result = join(curr_result, visit_lambda(curr_result.get_new()));
+            break;
+        case expr_kind::Pi:
+            new_result = join(curr_result, visit_pi(curr_result.get_new()));
+            break;
+        case expr_kind::App:
+            new_result = join(curr_result, visit_app(curr_result.get_new()));
+            break;
+        case expr_kind::Let:
+            new_result = join(curr_result, visit_let(curr_result.get_new()));
+            break;
+        }
+
+        if (auto r2 = post(new_result.get_new(), parent)) {
+            if (!r2->second) {
+                curr_result = join(new_result, r2->first);
+                break;
+            } else if (r2->first.get_new() == curr_result.get_new()) {
+                break;
+            } else {
+                /* continue simplifying */
+                curr_result = join(new_result, r2->first);
+            }
+        } else {
+            curr_result = new_result;
+            break;
+        }
+    }
+
+    if (m_lift_eq && m_rel != get_eq_name()) {
+        simp_result eq_result;
+        {
+            flet<name> use_eq(m_rel, get_eq_name());
+            freset<simplify_cache> reset_cache(m_cache);
+            eq_result = visit(curr_result.get_new(), parent);
+        }
+        if (eq_result.get_new() != curr_result.get_new()) {
+            curr_result = join(curr_result, lift_from_eq(eq_result));
+            curr_result = join(curr_result, visit(curr_result.get_new(), parent));
+        }
+    }
+
+    m_cache.insert(mk_pair(e, curr_result));
+    return curr_result;
+}
+
+simp_result simplify_core_fn::visit_fn(expr const & e) {
+    lean_assert(m_rel == get_eq_name());
+    lean_assert(is_app(e));
+    buffer<expr> args;
+    expr const & f = get_app_args(e, args);
+    simp_result r_f = visit(f, some_expr(e));
+    return congr_funs(r_f, args);
+}
+
+simp_result simplify_core_fn::visit_app(expr const & _e) {
+    lean_assert(is_app(_e));
+    expr e = should_defeq_canonize() ? defeq_canonize_args_step(_e) : _e;
+
+    // (1) Try user-defined congruences
+    simp_result r_user = try_user_congrs(e);
+    if (r_user.has_proof()) {
+        if (m_rel == get_eq_name()) {
+            return join(r_user, visit_fn(r_user.get_new()));
+        } else {
+            return r_user;
+        }
+    }
+
+    if (m_rel == get_eq_name()) {
+        // (2) Synthesize congruence lemma
+        optional<simp_result> r_args = try_auto_eq_congr(e);
+        if (r_args) return join(*r_args, visit_fn(r_args->get_new()));
+
+        // (3) Fall back on generic binary congruence
+        expr const & f = app_fn(e);
+        expr const & arg = app_arg(e);
+
+        simp_result r_f = visit(f, some_expr(e));
+
+        if (is_dependent_fn(f)) {
+            if (r_f.has_proof()) return congr_fun(r_f, arg);
+            else return mk_app(r_f.get_new(), arg);
+        } else {
+            simp_result r_arg = visit(arg, some_expr(e));
+            return congr_fun_arg(r_f, r_arg);
+        }
+    }
+
+    return simp_result(e);
+}
+
+optional<expr> simplify_core_fn::prove(expr const &) {
+    return none_expr();
+}
+
+simp_result simplify_core_fn::visit_lambda(expr const & e) {
+    return simp_result(e);
+}
+
+simp_result simplify_core_fn::visit_pi(expr const & e) {
+    return try_user_congrs(e);
+}
+
+simp_result simplify_core_fn::visit_let(expr const & e) {
+    return simp_result(e);
+}
+
+simp_result simplify_core_fn::visit_macro(expr const & e) {
+    return simp_result(e);
+}
+
+optional<pair<simp_result, bool>> simplify_core_fn::pre(expr const &, optional<expr> const &) {
+    return optional<pair<simp_result, bool>>();
+}
+
+optional<pair<simp_result, bool>> simplify_core_fn::post(expr const &, optional<expr> const &) {
+    return optional<pair<simp_result, bool>>();
+}
+
+simplify_core_fn::simplify_core_fn(type_context & ctx, simp_lemmas const & slss,
+                                   unsigned max_steps, bool contextual, bool lift_eq,
+                                   bool canonize_instances, bool canonize_proofs):
+    m_ctx(ctx), m_slss(slss), m_max_steps(max_steps), m_contextual(contextual),
+    m_lift_eq(lift_eq), m_canonize_instances(canonize_instances), m_canonize_proofs(canonize_proofs) {
+}
+
+simp_result simplify_core_fn::operator()(name const & rel, expr const & e) {
+    m_rel = rel;
+    m_cache.clear();
+    simp_result r(e);
+    while (true) {
+        m_need_restart = false;
+        r = join(r, visit(r.get_new(), none_expr()));
+        if (!m_need_restart || !should_defeq_canonize())
+            return r;
+        m_cache.clear();
+    }
+}
+
 
 static name * g_simplify_prefix = nullptr;
 name get_simplify_prefix_name() { return *g_simplify_prefix; }
@@ -102,8 +679,6 @@ static bool get_simplify_canonize_proofs_fixed_point(options const & o) {
     return o.get_bool(*g_simplify_canonize_proofs_fixed_point, LEAN_DEFAULT_SIMPLIFY_DEFEQ_CANONIZE_PROOFS_FIXED_POINT);
 }
 
-#define lean_simp_trace(tctx, n, code) lean_trace(n, scope_trace_env _scope1(tctx.env(), tctx); code)
-
 /* Main simplifier class */
 
 class simplifier {
diff --git a/src/library/tactic/simplify.h b/src/library/tactic/simplify.h
index bb356647cf..ef9e2151d0 100644
--- a/src/library/tactic/simplify.h
+++ b/src/library/tactic/simplify.h
@@ -1,7 +1,7 @@
 /*
 Copyright (c) 2015 Daniel Selsam. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Daniel Selsam
+Author: Daniel Selsam, Leonardo de Moura
 */
 #pragma once
 #include "kernel/expr_pair.h"
@@ -11,6 +11,90 @@ Author: Daniel Selsam
 #include "library/tactic/simp_result.h"
 
 namespace lean {
+/* Core simplification procedure. It performs the following tasks:
+   1- Manages the cache;
+   2- Applies congruence lemmas;
+   3- Canonizes instances & proofs;
+   4- Manages contextual rewriting
+
+   This is a base class for many simplification strategies.
+   Its behavior can be configured by overriding its virtual methods.
+   This class does *not* apply any simp lemma, nor it tries to
+   put subterms in weak-head-normal-form.
+
+   This class also does *not* use axioms. For example, it will
+   not use funext to go inside lambda terms. This feature is provided
+   by subclasses.
+
+   Remark: it is debatable whether the options m_lift_eq, m_canonize_instances and
+   m_canonize_proofs really need to be here. They may be moved to subclasses in the
+   future.
+*/
+class simplify_core_fn {
+protected:
+    typedef expr_struct_map<simp_result> simplify_cache;
+
+    type_context              m_ctx;
+    name                      m_rel;
+    simp_lemmas               m_slss;
+    simplify_cache            m_cache;
+
+    /* Logging */
+    unsigned                  m_num_steps{0};
+    bool                      m_need_restart{false};
+
+    /* Options */
+    unsigned                  m_max_steps;
+    bool                      m_contextual;
+    bool                      m_lift_eq;
+    bool                      m_canonize_instances;
+    bool                      m_canonize_proofs;
+
+    simp_result join(simp_result const & r1, simp_result const & r2);
+    void inc_num_steps();
+    bool is_dependent_fn(expr const & f);
+    bool should_defeq_canonize() const { return m_canonize_instances || m_canonize_proofs; }
+    bool instantiate_emetas(tmp_type_context & tmp_tctx, unsigned num_emeta, list<expr> const & emetas, list<bool> const & instances);
+    simp_result lift_from_eq(simp_result const & r_eq);
+    simp_lemmas add_to_slss(simp_lemmas const & slss, buffer<expr> const & ls);
+    expr remove_unnecessary_casts(expr const & e);
+    expr defeq_canonize_args_step(expr const & e);
+
+    /* Congruence */
+    simp_result try_user_congrs(expr const & e);
+    simp_result try_user_congr(expr const & e, simp_lemma const & cr);
+
+    optional<simp_result> try_auto_eq_congr(expr const & e);
+
+    simp_result congr_fun_arg(simp_result const & r_f, simp_result const & r_arg);
+    simp_result congr(simp_result const & r_f, simp_result const & r_arg);
+    simp_result congr_fun(simp_result const & r_f, expr const & arg);
+    simp_result congr_arg(expr const & f, simp_result const & r_arg);
+    simp_result congr_funs(simp_result const & r_f, buffer<expr> const & args);
+
+    /* Visitors */
+    virtual optional<pair<simp_result, bool>> pre(expr const & e, optional<expr> const & parent);
+    virtual optional<pair<simp_result, bool>> post(expr const & e, optional<expr> const & parent);
+
+    virtual optional<expr> prove(expr const & goal);
+
+    simp_result visit_fn(expr const & e);
+    virtual simp_result visit_lambda(expr const & e);
+    virtual simp_result visit_pi(expr const & e);
+    virtual simp_result visit_let(expr const & e);
+    virtual simp_result visit_app(expr const & e);
+    virtual simp_result visit_macro(expr const & e);
+
+    virtual simp_result visit(expr const & e, optional<expr> const & parent);
+
+public:
+    simplify_core_fn(type_context & ctx, simp_lemmas const & slss,
+                     unsigned max_steps, bool contextual, bool lift_eq,
+                     bool canonize_instances, bool canonize_proofs);
+
+    environment const & env() const;
+    simp_result operator()(name const & rel, expr const & e);
+};
 
 simp_result simplify(type_context & tctx, name const & rel, simp_lemmas const & simp_lemmas, vm_obj const & prove_fn, expr const & e);
 simp_result simplify(type_context & tctx, name const & rel, simp_lemmas const & simp_lemmas, expr const & e);