From 8e5e8e654006dd2ff3544f24db35bb4d3b28a057 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Wed, 4 Nov 2015 21:53:12 -0800
Subject: [PATCH] feat(library/blast/simplifier): basic infrastructure

---
 src/frontends/lean/builtin_cmds.cpp      |  37 +-
 src/frontends/lean/token_table.cpp       |   2 +-
 src/library/blast/CMakeLists.txt         |   2 +-
 src/library/blast/init_module.cpp        |   3 +
 src/library/blast/simplifier.cpp         | 621 +++++++++++++++++++++++
 src/library/blast/simplifier.h           |  43 ++
 src/library/constants.cpp                |   4 +-
 src/library/simplifier/ceqv.cpp          |  40 +-
 src/library/simplifier/ceqv.h            |   6 +-
 src/library/simplifier/simp_rule_set.cpp | 150 +++---
 src/library/simplifier/simp_rule_set.h   |  48 +-
 tests/lean/simplifier1.lean              |  16 +
 tests/lean/simplifier1.lean.expected.out |   3 +
 tests/lean/simplifier2.lean              |  15 +
 tests/lean/simplifier2.lean.expected.out |   2 +
 tests/lean/simplifier3.lean              |  36 ++
 tests/lean/simplifier3.lean.expected.out |   4 +
 tests/lean/simplifier4.lean              |  19 +
 tests/lean/simplifier4.lean.expected.out |   4 +
 tests/lean/simplifier5.lean              |  13 +
 tests/lean/simplifier5.lean.expected.out |  10 +
 tests/lean/simplifier6.lean              |  25 +
 tests/lean/simplifier6.lean.expected.out |   4 +
 tests/lean/simplifier7.lean              |  15 +
 tests/lean/simplifier7.lean.expected.out |   2 +
 tests/lean/simplifier8.lean              |  13 +
 tests/lean/simplifier8.lean.expected.out |   1 +
 27 files changed, 1017 insertions(+), 121 deletions(-)
 create mode 100644 src/library/blast/simplifier.cpp
 create mode 100644 src/library/blast/simplifier.h
 create mode 100644 tests/lean/simplifier1.lean
 create mode 100644 tests/lean/simplifier1.lean.expected.out
 create mode 100644 tests/lean/simplifier2.lean
 create mode 100644 tests/lean/simplifier2.lean.expected.out
 create mode 100644 tests/lean/simplifier3.lean
 create mode 100644 tests/lean/simplifier3.lean.expected.out
 create mode 100644 tests/lean/simplifier4.lean
 create mode 100644 tests/lean/simplifier4.lean.expected.out
 create mode 100644 tests/lean/simplifier5.lean
 create mode 100644 tests/lean/simplifier5.lean.expected.out
 create mode 100644 tests/lean/simplifier6.lean
 create mode 100644 tests/lean/simplifier6.lean.expected.out
 create mode 100644 tests/lean/simplifier7.lean
 create mode 100644 tests/lean/simplifier7.lean.expected.out
 create mode 100644 tests/lean/simplifier8.lean
 create mode 100644 tests/lean/simplifier8.lean.expected.out

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index b7c924a47..17a51f074 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -45,6 +45,8 @@ Author: Leonardo de Moura
 #include "library/congr_lemma_manager.h"
 #include "library/definitional/projection.h"
 #include "library/simplifier/simp_rule_set.h"
+#include "library/blast/blast.h"
+#include "library/blast/simplifier.h"
 #include "compiler/preprocess_rec.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/parser.h"
@@ -475,7 +477,7 @@ static void print_simp_rules(parser & p) {
     if (p.curr_is_identifier()) {
         ns = p.get_name_val();
         p.next();
-        s = get_simp_rule_sets(p.env(), ns);
+        s = get_simp_rule_sets(p.env(), p.ios(), ns);
     } else {
         s = get_simp_rule_sets(p.env());
     }
@@ -1311,6 +1313,38 @@ static environment congr_lemma_cmd(parser & p) {
     return env;
 }
 
+static environment simplify_cmd(parser & p) {
+    name rel = p.check_constant_next("invalid #simplify command, constant expected");
+    unsigned o = p.parse_small_nat();
+    
+    expr e; level_param_names ls;
+    std::tie(e, ls) = parse_local_expr(p);
+
+    blast::scope_debug scope(p.env(),p.ios());
+    blast::branch b;
+    blast::simp::result r = blast::simplify(b,rel,e);
+
+    flycheck_information info(p.regular_stream());
+    if (info.enabled()) {
+        p.display_information_pos(p.cmd_pos());
+        p.regular_stream() << "simplify result:\n";
+    }
+
+    if (r.is_none()) {
+        p.regular_stream() << "<refl>" << endl;
+    }
+    else {
+        auto tc = mk_type_checker(p.env(), p.mk_ngen());
+        expr pf_type = tc->check(r.get_proof(), ls).first;
+
+        if (o == 0) p.regular_stream() << r.get_new() << endl;
+        else if (o == 1) p.regular_stream() << r.get_proof() << endl;
+        else p.regular_stream() << pf_type << endl;
+    }
+
+    return p.env();
+}
+
 void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("open",              "create aliases for declarations, and use objects defined in other namespaces",
                         open_cmd));
@@ -1344,6 +1378,7 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("#accessible",       "(for debugging purposes) display number of accessible declarations for blast tactic", accessible_cmd));
     add_cmd(r, cmd_info("#decl_stats",       "(for debugging purposes) display declaration statistics", decl_stats_cmd));
     add_cmd(r, cmd_info("#relevant_thms",    "(for debugging purposes) select relevant theorems using Meng&Paulson heuristic", relevant_thms_cmd));
+    add_cmd(r, cmd_info("#simplify",         "(for debugging purposes) simplify given expression", simplify_cmd));    
 
     register_decl_cmds(r);
     register_inductive_cmd(r);
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 1acd2b5dd..b32ba961e 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -120,7 +120,7 @@ void init_token_table(token_table & t) {
          "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",
          "multiple_instances", "find_decl", "attribute", "persistent",
          "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq",
-         "#compile", "#accessible", "#decl_stats", "#relevant_thms", "#app_builder", "#refl", "#symm",
+         "#compile", "#accessible", "#decl_stats", "#relevant_thms", "#simplify", "#app_builder", "#refl", "#symm",
          "#trans", "#replace", "#congr", nullptr};
 
     pair<char const *, char const *> aliases[] =
diff --git a/src/library/blast/CMakeLists.txt b/src/library/blast/CMakeLists.txt
index d0f3d1fba..3a9f580ad 100644
--- a/src/library/blast/CMakeLists.txt
+++ b/src/library/blast/CMakeLists.txt
@@ -1,2 +1,2 @@
 add_library(blast OBJECT expr.cpp branch.cpp state.cpp blast.cpp
-  blast_tactic.cpp init_module.cpp)
+  blast_tactic.cpp init_module.cpp simplifier.cpp)
diff --git a/src/library/blast/init_module.cpp b/src/library/blast/init_module.cpp
index db2812a59..3beb0449c 100644
--- a/src/library/blast/init_module.cpp
+++ b/src/library/blast/init_module.cpp
@@ -8,16 +8,19 @@ Author: Leonardo de Moura
 #include "library/blast/branch.h"
 #include "library/blast/blast.h"
 #include "library/blast/blast_tactic.h"
+#include "library/blast/simplifier.h"
 
 namespace lean {
 void initialize_blast_module() {
     blast::initialize_expr();
     blast::initialize_branch();
     initialize_blast();
+    blast::initialize_simplifier();
     initialize_blast_tactic();
 }
 void finalize_blast_module() {
     finalize_blast_tactic();
+    blast::finalize_simplifier();    
     finalize_blast();
     blast::finalize_branch();
     blast::finalize_expr();
diff --git a/src/library/blast/simplifier.cpp b/src/library/blast/simplifier.cpp
new file mode 100644
index 000000000..5b69e8d6c
--- /dev/null
+++ b/src/library/blast/simplifier.cpp
@@ -0,0 +1,621 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#include "kernel/abstract.h"
+#include "kernel/expr_maps.h"
+#include "kernel/instantiate.h"
+#include "library/constants.h"
+#include "library/expr_lt.h"
+#include "library/class_instance_resolution.h"
+#include "library/relation_manager.h"
+#include "library/blast/expr.h"
+#include "library/blast/blast_exception.h"
+#include "library/blast/blast.h"
+#include "library/blast/simplifier.h"
+#include "library/simplifier/simp_rule_set.h"
+#include "library/simplifier/ceqv.h"
+#include "library/app_builder.h"
+#include "util/flet.h"
+#include "util/pair.h"
+#include "util/sexpr/option_declarations.h"
+#include <array>
+#include <iostream> // TODO just for occasional debugging
+
+#ifndef LEAN_DEFAULT_SIMPLIFY_MAX_STEPS
+#define LEAN_DEFAULT_SIMPLIFY_MAX_STEPS 100
+#endif
+#ifndef LEAN_DEFAULT_SIMPLIFY_TOP_DOWN
+#define LEAN_DEFAULT_SIMPLIFY_TOP_DOWN false
+#endif
+#ifndef LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE
+#define LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE true
+#endif
+#ifndef LEAN_DEFAULT_SIMPLIFY_MEMOIZE
+#define LEAN_DEFAULT_SIMPLIFY_MEMOIZE true
+#endif
+#ifndef LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL
+#define LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL true
+#endif
+#ifndef LEAN_DEFAULT_SIMPLIFY_EXPAND_MACROS
+#define LEAN_DEFAULT_SIMPLIFY_EXPAND_MACROS false
+#endif
+#ifndef LEAN_DEFAULT_SIMPLIFY_TRACE
+#define LEAN_DEFAULT_SIMPLIFY_TRACE false
+#endif
+
+namespace lean {
+namespace blast {
+
+using simp::result;
+
+/* Options */
+
+static name * g_simplify_max_steps     = nullptr;
+static name * g_simplify_top_down      = nullptr;
+static name * g_simplify_exhaustive    = nullptr;
+static name * g_simplify_memoize       = nullptr;
+static name * g_simplify_contextual    = nullptr;
+static name * g_simplify_expand_macros = nullptr;
+static name * g_simplify_trace         = nullptr;
+
+unsigned get_simplify_max_steps() {
+    return ios().get_options().get_unsigned(*g_simplify_max_steps, LEAN_DEFAULT_SIMPLIFY_MAX_STEPS);
+}
+
+bool get_simplify_top_down() {
+    return ios().get_options().get_bool(*g_simplify_top_down, LEAN_DEFAULT_SIMPLIFY_TOP_DOWN);
+}
+
+bool get_simplify_exhaustive() {
+    return ios().get_options().get_bool(*g_simplify_exhaustive, LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE);
+}
+
+bool get_simplify_memoize() {
+    return ios().get_options().get_bool(*g_simplify_memoize, LEAN_DEFAULT_SIMPLIFY_MEMOIZE);
+}
+
+bool get_simplify_contextual() {
+    return ios().get_options().get_bool(*g_simplify_contextual, LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL);
+}
+
+bool get_simplify_expand_macros() {
+    return ios().get_options().get_bool(*g_simplify_expand_macros, LEAN_DEFAULT_SIMPLIFY_EXPAND_MACROS);
+}
+
+bool get_simplify_trace() {
+    return ios().get_options().get_bool(*g_simplify_trace, LEAN_DEFAULT_SIMPLIFY_TRACE);
+}
+
+/* Main simplifier class */
+
+class simplifier {
+    blast_tmp_type_context                       m_tmp_tctx;
+    app_builder                                  m_app_builder;
+    branch                                       m_branch;
+    name                                         m_rel;
+
+    list<expr>                                   m_local_ctx;
+
+    /* Logging */
+    unsigned                                     m_num_steps{0};
+    unsigned                                     m_depth{0};
+
+    /* Options */
+    unsigned                                     m_max_steps{get_simplify_max_steps()};
+    bool                                         m_top_down{get_simplify_top_down()};
+    bool                                         m_exhaustive{get_simplify_exhaustive()};
+    bool                                         m_memoize{get_simplify_memoize()};
+    bool                                         m_contextual{get_simplify_contextual()};
+    bool                                         m_expand_macros{get_simplify_expand_macros()};
+    bool                                         m_trace{get_simplify_trace()};
+    
+    /* Cache */
+    expr_bi_struct_map<result>                   m_simplify_cache{};
+
+    /* Masks for building applications */
+    std::array<bool,6> eq_rec_all_mask{{true,true,true,true,true,true}};
+
+    /* Basic helpers */
+    bool using_eq() { return m_rel == get_eq_name(); }
+
+    bool is_dependent_fn(expr const & f) {
+        expr f_type = m_tmp_tctx->whnf(m_tmp_tctx->infer(f));
+        lean_assert(is_pi(f_type));
+        return has_free_vars(binding_body(f_type));
+    }
+
+    /* Results */
+    result lift_from_eq(expr const & x, result const & r);
+    result join(result const & r1, result const & r2);        
+    result funext(result const & r, expr const & l);
+    result finalize(result const & r);
+
+    /* Simplification */
+    result simplify(expr const & e);    
+    result simplify_lambda(expr const & e);
+    result simplify_pi(expr const & e);
+    result simplify_app(expr const & e);
+    result simplify_fun(expr const & e);
+    
+    /* Rewriting */
+    result rewrite(expr const & e);    
+    result rewrite(expr const & e, simp_rule const & sr);
+    void init_tmp_tctx_for(simp_rule_core const & sr);
+
+    /* Congruence */
+    result congr(result const & r_f, result const & r_arg);        
+    result congr_fun(result const & r_f, expr const & arg);
+    result congr_arg(expr const & f, result const & r_arg);
+    result congr_funs(result const & r_f, buffer<expr> const & args);    
+    
+    result try_congrs(expr const & e);    
+    result try_congr(expr const & e, congr_rule const & cr);
+
+public:
+    simplifier(branch const & b, name const & rel);
+    result operator()(expr const & e) { return simplify(e); }
+
+};
+
+/* Constructor */
+
+simplifier::simplifier(branch const & b, name const & rel):
+    m_app_builder(*m_tmp_tctx), m_branch(b), m_rel(rel) { }
+
+/* Results */
+
+result simplifier::lift_from_eq(expr const & x, result const & r) {
+    lean_assert(!r.is_none());
+
+    expr l = m_tmp_tctx->mk_tmp_local(m_tmp_tctx->infer(x));
+    auto motive_local = m_app_builder.mk_app(m_rel,x,l);
+    lean_assert(motive_local);
+
+    expr motive = Fun(l,*motive_local);
+    
+    auto Rxx = m_app_builder.mk_refl(m_rel,x);
+    lean_assert(Rxx);
+
+    auto pf = m_app_builder.mk_eq_rec(motive,*Rxx,r.get_proof());
+    return result(r.get_new(),pf);
+}
+
+result simplifier::join(result const & r1, result const & r2) {
+    /* Assumes that both results are with respect to the same relation */
+    if (r1.is_none()) {
+        return r2;
+    }
+    else if (r2.is_none()) {
+        return r1;
+    }
+    else {
+        auto trans = m_app_builder.mk_trans(m_rel,r1.get_proof(),r2.get_proof());
+        lean_assert(trans);
+        return result(r2.get_new(),*trans);
+    }
+}
+
+result simplifier::funext(result const & r, expr const & l) {
+    // theorem funext {f₁ f₂ : Πx : A, B x} : (∀x, f₁ x = f₂ x) → f₁ = f₂ :=
+    lean_assert(!r.is_none());
+    expr e = Fun(l,r.get_new());
+    if (auto pf = m_app_builder.mk_app(get_funext_name(),Fun(l,r.get_proof())))
+        return result(e,*pf);
+    else
+        throw blast_exception("failed on [funext] matching",e);
+}
+
+result simplifier::finalize(result const & r) {
+    if (!r.is_none()) return r;
+    if (auto pf = m_app_builder.mk_refl(m_rel,r.get_new()))
+        return result(r.get_new(),*pf);
+    else
+        throw blast_exception("failed on [refl] matching",r.get_new());
+}
+
+
+/* Simplification */
+
+result simplifier::simplify(expr const & e) {
+    m_num_steps++;
+    flet<unsigned> inc_depth(m_depth, m_depth+1);
+
+    if (m_trace) {
+        ios().get_diagnostic_channel() << m_num_steps << "." << m_depth << "." << m_rel << ": " << e << "\n";
+    }
+
+    if (m_num_steps > m_max_steps)
+        throw blast_exception("simplifier failed, maximum number of steps exceeded", e);
+
+    if (m_memoize) {
+        auto it = m_simplify_cache.find(e);
+        if (it != m_simplify_cache.end()) return it->second;
+    }
+    result r(e);
+
+    if (m_top_down) r = join(r, rewrite(whnf(r.get_new())));
+
+    r.update(whnf(r.get_new()));
+
+    switch (r.get_new().kind()) {
+    case expr_kind::Local:
+    case expr_kind::Meta:
+    case expr_kind::Sort:
+    case expr_kind::Constant:
+        // no-op
+        break;
+    case expr_kind::Var:
+        lean_unreachable();
+    case expr_kind::Macro:
+        /* TODO
+        if (m_expand_macros) {
+            if (auto m = blast::expand_macro(e)) r = join(r,simplify(whnf(*m)));
+        }
+        */
+        break;
+    case expr_kind::Lambda:
+        if (using_eq()) r = join(r,simplify_lambda(r.get_new()));
+        break;
+    case expr_kind::Pi:
+        r = join(r,simplify_pi(r.get_new()));
+        break;
+    case expr_kind::App:
+        r = join(r,simplify_app(r.get_new()));
+        break;
+    }
+
+    if (!m_top_down) r = join(r,rewrite(whnf(r.get_new())));
+
+    if (r.get_new() == e && !using_eq()) {
+        {
+            flet<name> use_eq(m_rel, get_eq_name());
+            r = simplify(r.get_new());
+        }
+        if (!r.is_none()) r = lift_from_eq(e,r);
+    }
+
+    if (m_exhaustive && r.get_new() != e) r = join(r,simplify(r.get_new()));
+
+    if (m_memoize) m_simplify_cache.insert(mk_pair(e, r));
+
+    return r;
+}
+    
+result simplifier::simplify_lambda(expr const & _e) {
+    lean_assert(is_lambda(_e));
+    expr e = _e;
+    
+    buffer<expr> ls;
+    while (is_lambda(e)) {
+        expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data());
+        expr l = m_tmp_tctx->mk_tmp_local(d,binding_info(e));
+        ls.push_back(l);
+        e = instantiate(binding_body(e),l);
+    }
+
+    result r = simplify(e);
+    if (r.is_none()) { return result(_e); }
+
+    for (int i = ls.size() - 1; i >= 0; --i) r = funext(r,ls[i]);
+
+    return r;
+}
+
+result simplifier::simplify_pi(expr const & e) {
+    lean_assert(is_pi(e));
+    return try_congrs(e);
+}
+
+result simplifier::simplify_app(expr const & e) {
+    lean_assert(is_app(e));
+    // TODO simplify operator as well, in cases (1) and (2)
+    
+    /* (1) Try user-defined congruences */
+    result r = try_congrs(e);
+    if (!r.is_none()) {
+        if (using_eq()) return join(r,simplify_fun(r.get_new()));
+        else return r;
+    }
+    
+    /* (2) Synthesize congruence lemma */
+    if (using_eq()) {
+        // TODO
+    }
+
+    /* (3) Fall back on generic binary congruence */
+    if (using_eq()) {
+        expr const & f = app_fn(e);
+        expr const & arg = app_arg(e);
+
+        result r_f = simplify(f);
+
+        if (is_dependent_fn(f)) {
+            if (r_f.is_none()) return e;
+            else return congr_fun(r_f,arg);
+        }
+        else {
+            result r_arg = simplify(arg);
+            if (r_f.is_none() && r_arg.is_none()) return e;
+            else if (r_f.is_none()) return congr_arg(f,r_arg);
+            else if (r_arg.is_none()) return congr_fun(r_f,arg);            
+            else return congr(r_f,r_arg);
+        }
+    }
+
+    return result(e);
+}
+
+result simplifier::simplify_fun(expr const & e) {
+    lean_assert(is_app(e));
+    buffer<expr> args;
+    expr const & f = get_app_args(e, args);
+    result r_f = simplify(f);
+    if (r_f.is_none()) return result(e);
+    else return congr_funs(simplify(f),args);
+}
+
+/* Rewriting */
+
+result simplifier::rewrite(expr const & e) {
+    result r(e);
+
+    /* First, we rewrite with local hypotheses */
+    //TODO
+
+    /* Next, we rewrite with the [simp_rule_set] */
+    simp_rule_set const * sr = get_simp_rule_sets(env()).find(m_rel);
+    if (!sr) return r;
+
+    list<simp_rule> const * srs = sr->find_simp(e);
+    if (!srs) return r;
+    
+    for_each(*srs,[&](simp_rule const & sr) { r = join(r,rewrite(r.get_new(),sr)); });
+    
+    return r;
+}
+
+result simplifier::rewrite(expr const & e, simp_rule const & sr) {
+    // TODO restore
+//    blast_tmp_type_context tmp_tctx(sr.get_num_umeta(),sr.get_num_emeta());
+    blast_tmp_type_context tmp_tctx;
+    tmp_tctx->clear();
+    tmp_tctx->set_next_uvar_idx(sr.get_num_umeta());
+    tmp_tctx->set_next_mvar_idx(sr.get_num_emeta());
+
+    if (!tmp_tctx->is_def_eq(e,sr.get_lhs())) return result(e);
+
+    /* Traverse metavariables backwards */
+    for (int i = sr.get_num_emeta() - 1; i >= 0; --i) {
+        expr const & m = sr.get_emeta(i);
+        bool is_instance = sr.is_instance(i);
+
+        if (is_instance) {
+            expr type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m));
+            if (auto v = tmp_tctx->mk_class_instance(type)) {
+                if (!tmp_tctx->force_assign(m, *v))
+                    return result(e);
+            } else {
+                return result(e);
+            }
+        }
+
+        if (tmp_tctx->is_mvar_assigned(i)) continue;
+
+        if (tmp_tctx->is_prop(tmp_tctx->infer(m))) {
+            // TODO try to prove
+            return result(e);
+        }
+
+        /* We fail if there is a meta variable that we still cannot assign */
+        return result(e);
+    }
+
+    for (unsigned i = 0; i < sr.get_num_umeta(); i++) {
+        if (!tmp_tctx->is_uvar_assigned(i)) return result(e);
+    }
+    
+    expr e_s = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs());
+
+    if (sr.is_perm() && !is_lt(e_s,e,false)) return result(e);
+    expr pf = tmp_tctx->instantiate_uvars_mvars(sr.get_proof());
+    return result(result(e_s,pf));
+}
+
+
+
+/* Congruence */
+result simplifier::congr(result const & r_f, result const & r_arg) {
+    lean_assert(!r_f.is_none() && !r_arg.is_none());
+    // 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());
+    if (auto pf = m_app_builder.mk_app(get_congr_name(),r_f.get_proof(),r_arg.get_proof()))
+        return result(e,*pf);
+    else
+        throw blast_exception("failed on [congr] matching",e);
+}
+
+result simplifier::congr_fun(result const & r_f, expr const & arg) {
+    lean_assert(!r_f.is_none());
+    // 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);
+    if (auto pf = m_app_builder.mk_app(get_congr_fun_name(),r_f.get_proof(),arg))
+        return result(e,*pf);
+    else
+        throw blast_exception("failed on [congr_fun] matching",e);        
+}
+
+result simplifier::congr_arg(expr const & f, result const & r_arg) {
+    lean_assert(!r_arg.is_none());
+    // 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());
+    if (auto pf = m_app_builder.mk_app(get_congr_arg_name(),f,r_arg.get_proof()))
+        return result(e,*pf);
+    else
+        throw blast_exception("failed on [congr_arg] matching",e);                
+}
+
+result simplifier::congr_funs(result const & r_f, buffer<expr> const & args) {
+    lean_assert(!r_f.is_none());
+    // congr_fun : ∀ {A : Type} {B : A → Type} {f g : Π (x : A), B x}, f = g → (∀ (a : A), f a = g a)
+    expr e = r_f.get_new();
+    expr pf = r_f.get_proof();
+    for (unsigned i = 0; i < args.size(); ++i) {
+        e = mk_app(e,args[i]);
+        auto p = m_app_builder.mk_app(get_congr_fun_name(),pf,args[i]);
+        if (p) pf = *p;
+        else throw blast_exception("failed on [congr_fun] matching",e);
+    }
+    return result(e,pf);
+}
+
+result simplifier::try_congrs(expr const & e) {
+    simp_rule_set const * sr = get_simp_rule_sets(env()).find(m_rel);
+    if (!sr) return result(e);
+
+    list<congr_rule> const * crs = sr->find_congr(e);
+    if (!crs) return result(e);
+
+    result r(e);
+    for_each(*crs,[&](congr_rule const & cr) {
+            if (!r.is_none()) return;
+            r = try_congr(e,cr);
+        }); 
+    return r;
+}
+
+result simplifier::try_congr(expr const & e, congr_rule const & cr) {
+    // TODO restore
+//    blast_tmp_type_context tmp_tctx(cr.get_num_umeta(),cr.get_num_emeta());
+    blast_tmp_type_context tmp_tctx;
+    tmp_tctx->clear();
+    tmp_tctx->set_next_uvar_idx(cr.get_num_umeta());
+    tmp_tctx->set_next_mvar_idx(cr.get_num_emeta());
+
+    if (!tmp_tctx->is_def_eq(e,cr.get_lhs())) return result(e);
+    
+    /* First, iterate over the congruence hypotheses */
+    bool failed = false;
+    bool simplified = false;
+    list<expr> const & congr_hyps = cr.get_congr_hyps();
+    for_each(congr_hyps,[&](expr const & m) {
+        if (failed) return;
+        buffer<expr> ls;
+        expr m_type = tmp_tctx->infer(m);
+
+        while (is_pi(m_type)) {
+            expr d = instantiate_rev(binding_domain(m_type), ls.size(), ls.data());
+            expr l = tmp_tctx->mk_tmp_local(d,binding_info(e));
+            ls.push_back(l);
+            m_type = instantiate(binding_body(m_type),l);
+        }
+
+        expr h_rel, h_lhs, h_rhs;
+        bool valid = is_simp_relation(env(), m_type, h_rel, h_lhs, h_rhs) && is_constant(h_rel);
+        lean_assert(valid);
+        {
+            flet<name> set_name(m_rel,const_name(h_rel));
+            flet<list<expr>> set_local_ctx(m_local_ctx,to_list(ls));
+            h_lhs = tmp_tctx->instantiate_uvars_mvars(h_lhs);
+            result r_congr_hyp = simplify(h_lhs);
+            expr hyp;
+            if (r_congr_hyp.is_none()) {
+                hyp = finalize(r_congr_hyp).get_proof();
+            }
+            else {
+                hyp = r_congr_hyp.get_proof();
+                simplified = true;
+            }
+            hyp = Fun(ls,hyp);
+            if (!tmp_tctx->is_def_eq(m,hyp)) failed = true;
+        }
+        });
+    if (failed || !simplified) return result(e);
+    /* Traverse metavariables backwards, proving or synthesizing the rest */
+    for (int i = cr.get_num_emeta() - 1; i >= 0; --i) {
+        expr const & m = cr.get_emeta(i);
+        bool is_instance = cr.is_instance(i);
+
+        if (is_instance) {
+            expr type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m));
+            if (auto v = tmp_tctx->mk_class_instance(type)) {
+                if (!tmp_tctx->force_assign(m, *v))
+                    return result(e);
+            } else {
+                return result(e);
+            }
+        }
+
+        if (tmp_tctx->is_mvar_assigned(i)) continue;
+
+        if (tmp_tctx->is_prop(tmp_tctx->infer(m))) {
+            // TODO try to prove
+            return result(e);
+        }
+
+        /* We fail if there is a meta variable that we still cannot assign */
+        return result(e);
+    }
+
+    for (unsigned i = 0; i < cr.get_num_umeta(); i++) {
+        if (!tmp_tctx->is_uvar_assigned(i)) return result(e);
+    }
+
+    expr e_s = tmp_tctx->instantiate_uvars_mvars(cr.get_rhs());
+    expr pf = tmp_tctx->instantiate_uvars_mvars(cr.get_proof());
+    return result(e_s,pf);
+}
+
+/* Setup and teardown */
+
+void initialize_simplifier() {
+    g_simplify_max_steps     = new name{"simplify", "max_steps"};
+    g_simplify_top_down      = new name{"simplify", "top_down"};
+    g_simplify_exhaustive    = new name{"simplify", "exhaustive"};
+    g_simplify_memoize       = new name{"simplify", "memoize"};
+    g_simplify_contextual    = new name{"simplify", "contextual"};
+    g_simplify_expand_macros = new name{"simplify", "expand_macros"};
+    g_simplify_trace         = new name{"simplify", "trace"};    
+
+    register_unsigned_option(*g_simplify_max_steps, LEAN_DEFAULT_SIMPLIFY_MAX_STEPS,
+                             "(simplify) max allowed steps in simplification");
+
+    register_bool_option(*g_simplify_top_down, LEAN_DEFAULT_SIMPLIFY_TOP_DOWN,
+                         "(simplify) use top-down rewriting instead of bottom-up");
+
+    register_bool_option(*g_simplify_exhaustive, LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE,
+                         "(simplify) rewrite exhaustively");
+
+    register_bool_option(*g_simplify_memoize, LEAN_DEFAULT_SIMPLIFY_MEMOIZE,
+                         "(simplify) memoize simplifications");
+
+    register_bool_option(*g_simplify_contextual, LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL,
+                         "(simplify) use contextual simplification");
+
+    register_bool_option(*g_simplify_expand_macros, LEAN_DEFAULT_SIMPLIFY_EXPAND_MACROS,
+                         "(simplify) expand macros");
+
+    register_bool_option(*g_simplify_trace, LEAN_DEFAULT_SIMPLIFY_TRACE,
+                         "(simplify) trace");
+    
+
+}
+
+void finalize_simplifier() {
+    delete g_simplify_trace;
+    delete g_simplify_expand_macros;
+    delete g_simplify_contextual;
+    delete g_simplify_memoize;
+    delete g_simplify_exhaustive;
+    delete g_simplify_top_down;    
+    delete g_simplify_max_steps;
+}
+
+/* Entry point */
+
+result simplify(branch const & b, name const & rel, expr const & e) {
+    return simplifier(b,rel)(e);
+}
+
+}}
diff --git a/src/library/blast/simplifier.h b/src/library/blast/simplifier.h
new file mode 100644
index 000000000..ac4293392
--- /dev/null
+++ b/src/library/blast/simplifier.h
@@ -0,0 +1,43 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#pragma once
+#include "kernel/expr_pair.h"
+#include "library/blast/branch.h"
+
+namespace lean {
+namespace blast {
+
+namespace simp {
+
+/* Struct to store results of simplification */
+struct result {
+    /* Invariant [m_pf : m_orig <rel> m_new] */
+    expr m_new;
+    optional<expr> m_proof;
+
+public:
+    result(expr const & e): m_new(e) {}
+    result(expr const & e, expr const & pf): m_new(e), m_proof(pf) {}
+    result(expr const & e, optional<expr> const & pf): m_new(e), m_proof(pf) {}
+
+    bool is_none() const { return !static_cast<bool>(m_proof); }
+    expr get_new() const { return m_new; }
+    expr get_proof() const { lean_assert(m_proof); return *m_proof; }
+
+    /* The following assumes that [e] and [m_new] are definitionally equal */
+    void update(expr const & e) { m_new = e; }
+        
+};
+
+}
+
+simp::result simplify(branch const & b, name const & rel, expr const & e);
+
+void initialize_simplifier();
+void finalize_simplifier();
+
+}
+}
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 109dde065..720ce09d6 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -178,6 +178,8 @@ void initialize_constants() {
     g_congr = new name{"congr"};
     g_congr_arg = new name{"congr_arg"};
     g_congr_fun = new name{"congr_fun"};
+    g_congr_fun = new name{"congr_fun"};
+    g_congr_arg = new name{"congr_arg"};
     g_dite = new name{"dite"};
     g_div = new name{"div"};
     g_empty = new name{"empty"};
@@ -336,9 +338,9 @@ void finalize_constants() {
     delete g_bool_tt;
     delete g_char;
     delete g_char_mk;
-    delete g_congr;
     delete g_congr_arg;
     delete g_congr_fun;
+    delete g_congr;
     delete g_dite;
     delete g_div;
     delete g_empty;
diff --git a/src/library/simplifier/ceqv.cpp b/src/library/simplifier/ceqv.cpp
index 21e243fbb..5b19272b9 100644
--- a/src/library/simplifier/ceqv.cpp
+++ b/src/library/simplifier/ceqv.cpp
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "kernel/type_checker.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "kernel/for_each_fn.h"
@@ -15,7 +14,7 @@ Author: Leonardo de Moura
 #include "library/simplifier/ceqv.h"
 
 namespace lean {
-bool is_ceqv(type_checker & tc, expr e);
+bool is_ceqv(tmp_type_context & tctx, expr e);
 
 bool is_simp_relation(environment const & env, name const & n) {
     return is_trans_relation(env, n) && is_refl_relation(env, n);
@@ -24,14 +23,14 @@ bool is_simp_relation(environment const & env, name const & n) {
 /** \brief Auxiliary functional object for creating "conditional equations" */
 class to_ceqvs_fn {
     environment const &   m_env;
-    type_checker &        m_tc;
+    tmp_type_context &        m_tctx;
 
     static list<expr_pair> mk_singleton(expr const & e, expr const & H) {
         return list<expr_pair>(mk_pair(e, H));
     }
 
     bool is_type(expr const & e) {
-        return is_sort(m_tc.whnf(m_tc.infer(e).first).first);
+        return is_sort(m_tctx.whnf(m_tctx.infer(e)));
     }
 
     bool is_relation(expr const & e) {
@@ -48,8 +47,7 @@ class to_ceqvs_fn {
     }
 
     bool is_prop(expr const & e) {
-        constraint_seq cs;
-        return m_tc.is_prop(e, cs) && !cs;
+        return m_tctx.is_prop(e);
     }
 
     // If restricted is true, we don't use (e <-> true) rewrite
@@ -69,7 +67,8 @@ class to_ceqvs_fn {
             auto r2 = apply(arg2, H2, restrited);
             return append(r1, r2);
         } else if (is_pi(e)) {
-            expr local = mk_local(m_tc.mk_fresh_name(), binding_name(e), binding_domain(e), binding_info(e));
+            // TODO(dhs): keep name?
+            expr local = m_tctx.mk_tmp_local(binding_domain(e), binding_info(e));
             expr new_e = instantiate(binding_body(e), local);
             expr new_H = mk_app(H, local);
             auto r = apply(new_e, new_H, restrited);
@@ -83,9 +82,9 @@ class to_ceqvs_fn {
             }
         } else if (is_standard(m_env) && is_ite(e, c, Hdec, A, arg1, arg2) && is_prop(e)) {
             // TODO(Leo): support HoTT mode if users request
-            expr not_c = mk_not(m_tc, c);
-            expr Hc    = mk_local(m_tc.mk_fresh_name(), c);
-            expr Hnc   = mk_local(m_tc.mk_fresh_name(), not_c);
+            expr not_c = mk_app(mk_constant(get_not_name()), c);
+            expr Hc    = m_tctx.mk_tmp_local(c);
+            expr Hnc   = m_tctx.mk_tmp_local(not_c);
             expr H1    = mk_app({mk_constant(get_implies_of_if_pos_name()),
                                  c, arg1, arg2, Hdec, e, Hc});
             expr H2    = mk_app({mk_constant(get_implies_of_if_neg_name()),
@@ -94,9 +93,8 @@ class to_ceqvs_fn {
             auto r2    = lift(Hnc, apply(arg2, H2, restrited));
             return append(r1, r2);
         } else if (!restrited) {
-            constraint_seq cs;
-            expr new_e = m_tc.whnf(e, cs);
-            if (new_e != e && !cs) {
+            expr new_e = m_tctx.whnf(e);
+            if (new_e != e) {
                 if (auto r = apply(new_e, H, true))
                     return r;
             }
@@ -112,17 +110,17 @@ class to_ceqvs_fn {
         }
     }
 public:
-    to_ceqvs_fn(type_checker & tc):m_env(tc.env()), m_tc(tc) {}
+    to_ceqvs_fn(tmp_type_context & tctx):m_env(tctx.env()), m_tctx(tctx) {}
 
     list<expr_pair> operator()(expr const & e, expr const & H) {
         bool restrited = false;
         list<expr_pair> lst = apply(e, H, restrited);
-        return filter(lst, [&](expr_pair const & p) { return is_ceqv(m_tc, p.first); });
+        return filter(lst, [&](expr_pair const & p) { return is_ceqv(m_tctx, p.first); });
     }
 };
 
-list<expr_pair> to_ceqvs(type_checker & tc, expr const & e, expr const & H) {
-    return to_ceqvs_fn(tc)(e, H);
+list<expr_pair> to_ceqvs(tmp_type_context & tctx, expr const & e, expr const & H) {
+    return to_ceqvs_fn(tctx)(e, H);
 }
 
 bool is_simp_relation(environment const & env, expr const & e, expr & rel, expr & lhs, expr & rhs) {
@@ -143,7 +141,7 @@ bool is_simp_relation(environment const & env, expr const & e, expr & lhs, expr
     return is_simp_relation(env, e, rel, lhs, rhs);
 }
 
-bool is_ceqv(type_checker & tc, expr e) {
+bool is_ceqv(tmp_type_context & tctx, expr e) {
     if (has_expr_metavar(e))
         return false;
     name_set to_find;
@@ -158,7 +156,7 @@ bool is_ceqv(type_checker & tc, expr e) {
             return true;
         }
     };
-    environment const & env = tc.env();
+    environment const & env = tctx.env();
     bool is_std = is_standard(env);
     buffer<expr> hypotheses; // arguments that are propositions
     while (is_pi(e)) {
@@ -168,11 +166,11 @@ bool is_ceqv(type_checker & tc, expr e) {
             // by matching the type.
             for_each(binding_domain(e), visitor_fn);
         }
-        expr local = mk_local(tc.mk_fresh_name(), binding_domain(e));
+        expr local = tctx.mk_tmp_local(binding_domain(e));
         if (binding_info(e).is_inst_implicit()) {
             // If the argument can be instantiated by type class resolution, then
             // we don't need to find it in the lhs
-        } else if (is_std && tc.is_prop(binding_domain(e)).first) {
+        } else if (is_std && tctx.is_prop(binding_domain(e))) {
             // If the argument is a proposition, we store it in hypotheses.
             // We check whether the lhs occurs in hypotheses or not.
             hypotheses.push_back(binding_domain(e));
diff --git a/src/library/simplifier/ceqv.h b/src/library/simplifier/ceqv.h
index b5ff0f464..b6e5868a8 100644
--- a/src/library/simplifier/ceqv.h
+++ b/src/library/simplifier/ceqv.h
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "kernel/type_checker.h"
+#include "library/tmp_type_context.h"
 #include "library/expr_pair.h"
 
 namespace lean {
@@ -14,7 +14,7 @@ bool is_simp_relation(environment const & env, expr const & e, expr & rel, expr
     a "conditional" rewriting rule. Any equivalence relation registered using
     the relation_manager is considered.
 */
-list<expr_pair> to_ceqvs(type_checker & tc, expr const & e, expr const & H);
-bool is_ceqv(type_checker & tc, expr e);
+list<expr_pair> to_ceqvs(tmp_type_context & tctx, expr const & e, expr const & H);
+bool is_ceqv(tmp_type_context & tctx, expr e);
 bool is_permutation_ceqv(environment const & env, expr e);
 }
diff --git a/src/library/simplifier/simp_rule_set.cpp b/src/library/simplifier/simp_rule_set.cpp
index 4509b3449..624f1a933 100644
--- a/src/library/simplifier/simp_rule_set.cpp
+++ b/src/library/simplifier/simp_rule_set.cpp
@@ -16,13 +16,14 @@ Author: Leonardo de Moura
 #include "library/simplifier/simp_rule_set.h"
 
 namespace lean {
-simp_rule_core::simp_rule_core(name const & id, levels const & univ_metas, list<expr> const & metas,
-                               expr const & lhs, expr const & rhs, expr const & proof):
-    m_id(id), m_univ_metas(univ_metas), m_metas(metas), m_lhs(lhs), m_rhs(rhs), m_proof(proof) {}
+simp_rule_core::simp_rule_core(name const & id, levels const & umetas, std::vector<expr> const & emetas,
+                               std::vector<bool> const & instances, expr const & lhs, expr const & rhs, expr const & proof):
+    m_id(id), m_umetas(umetas), m_emetas(emetas), m_instances(instances),
+    m_lhs(lhs), m_rhs(rhs), m_proof(proof) {}
 
-simp_rule::simp_rule(name const & id, levels const & univ_metas, list<expr> const & metas,
-                     expr const & lhs, expr const & rhs, expr const & proof, bool is_perm):
-    simp_rule_core(id, univ_metas, metas, lhs, rhs, proof),
+simp_rule::simp_rule(name const & id, levels const & umetas, std::vector<expr> const & emetas,
+                     std::vector<bool> const & instances, expr const & lhs, expr const & rhs, expr const & proof, bool is_perm):
+    simp_rule_core(id, umetas, emetas, instances, lhs, rhs, proof),
     m_is_permutation(is_perm) {}
 
 bool operator==(simp_rule const & r1, simp_rule const & r2) {
@@ -31,18 +32,19 @@ bool operator==(simp_rule const & r1, simp_rule const & r2) {
 
 format simp_rule::pp(formatter const & fmt) const {
     format r;
-    r += format("#") + format(length(m_metas));
+    r += format("#") + format(get_num_emeta());
     if (m_is_permutation)
         r += space() + format("perm");
-    format r1 = comma() + space() + fmt(m_lhs);
-    r1       += space() + format("↦") + pp_indent_expr(fmt, m_rhs);
+    format r1 = comma() + space() + fmt(get_lhs());
+    r1       += space() + format("↦") + pp_indent_expr(fmt, get_rhs());
     r += group(r1);
     return r;
 }
 
-congr_rule::congr_rule(name const & id, levels const & univ_metas, list<expr> const & metas,
-                       expr const & lhs, expr const & rhs, expr const & proof, list<expr> const & congr_hyps):
-    simp_rule_core(id, univ_metas, metas, lhs, rhs, proof),
+congr_rule::congr_rule(name const & id, levels const & umetas, std::vector<expr> const & emetas,
+                       std::vector<bool> const & instances, expr const & lhs, expr const & rhs, expr const & proof,
+                       list<expr> const & congr_hyps):
+    simp_rule_core(id, umetas, emetas, instances, lhs, rhs, proof),    
     m_congr_hyps(congr_hyps) {}
 
 bool operator==(congr_rule const & r1, congr_rule const & r2) {
@@ -51,15 +53,15 @@ bool operator==(congr_rule const & r1, congr_rule const & r2) {
 
 format congr_rule::pp(formatter const & fmt) const {
     format r;
-    r += format("#") + format(length(m_metas));
+    r += format("#") + format(get_num_emeta());
     format r1;
     for (expr const & h : m_congr_hyps) {
         r1 += space() + paren(fmt(mlocal_type(h)));
     }
     r += group(r1);
     r += space() + format(":") + space();
-    format r2 = paren(fmt(m_lhs));
-    r2       += space() + format("↦") + space() + paren(fmt(m_rhs));
+    format r2 = paren(fmt(get_lhs()));
+    r2       += space() + format("↦") + space() + paren(fmt(get_rhs()));
     r += group(r2);
     return r;
 }
@@ -253,33 +255,34 @@ format simp_rule_sets::pp(formatter const & fmt) const {
 
 static name * g_prefix = nullptr;
 
-simp_rule_sets add_core(type_checker & tc, simp_rule_sets const & s,
+simp_rule_sets add_core(tmp_type_context & tctx, simp_rule_sets const & s,
                         name const & id, levels const & univ_metas, expr const & e, expr const & h) {
-    list<expr_pair> ceqvs   = to_ceqvs(tc, e, h);
-    environment const & env = tc.env();
+    list<expr_pair> ceqvs   = to_ceqvs(tctx, e, h);
+    environment const & env = tctx.env();
     simp_rule_sets new_s = s;
     for (expr_pair const & p : ceqvs) {
-        expr new_e = p.first;
-        expr new_h = p.second;
-        bool is_perm       = is_permutation_ceqv(env, new_e);
-        buffer<expr> metas;
-        unsigned idx = 0;
-        while (is_pi(new_e)) {
-            expr mvar = mk_metavar(name(*g_prefix, idx), binding_domain(new_e));
-            idx++;
-            metas.push_back(mvar);
-            new_e = instantiate(binding_body(new_e), mvar);
+        expr rule = tctx.whnf(p.first);
+        expr proof = tctx.whnf(p.second);
+        bool is_perm = is_permutation_ceqv(env, rule);
+        std::vector<expr> emetas;
+        std::vector<bool> instances;        
+        while (is_pi(rule)) {
+            expr mvar = tctx.mk_mvar(binding_domain(rule));
+            emetas.push_back(mvar);
+            instances.push_back(binding_info(rule).is_inst_implicit());
+            rule = tctx.whnf(instantiate(binding_body(rule), mvar));
+            proof = mk_app(proof,mvar);
         }
         expr rel, lhs, rhs;
-        if (is_simp_relation(env, new_e, rel, lhs, rhs) && is_constant(rel)) {
-            new_s.insert(const_name(rel), simp_rule(id, univ_metas, to_list(metas), lhs, rhs, new_h, is_perm));
+        if (is_simp_relation(env, rule, rel, lhs, rhs) && is_constant(rel)) {
+            new_s.insert(const_name(rel), simp_rule(id, univ_metas, emetas, instances, lhs, rhs, proof, is_perm));
         }
     }
     return new_s;
 }
 
-simp_rule_sets add(type_checker & tc, simp_rule_sets const & s, name const & id, expr const & e, expr const & h) {
-    return add_core(tc, s, id, list<level>(), e, h);
+simp_rule_sets add(tmp_type_context & tctx, simp_rule_sets const & s, name const & id, expr const & e, expr const & h) {
+    return add_core(tctx, s, id, list<level>(), e, h);
 }
 
 simp_rule_sets join(simp_rule_sets const & s1, simp_rule_sets const & s2) {
@@ -293,17 +296,17 @@ simp_rule_sets join(simp_rule_sets const & s1, simp_rule_sets const & s2) {
 static name * g_class_name = nullptr;
 static std::string * g_key = nullptr;
 
-static simp_rule_sets add_core(type_checker & tc, simp_rule_sets const & s, name const & cname) {
-    declaration const & d = tc.env().get(cname);
+static simp_rule_sets add_core(tmp_type_context & tctx, simp_rule_sets const & s, name const & cname) {
+    declaration const & d = tctx.env().get(cname);
     buffer<level> us;
     unsigned num_univs = d.get_num_univ_params();
     for (unsigned i = 0; i < num_univs; i++) {
-        us.push_back(mk_meta_univ(name(*g_prefix, i)));
+        us.push_back(tctx.mk_uvar());
     }
     levels ls = to_list(us);
-    expr e    = instantiate_type_univ_params(d, ls);
+    expr e    = tctx.whnf(instantiate_type_univ_params(d, ls));
     expr h    = mk_constant(cname, ls);
-    return add_core(tc, s, cname, ls, e, h);
+    return add_core(tctx, s, cname, ls, e, h);
 }
 
 
@@ -350,30 +353,30 @@ static bool is_valid_congr_hyp_rhs(expr const & rhs, name_set & found_mvars) {
     return true;
 }
 
-void add_congr_core(environment const & env, simp_rule_sets & s, name const & n) {
-    declaration const & d = env.get(n);
-    type_checker tc(env);
+void add_congr_core(tmp_type_context & tctx, simp_rule_sets & s, name const & n) {
+    declaration const & d = tctx.env().get(n);
     buffer<level> us;
     unsigned num_univs = d.get_num_univ_params();
     for (unsigned i = 0; i < num_univs; i++) {
-        us.push_back(mk_meta_univ(name(*g_prefix, i)));
+        us.push_back(tctx.mk_uvar());
     }
     levels ls = to_list(us);
-    expr pr   = mk_constant(n, ls);
-    expr e    = instantiate_type_univ_params(d, ls);
-    buffer<bool> explicit_args;
-    buffer<expr> metas;
-    unsigned idx = 0;
-    while (is_pi(e)) {
-        expr mvar = mk_metavar(name(*g_prefix, idx), binding_domain(e));
-        idx++;
-        explicit_args.push_back(is_explicit(binding_info(e)));
-        metas.push_back(mvar);
-        e   = instantiate(binding_body(e), mvar);
-        pr  = mk_app(pr, mvar);
+    expr rule    = instantiate_type_univ_params(d, ls);
+    expr proof   = mk_constant(n, ls);
+
+    std::vector<expr> emetas;
+    std::vector<bool> instances, explicits;        
+    
+    while (is_pi(rule)) {
+        expr mvar = tctx.mk_mvar(binding_domain(rule));
+        emetas.push_back(mvar);
+        explicits.push_back(is_explicit(binding_info(rule)));
+        instances.push_back(binding_info(rule).is_inst_implicit());
+        rule = tctx.whnf(instantiate(binding_body(rule), mvar));
+        proof = mk_app(proof,mvar);
     }
     expr rel, lhs, rhs;
-    if (!is_simp_relation(env, e, rel, lhs, rhs) || !is_constant(rel)) {
+    if (!is_simp_relation(tctx.env(), rule, rel, lhs, rhs) || !is_constant(rel)) {
         throw exception(sstream() << "invalid congruence rule, '" << n
                         << "' resulting type is not of the form t ~ s, where '~' is a transitive and reflexive relation");
     }
@@ -414,19 +417,19 @@ void add_congr_core(environment const & env, simp_rule_sets & s, name const & n)
     }
 
     buffer<expr> congr_hyps;
-    lean_assert(metas.size() == explicit_args.size());
-    for (unsigned i = 0; i < metas.size(); i++) {
-        expr const & mvar = metas[i];
-        if (explicit_args[i] && !found_mvars.contains(mlocal_name(mvar))) {
+    lean_assert(emetas.size() == explicits.size());
+    for (unsigned i = 0; i < emetas.size(); i++) {
+        expr const & mvar = emetas[i];
+        if (explicits[i] && !found_mvars.contains(mlocal_name(mvar))) {
             buffer<expr> locals;
             expr type = mlocal_type(mvar);
             while (is_pi(type)) {
-                expr local = mk_local(tc.mk_fresh_name(), binding_domain(type));
+                expr local = tctx.mk_tmp_local(binding_domain(type));
                 locals.push_back(local);
                 type = instantiate(binding_body(type), local);
             }
             expr h_rel, h_lhs, h_rhs;
-            if (!is_simp_relation(env, type, h_rel, h_lhs, h_rhs) || !is_constant(h_rel))
+            if (!is_simp_relation(tctx.env(), type, h_rel, h_lhs, h_rhs) || !is_constant(h_rel))
                 continue;
             unsigned j = 0;
             for (expr const & local : locals) {
@@ -452,8 +455,8 @@ void add_congr_core(environment const & env, simp_rule_sets & s, name const & n)
             congr_hyps.push_back(mvar);
         }
     }
-    congr_rule rule(n, ls, to_list(metas), lhs, rhs, pr, to_list(congr_hyps));
-    s.insert(const_name(rel), rule);
+    
+    s.insert(const_name(rel), congr_rule(n, ls, emetas, instances, lhs, rhs, proof, to_list(congr_hyps)));
 }
 
 struct rrs_state {
@@ -461,14 +464,15 @@ struct rrs_state {
     name_set                 m_simp_names;
     name_set                 m_congr_names;
 
-    void add_simp(environment const & env, name const & cname) {
-        type_checker tc(env);
-        m_sets = add_core(tc, m_sets, cname);
+    void add_simp(environment const & env, io_state const & ios, name const & cname) {
+        tmp_type_context tctx{env,ios};
+        m_sets = add_core(tctx, m_sets, cname);
         m_simp_names.insert(cname);
     }
 
-    void add_congr(environment const & env, name const & n) {
-        add_congr_core(env, m_sets, n);
+    void add_congr(environment const & env, io_state const & ios, name const & n) {
+        tmp_type_context tctx{env,ios};        
+        add_congr_core(tctx,m_sets, n);
         m_congr_names.insert(n);
     }
 };
@@ -476,11 +480,11 @@ struct rrs_state {
 struct rrs_config {
     typedef pair<bool, name> entry;
     typedef rrs_state        state;
-    static void add_entry(environment const & env, io_state const &, state & s, entry const & e) {
+    static void add_entry(environment const & env, io_state const & ios, state & s, entry const & e) {
         if (e.first)
-            s.add_simp(env, e.second);
+            s.add_simp(env, ios, e.second);
         else
-            s.add_congr(env, e.second);
+            s.add_congr(env, ios, e.second);
     }
     static name const & get_class_name() {
         return *g_class_name;
@@ -522,13 +526,13 @@ simp_rule_sets get_simp_rule_sets(environment const & env) {
     return rrs_ext::get_state(env).m_sets;
 }
 
-simp_rule_sets get_simp_rule_sets(environment const & env, name const & ns) {
+simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios, name const & ns) {
     simp_rule_sets set;
     list<pair<bool, name>> const * cnames = rrs_ext::get_entries(env, ns);
     if (cnames) {
-        type_checker tc(env);
+        tmp_type_context tctx(env,ios);
         for (pair<bool, name> const & p : *cnames) {
-            set = add_core(tc, set, p.second);
+            set = add_core(tctx, set, p.second);
         }
     }
     return set;
diff --git a/src/library/simplifier/simp_rule_set.h b/src/library/simplifier/simp_rule_set.h
index 94f0e62b9..4d093ece6 100644
--- a/src/library/simplifier/simp_rule_set.h
+++ b/src/library/simplifier/simp_rule_set.h
@@ -5,27 +5,34 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "kernel/type_checker.h"
+#include "library/tmp_type_context.h"
 #include "library/head_map.h"
 #include "library/io_state_stream.h"
+#include <vector>
 
 namespace lean {
 class simp_rule_sets;
 
 class simp_rule_core {
 protected:
-    name           m_id;
-    levels         m_univ_metas;
-    list<expr>     m_metas;
-    expr           m_lhs;
-    expr           m_rhs;
-    expr           m_proof;
-    simp_rule_core(name const & id, levels const & univ_metas, list<expr> const & metas,
-                   expr const & lhs, expr const & rhs, expr const & proof);
+    name                m_id;
+    levels              m_umetas;
+    std::vector<expr>   m_emetas;
+    std::vector<bool>   m_instances;
+    
+    expr                m_lhs;
+    expr                m_rhs;
+    expr                m_proof;
+    simp_rule_core(name const & id, levels const & umetas, std::vector<expr> const & emetas,
+                   std::vector<bool> const & instances, expr const & lhs, expr const & rhs, expr const & proof);
 public:
     name const & get_id() const { return m_id; }
-    levels const & get_univ_metas() const { return m_univ_metas; }
-    list<expr> const & get_metas() const { return m_metas; }
+    unsigned get_num_umeta() const { return length(m_umetas); }
+    unsigned get_num_emeta() const { return m_emetas.size(); }
+
+    expr const & get_emeta(unsigned i) const { return m_emetas[i]; }
+    bool is_instance(unsigned i) const { return m_instances[i]; }
+    
     expr const & get_lhs() const { return m_lhs; }
     expr const & get_rhs() const { return m_rhs; }
     expr const & get_proof() const { return m_proof; }
@@ -33,9 +40,9 @@ public:
 
 class simp_rule : public simp_rule_core {
     bool           m_is_permutation;
-    simp_rule(name const & id, levels const & univ_metas, list<expr> const & metas,
-              expr const & lhs, expr const & rhs, expr const & proof, bool is_perm);
-    friend simp_rule_sets add_core(type_checker & tc, simp_rule_sets const & s, name const & id,
+    simp_rule(name const & id, levels const & umetas, std::vector<expr> const & emetas,
+              std::vector<bool> const & instances, expr const & lhs, expr const & rhs, expr const & proof, bool is_perm);
+    friend simp_rule_sets add_core(tmp_type_context & tctx, simp_rule_sets const & s, name const & id,
                                    levels const & univ_metas, expr const & e, expr const & h);
 public:
     friend bool operator==(simp_rule const & r1, simp_rule const & r2);
@@ -48,10 +55,11 @@ inline bool operator!=(simp_rule const & r1, simp_rule const & r2) { return !ope
 
 class congr_rule : public simp_rule_core {
     list<expr>  m_congr_hyps;
-    congr_rule(name const & id, levels const & univ_metas, list<expr> const & metas,
-               expr const & lhs, expr const & rhs, expr const & proof, list<expr> const & congr_hyps);
-    friend void add_congr_core(environment const & env, simp_rule_sets & s, name const & n);
-public:
+    congr_rule(name const & id, levels const & umetas, std::vector<expr> const & emetas,
+               std::vector<bool> const & instances, expr const & lhs, expr const & rhs, expr const & proof,
+               list<expr> const & congr_hyps);
+    friend void add_congr_core(tmp_type_context & tctx, simp_rule_sets & s, name const & n);
+public:    
     friend bool operator==(congr_rule const & r1, congr_rule const & r2);
     list<expr> const & get_congr_hyps() const { return m_congr_hyps; }
     format pp(formatter const & fmt) const;
@@ -108,7 +116,7 @@ public:
     format pp(formatter const & fmt) const;
 };
 
-simp_rule_sets add(type_checker & tc, simp_rule_sets const & s, name const & id, expr const & e, expr const & h);
+simp_rule_sets add(tmp_type_context & tctx, simp_rule_sets const & s, name const & id, expr const & e, expr const & h);
 simp_rule_sets join(simp_rule_sets const & s1, simp_rule_sets const & s2);
 
 environment add_simp_rule(environment const & env, name const & n, bool persistent = true);
@@ -121,7 +129,7 @@ bool is_congr_rule(environment const & env, name const & n);
 /** \brief Get current simplification rule sets */
 simp_rule_sets get_simp_rule_sets(environment const & env);
 /** \brief Get simplification rule sets in the given namespace. */
-simp_rule_sets get_simp_rule_sets(environment const & env, name const & ns);
+simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios, name const & ns);
 
 io_state_stream const & operator<<(io_state_stream const & out, simp_rule_sets const & s);
 
diff --git a/tests/lean/simplifier1.lean b/tests/lean/simplifier1.lean
new file mode 100644
index 000000000..3ce3521e0
--- /dev/null
+++ b/tests/lean/simplifier1.lean
@@ -0,0 +1,16 @@
+/- Basic rewriting with eq without congruence or conditionals -/
+universe l
+constant T : Type.{l}
+constants (x y z : T) (f g h : T → T) 
+constants (Hfxgy : f x = g y) (Hgyhz : g y = h z)
+
+#simplify eq 2 (f x) -- f x
+
+attribute Hfxgy [simp]
+attribute Hgyhz [simp]
+
+set_option simplify.exhaustive false
+#simplify eq 2 (f x) -- g y
+
+set_option simplify.exhaustive true
+#simplify eq 2 (f x) -- h z
diff --git a/tests/lean/simplifier1.lean.expected.out b/tests/lean/simplifier1.lean.expected.out
new file mode 100644
index 000000000..c260717a7
--- /dev/null
+++ b/tests/lean/simplifier1.lean.expected.out
@@ -0,0 +1,3 @@
+<refl>
+f x = g y
+f x = h z
diff --git a/tests/lean/simplifier2.lean b/tests/lean/simplifier2.lean
new file mode 100644
index 000000000..e30fddbcb
--- /dev/null
+++ b/tests/lean/simplifier2.lean
@@ -0,0 +1,15 @@
+/- Basic rewriting with eq and lambda without congruence or conditionals -/
+universe l
+constant T : Type.{l}
+constants (x y z : T) (f g h : T → T) 
+constants (Hfxgy : f x = g y) (Hgyhz : g y = h z)
+
+attribute Hfxgy [simp]
+attribute Hgyhz [simp]
+
+set_option simplify.exhaustive false
+#simplify eq 0 (λ a b c : bool, f x) -- λ (a b c : bool), g y
+
+set_option simplify.exhaustive true
+#simplify eq 0 (λ a b c : bool, f x) -- λ (a b c : bool), h z
+
diff --git a/tests/lean/simplifier2.lean.expected.out b/tests/lean/simplifier2.lean.expected.out
new file mode 100644
index 000000000..658a86497
--- /dev/null
+++ b/tests/lean/simplifier2.lean.expected.out
@@ -0,0 +1,2 @@
+λ (x x x : bool), g y
+λ (x x x : bool), h z
diff --git a/tests/lean/simplifier3.lean b/tests/lean/simplifier3.lean
new file mode 100644
index 000000000..2d1a07b0f
--- /dev/null
+++ b/tests/lean/simplifier3.lean
@@ -0,0 +1,36 @@
+/- Basic rewriting with eq and generic congruence, with no conditionals -/
+
+namespace test_congr
+
+universe l
+constant T : Type.{l}
+constants (x y z : T → T) (f g h : (T →  T) → (T →  T)) (a b c : T)
+constants (Hfxgy : f x = g y) (Hgyhz : g y = h z) (Hab : a = b) (Hbc : b = c)
+
+#simplify eq 2 (f x a) -- f x a
+
+attribute Hfxgy [simp]
+attribute Hgyhz [simp]
+attribute Hab [simp]
+attribute Hbc [simp]
+
+set_option simplify.exhaustive false
+#simplify eq 2 (f x a) -- g y b
+
+set_option simplify.exhaustive true
+#simplify eq 2 (f x a) -- h z c
+
+end test_congr
+
+namespace test_congr_fun
+
+universes l1 l2
+constants (T : Type.{l1}) (U : T → Type.{l2})
+constants (f g : Π (x:T), U x) (x y : T)
+constants (Hfg : f = g) (Hxy : x = y)
+
+attribute Hfg [simp]
+attribute Hxy [simp]
+
+#simplify eq 2 (f x)
+end test_congr_fun
diff --git a/tests/lean/simplifier3.lean.expected.out b/tests/lean/simplifier3.lean.expected.out
new file mode 100644
index 000000000..6b78a0be1
--- /dev/null
+++ b/tests/lean/simplifier3.lean.expected.out
@@ -0,0 +1,4 @@
+<refl>
+f x a = g y b
+f x a = h z c
+f x = g x
diff --git a/tests/lean/simplifier4.lean b/tests/lean/simplifier4.lean
new file mode 100644
index 000000000..d54c20456
--- /dev/null
+++ b/tests/lean/simplifier4.lean
@@ -0,0 +1,19 @@
+/- Basic rewriting with a custom relation without congruence or conditionals -/
+import logic.connectives data.nat
+
+universe l
+constant T : Type.{l}
+constants (x y z : T) (f g h : T → T) 
+constants (R : T → T → Prop) 
+constants (R_refl : ∀ x, R x x) (R_sym : ∀ x y, R x y →  R y x) (R_trans : ∀ x y z, R x y → R y z → R x z)
+constants (Hfxgy : R (f x) (g y)) (Hgyhz : R (g y) (h z))
+
+attribute R_refl [refl]
+attribute R_sym [symm]
+#simplify R 2 (f x) -- f x
+attribute R_trans [trans]
+#simplify R 2 (f x) -- f x
+attribute Hfxgy [simp]
+#simplify R 2 (f x) -- f x
+attribute Hgyhz [simp]
+#simplify R 2 (f x) -- f x
diff --git a/tests/lean/simplifier4.lean.expected.out b/tests/lean/simplifier4.lean.expected.out
new file mode 100644
index 000000000..fabfcc8ff
--- /dev/null
+++ b/tests/lean/simplifier4.lean.expected.out
@@ -0,0 +1,4 @@
+<refl>
+<refl>
+R (f x) (g y)
+R (f x) (h z)
diff --git a/tests/lean/simplifier5.lean b/tests/lean/simplifier5.lean
new file mode 100644
index 000000000..5816e541c
--- /dev/null
+++ b/tests/lean/simplifier5.lean
@@ -0,0 +1,13 @@
+/- Basic rewriting with iff with congr_iff -/
+import logic.connectives
+open nat
+#simplify iff 2 (@le nat nat_has_le 0 0) -- true
+#simplify iff 2 (@le nat nat_has_le 0 1) -- true
+#simplify iff 2 (@le nat nat_has_le 0 2) -- true
+#simplify iff 2 (@lt nat nat_has_lt 0 0) -- false
+#simplify iff 2 (@lt nat nat_has_lt 0 (succ 0)) -- true
+#simplify iff 2 (@lt nat nat_has_lt 1 (succ 1)) -- true
+#simplify iff 2 (@lt nat nat_has_lt 0 (succ (succ 0))) -- true
+#simplify iff 2 (@le nat nat_has_le 0 0 ↔ @le nat nat_has_le 0 0) -- true
+#simplify iff 2 (@le nat nat_has_le 0 0 ↔ @le nat nat_has_le 0 1) -- true
+#simplify iff 2 (@le nat nat_has_le 0 0 ↔ @lt nat nat_has_lt 0 0) -- false
diff --git a/tests/lean/simplifier5.lean.expected.out b/tests/lean/simplifier5.lean.expected.out
new file mode 100644
index 000000000..6ebd4546a
--- /dev/null
+++ b/tests/lean/simplifier5.lean.expected.out
@@ -0,0 +1,10 @@
+0 ≤ 0 ↔ true
+0 ≤ 1 ↔ true
+0 ≤ 2 ↔ true
+0 < 0 ↔ false
+0 < succ 0 ↔ true
+1 < succ 1 ↔ true
+0 < succ (succ 0) ↔ true
+0 ≤ 0 ↔ 0 ≤ 0 ↔ true
+0 ≤ 0 ↔ 0 ≤ 1 ↔ true
+0 ≤ 0 ↔ 0 < 0 ↔ false
diff --git a/tests/lean/simplifier6.lean b/tests/lean/simplifier6.lean
new file mode 100644
index 000000000..4a6c11161
--- /dev/null
+++ b/tests/lean/simplifier6.lean
@@ -0,0 +1,25 @@
+/- Basic pi congruence -/
+import logic.connectives logic.quantifiers
+
+namespace pi_congr1
+constants (p1 q1 p2 q2 p3 q3 : Prop) (H1 : p1 ↔ q1) (H2 : p2 ↔ q2) (H3 : p3 ↔ q3)
+local attribute H1 [simp]
+local attribute H2 [simp]
+local attribute H3 [simp]
+
+#simplify iff 1 p1
+#simplify iff 1 p1 →  p2
+#simplify iff 1 p1 →  p2 → p3
+
+end pi_congr1
+
+namespace pi_congr2
+universe l
+constants (T : Type.{l}) (P Q : T → Prop) (H : ∀ (x : T), P x ↔ Q x)
+local attribute H [simp]
+constant (x : T)
+
+#simplify iff 1 (∀ (x : T), P x)
+
+
+end pi_congr2
diff --git a/tests/lean/simplifier6.lean.expected.out b/tests/lean/simplifier6.lean.expected.out
new file mode 100644
index 000000000..a366c0040
--- /dev/null
+++ b/tests/lean/simplifier6.lean.expected.out
@@ -0,0 +1,4 @@
+H1
+congr_imp H1 H2
+congr_imp H1 (congr_imp H2 H3)
+congr_forall (λ (x : T), H x)
diff --git a/tests/lean/simplifier7.lean b/tests/lean/simplifier7.lean
new file mode 100644
index 000000000..ef94541b0
--- /dev/null
+++ b/tests/lean/simplifier7.lean
@@ -0,0 +1,15 @@
+-- Simplifying the operator with a user-defined congruence
+import logic.connectives
+
+constants (P1 Q1 P2 Q2 P3 Q3 : Prop) (H1 : P1 ↔ Q1) (H2 : P2 ↔ Q2) (H3 : P3 ↔ Q3)
+constants (f g : Prop → Prop → Prop)
+constants (Hf : and = f) (Hg : f = g)
+
+attribute H1 [simp]
+attribute H2 [simp]
+attribute H3 [simp]
+attribute Hf [simp]
+attribute Hg [simp]
+
+#simplify iff 2 (and P1 (and P2 P3))
+#simplify iff 2 (and P1 (iff P2 P3))
diff --git a/tests/lean/simplifier7.lean.expected.out b/tests/lean/simplifier7.lean.expected.out
new file mode 100644
index 000000000..454f9a605
--- /dev/null
+++ b/tests/lean/simplifier7.lean.expected.out
@@ -0,0 +1,2 @@
+P1 ∧ P2 ∧ P3 ↔ g Q1 (g Q2 Q3)
+P1 ∧ (P2 ↔ P3) ↔ g Q1 (Q2 ↔ Q3)
diff --git a/tests/lean/simplifier8.lean b/tests/lean/simplifier8.lean
new file mode 100644
index 000000000..469fe1884
--- /dev/null
+++ b/tests/lean/simplifier8.lean
@@ -0,0 +1,13 @@
+-- deeper congruence
+
+universe l
+constants (T : Type.{l}) (x1 x2 x3 x4 x5 x6 : T) (f : T → T → T)
+constants (f_comm : ∀ x y, f x y = f y x)
+          (f_l : ∀ x y z, f (f x y) z = f x (f y z))
+          (f_r : ∀ x y z, f x (f y z) = f y (f x z))
+
+attribute f_comm [simp]
+attribute f_l [simp]
+attribute f_r [simp]
+
+#simplify eq 0 (f (f x2 x4) (f x5 (f x3 (f x1 x6))))
diff --git a/tests/lean/simplifier8.lean.expected.out b/tests/lean/simplifier8.lean.expected.out
new file mode 100644
index 000000000..37ea1ee9a
--- /dev/null
+++ b/tests/lean/simplifier8.lean.expected.out
@@ -0,0 +1 @@
+f x1 (f x2 (f x3 (f x4 (f x5 x6))))