feat(library/blast/blast): use defeq_simplifier to normalize

library/init/logic.lean

@@ -53,6 +53,8 @@ false.rec c H
 notation a = b := eq a b
 definition rfl {A : Type} {a : A} : a = a := eq.refl a
 
+definition id.def [defeq] {A : Type} (a : A) : id a = a := rfl
+
 -- proof irrelevance is built in
 theorem proof_irrel {a : Prop} (H₁ H₂ : a) : H₁ = H₂ :=
 rfl
@@ -142,6 +144,7 @@ rfl
 /- ne -/
 
 definition ne [reducible] {A : Type} (a b : A) := ¬(a = b)
+definition ne.def [defeq] {A : Type} (a b : A) : ne a b = ¬ (a = b) := rfl
 notation a ≠ b := ne a b
 
 namespace ne

src/frontends/lean/builtin_cmds.cpp

@@ -574,8 +574,8 @@ static environment defeq_simplify_cmd(parser & p) {
     std::tie(e, ls) = parse_local_expr(p);
 
     auto tc = mk_type_checker(p.env());
-
+    default_tmp_type_context_pool pool(p.env(), p.get_options());
-    expr e_simp = defeq_simplify(env, p.get_options(), sls, e);
+    expr e_simp = defeq_simplify(pool, p.get_options(), sls, e);
     if (!tc->is_def_eq(e, e_simp).first) {
         throw parser_error("defeq_simplify result not definitionally equal to input expression", pos);
     }

src/library/blast/blast.cpp

@@ -10,9 +10,13 @@ Author: Leonardo de Moura
 #include "kernel/for_each_fn.h"
 #include "kernel/find_fn.h"
 #include "kernel/replace_fn.h"
+#include "kernel/instantiate.h"
+#include "kernel/abstract.h"
 #include "kernel/type_checker.h"
 #include "library/replace_visitor.h"
 #include "library/util.h"
+#include "library/defeq_simp_lemmas.h"
+#include "library/defeq_simplifier.h"
 #include "library/trace.h"
 #include "library/reducible.h"
 #include "library/class.h"
@@ -21,6 +25,7 @@ Author: Leonardo de Moura
 #include "library/relation_manager.h"
 #include "library/congr_lemma_manager.h"
 #include "library/abstract_expr_manager.h"
+#include "library/proof_irrel_expr_manager.h"
 #include "library/light_lt_manager.h"
 #include "library/projection.h"
 #include "library/scoped_ext.h"
@@ -67,6 +72,15 @@ struct imp_extension_entry {
         m_ext_state(ext_state), m_ext_id(ext_id), m_ext_of_ext_state(ext_of_ext_state) {}
 };
 
+unsigned proof_irrel_hash(expr const & e);
+bool proof_irrel_is_equal(expr const & e1, expr const & e2);
+
+class tmp_tctx_pool : public tmp_type_context_pool {
+public:
+    virtual tmp_type_context * mk_tmp_type_context() override;
+    virtual void recycle_tmp_type_context(tmp_type_context * tmp_tctx) override;
+};
+
 class blastenv {
     friend class scope_assignment;
     friend class scope_unfold_macro_pred;
@@ -103,6 +117,7 @@ class blastenv {
     fun_info_manager           m_fun_info_manager;
     congr_lemma_manager        m_congr_lemma_manager;
     abstract_expr_manager      m_abstract_expr_manager;
+    proof_irrel_expr_manager   m_proof_irrel_expr_manager;
     light_lt_manager           m_light_lt_manager;
     imp_extension_entries      m_imp_extension_entries;
     relation_info_getter       m_rel_getter;
@@ -517,9 +532,35 @@ class blastenv {
     }
 
     tctx                       m_tctx;
+
+    /* Normalizing instances */
     normalizer                 m_normalizer;
+
+    struct inst_key {
+        expr              m_e;
+        unsigned          m_hash;
+
+        inst_key(expr const & e):
+            m_e(e), m_hash(blast::proof_irrel_hash(e)) { }
+    };
+
+    struct inst_key_hash_fn {
+        unsigned operator()(inst_key const & k) const { return k.m_hash; }
+    };
+
+    struct inst_key_eq_fn {
+        bool operator()(inst_key const & k1, inst_key const & k2) const {
+            return blast::proof_irrel_is_equal(k1.m_e, k2.m_e);
+        }
+    };
+
+    typedef std::unordered_map<inst_key, expr, inst_key_hash_fn, inst_key_eq_fn> inst_cache;
+    inst_cache      m_inst_nf_to_cf;
+    expr_map<expr>  m_inst_to_nf;
+
     expr_map<expr>  m_norm_cache; // normalization cache
 
+
     void save_initial_context() {
         hypothesis_idx_buffer hidxs;
         m_curr_state.get_sorted_hypotheses(hidxs);
@@ -528,6 +569,8 @@ class blastenv {
             ctx.push_back(mk_href(hidx));
         }
         m_initial_context = to_list(ctx);
+        for (auto ctx : m_tmp_ctx_pool) delete ctx;
+        m_tmp_ctx_pool.clear();
     }
 
     name_map<level> mk_uref2uvar() const {
@@ -636,6 +679,7 @@ public:
         m_fun_info_manager(*m_tmp_ctx),
         m_congr_lemma_manager(m_app_builder, m_fun_info_manager),
         m_abstract_expr_manager(m_congr_lemma_manager),
+        m_proof_irrel_expr_manager(m_fun_info_manager),
         m_light_lt_manager(env),
         m_rel_getter(mk_relation_info_getter(env)),
         m_refl_getter(mk_refl_info_getter(env)),
@@ -709,6 +753,10 @@ public:
         return m_projection_info.find(n);
     }
 
+    unfold_macro_pred get_unfold_macro_pred() const {
+        return m_unfold_macro_pred;
+    }
+
     expr mk_fresh_local(expr const & type, binder_info const & bi) {
         return m_tctx.mk_tmp_local(type, bi);
     }
@@ -793,6 +841,10 @@ public:
         return m_abstract_expr_manager.hash(e);
     }
 
+    unsigned proof_irrel_hash(expr const & e) {
+        return m_proof_irrel_expr_manager.hash(e);
+    }
+
     void init_imp_extension_entries() {
         for (auto & p : get_imp_extension_manager().get_entries()) {
             branch_extension & b_ext = curr_state().get_extension(p.second);
@@ -849,6 +901,10 @@ public:
         return m_abstract_expr_manager.is_equal(e1, e2);
     }
 
+    bool proof_irrel_is_equal(expr const & e1, expr const & e2) {
+        return m_proof_irrel_expr_manager.is_equal(e1, e2);
+    }
+
     bool is_light_lt(expr const & e1, expr const & e2) {
         return m_light_lt_manager.is_lt(e1, e2);
     }
@@ -870,11 +926,74 @@ public:
         return m_tctx;
     }
 
+    expr normalize_instance(expr const & inst) {
+        auto it1 = m_inst_to_nf.find(inst);
+        expr inst_nf;
+        if (it1 != m_inst_to_nf.end()) {
+            inst_nf = it1->second;
+        } else {
+            inst_nf = m_normalizer(inst);
+            m_inst_to_nf.insert(mk_pair(inst, inst_nf));
+        }
+
+        auto it2 = m_inst_nf_to_cf.find(inst_nf);
+        expr inst_cf;
+        if (it2 != m_inst_nf_to_cf.end()) {
+            inst_cf = it2->second;
+        } else {
+            inst_cf = inst;
+            m_inst_nf_to_cf.insert(mk_pair(inst_nf, inst_cf));
+        }
+        lean_trace(name({"debug", "blast", "inst_cache"}),
+                   tout() << "\n" << inst << "\n==>\n" << inst_nf << "\n==>\n" << inst_cf << "\n";);
+        return inst_cf;
+    }
+
+    expr normalize_instances(expr const & e) {
+        expr b, l, d;
+        switch (e.kind()) {
+        case expr_kind::Constant:
+        case expr_kind::Local:
+        case expr_kind::Meta:
+        case expr_kind::Sort:
+        case expr_kind::Var:
+        case expr_kind::Macro:
+            return e;
+        case expr_kind::Lambda:
+        case expr_kind::Pi:
+            d = normalize_instances(binding_domain(e));
+            l = mk_fresh_local(d, binding_info(e));
+            b = abstract(normalize_instances(instantiate(binding_body(e), l)), l);
+            return update_binding(e, d, b);
+        case expr_kind::App:
+            buffer<expr> args;
+            expr const & f     = get_app_args(e, args);
+            unsigned prefix_sz = get_specialization_prefix_size(f, args.size());
+            expr new_f = e;
+            unsigned rest_sz   = args.size() - prefix_sz;
+            for (unsigned i = 0; i < rest_sz; i++)
+                new_f = app_fn(new_f);
+            fun_info info = get_fun_info(new_f, rest_sz);
+            lean_assert(length(info.get_params_info()) == rest_sz);
+            unsigned i = prefix_sz;
+            for_each(info.get_params_info(), [&](param_info const & p_info) {
+                    if (p_info.is_inst_implicit()) {
+                        args[i] = normalize_instance(args[i]);
+                    } else {
+                        args[i] = normalize_instances(args[i]);
+                    }
+                    i++;
+                });
+            return mk_app(f, args);
+        }
+        lean_unreachable();
+    }
+
     expr normalize(expr const & e) {
         auto it = m_norm_cache.find(e);
-        if (it != m_norm_cache.end())
+        if (it != m_norm_cache.end()) return it->second;
-            return it->second;
+        tmp_tctx_pool pool;
-        expr r = m_normalizer(e);
+        expr r = normalize_instances(defeq_simplify(pool, m_ios.get_options(), get_defeq_simp_lemmas(m_env), e));
         m_norm_cache.insert(mk_pair(e, r));
         return r;
     }
@@ -1114,6 +1233,11 @@ optional<expr> mk_subsingleton_instance(expr const & type) {
     return g_blastenv->mk_subsingleton_instance(type);
 }
 
+unfold_macro_pred get_unfold_macro_pred() {
+    lean_assert(g_blastenv);
+    return g_blastenv->get_unfold_macro_pred();
+}
+
 expr mk_fresh_local(expr const & type, binder_info const & bi) {
     lean_assert(g_blastenv);
     return g_blastenv->mk_fresh_local(type, bi);
@@ -1194,6 +1318,11 @@ unsigned abstract_hash(expr const & e) {
     return g_blastenv->abstract_hash(e);
 }
 
+unsigned proof_irrel_hash(expr const & e) {
+    lean_assert(g_blastenv);
+    return g_blastenv->proof_irrel_hash(e);
+}
+
 unsigned register_imp_extension(std::function<imp_extension_state*()> & ext_state_maker) {
     return get_imp_extension_manager().register_imp_extension(ext_state_maker);
 }
@@ -1208,6 +1337,11 @@ bool abstract_is_equal(expr const & e1, expr const & e2) {
     return g_blastenv->abstract_is_equal(e1, e2);
 }
 
+bool proof_irrel_is_equal(expr const & e1, expr const & e2) {
+    lean_assert(g_blastenv);
+    return g_blastenv->proof_irrel_is_equal(e1, e2);
+}
+
 bool is_light_lt(expr const & e1, expr const & e2) {
     lean_assert(g_blastenv);
     return g_blastenv->is_light_lt(e1, e2);
@@ -1313,6 +1447,10 @@ public:
     tmp_tctx(environment const & env, options const & o):
         tmp_type_context(env, o) {}
 
+    virtual bool should_unfold_macro(expr const & e) const override {
+        return get_unfold_macro_pred()(e);
+    }
+
     /** \brief Return the type of a local constant (local or not).
         \remark This method allows the customer to store the type of local constants
         in a different place. */
@@ -1358,6 +1496,16 @@ tmp_type_context * blastenv::mk_tmp_type_context() {
     return r;
 }
 
+tmp_type_context * tmp_tctx_pool::mk_tmp_type_context() {
+    lean_assert(g_blastenv);
+    return g_blastenv->mk_tmp_type_context();
+}
+
+void tmp_tctx_pool::recycle_tmp_type_context(tmp_type_context * tmp_tctx) {
+    lean_assert(g_blastenv);
+    g_blastenv->recycle_tmp_type_context(tmp_tctx);
+}
+
 blast_tmp_type_context::blast_tmp_type_context(unsigned num_umeta, unsigned num_emeta) {
     lean_assert(g_blastenv);
     m_ctx = g_blastenv->mk_tmp_type_context();
@@ -1400,6 +1548,7 @@ void initialize_blast() {
     register_trace_class(name{"blast", "search"});
     register_trace_class(name{"blast", "deadend"});
     register_trace_class(name{"debug", "blast"});
+    register_trace_class(name{"debug", "blast", "inst_cache"});
 
     register_trace_class_alias("app_builder", name({"blast", "event"}));
     register_trace_class_alias(name({"simplifier", "failure"}), name({"blast", "event"}));

src/library/blast/blast.h

@@ -168,10 +168,14 @@ fun_info get_specialized_fun_info(expr const & a);
 /** \brief Return the given function specialization prefix size. */
 unsigned get_specialization_prefix_size(expr const & fn, unsigned nargs);
 
-/** \brief Hash and equality test for abstract expressions */
+/** \brief Hash and equality test that ignore subsingleton arguments */
 unsigned abstract_hash(expr const & e);
 bool abstract_is_equal(expr const & e1, expr const & e2);
 
+/** \brief Hash and equality test that ignore arguments that are proofs */
+unsigned proof_irrel_hash(expr const & e);
+bool proof_irrel_is_equal(expr const & e1, expr const & e2);
+
 /** \brief Order on expressions that supports the "light" annotation */
 bool is_light_lt(expr const & e1, expr const & e2);
 

src/library/defeq_simp_lemmas.cpp

@@ -129,10 +129,11 @@ defeq_simp_lemmas get_defeq_simp_lemmas(environment const & env) {
 }
 
 defeq_simp_lemmas get_defeq_simp_lemmas(environment const & env, name const & ns) {
-    list<defeq_simp_lemmas_entry> const * entries = defeq_simp_lemmas_ext::get_entries(env, ns);
+    list<defeq_simp_lemmas_entry> const * _entries = defeq_simp_lemmas_ext::get_entries(env, ns);
     defeq_simp_lemmas_state s;
-    if (entries) {
+    if (_entries) {
-        for (auto const & e : *entries) {
+        list<defeq_simp_lemmas_entry> entries = reverse(*_entries);
+        for (auto const & e : entries) {
             tmp_type_context tctx(env, get_dummy_ios().get_options());
             s.register_defeq_simp_lemma(tctx, e.m_decl_name, e.m_priority);
         }

src/library/defeq_simplifier.cpp

@@ -15,10 +15,10 @@ Author: Daniel Selsam
 #include "library/normalize.h"
 
 #ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS
-#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS 1000
+#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS 5000
 #endif
 #ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_REWRITE_ROUNDS
-#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_REWRITE_ROUNDS 1000
+#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_REWRITE_ROUNDS 5000
 #endif
 #ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_TOP_DOWN
 #define LEAN_DEFAULT_DEFEQ_SIMPLIFY_TOP_DOWN false
@@ -29,9 +29,6 @@ Author: Daniel Selsam
 #ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_MEMOIZE
 #define LEAN_DEFAULT_DEFEQ_SIMPLIFY_MEMOIZE true
 #endif
-#ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXPAND_MACROS
-#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXPAND_MACROS false
-#endif
 
 namespace lean {
 
@@ -42,7 +39,6 @@ static name * g_simplify_max_rewrite_rounds  = nullptr;
 static name * g_simplify_top_down            = nullptr;
 static name * g_simplify_exhaustive          = nullptr;
 static name * g_simplify_memoize             = nullptr;
-static name * g_simplify_expand_macros       = nullptr;
 
 static unsigned get_simplify_max_simp_rounds(options const & o) {
     return o.get_unsigned(*g_simplify_max_simp_rounds, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS);
@@ -64,29 +60,23 @@ static bool get_simplify_memoize(options const & o) {
     return o.get_bool(*g_simplify_memoize, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MEMOIZE);
 }
 
-static bool get_simplify_expand_macros(options const & o) {
-    return o.get_bool(*g_simplify_expand_macros, LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXPAND_MACROS);
-}
-
 /* Main simplifier class */
 
 class defeq_simplify_fn {
-    tmp_type_context                  m_tmp_tctx;
+    tmp_type_context_pool           & m_tmp_tctx_pool;
-    normalizer                        m_normalizer;
+    tmp_type_context                * m_tmp_tctx;
+
     defeq_simp_lemmas                 m_simp_lemmas;
 
     unsigned                          m_num_simp_rounds{0};
     unsigned                          m_num_rewrite_rounds{0};
 
-    options const &                   m_options;
-
     /* Options */
     unsigned                          m_max_simp_rounds;
     unsigned                          m_max_rewrite_rounds;
     bool                              m_top_down;
     bool                              m_exhaustive;
     bool                              m_memoize;
-    bool                              m_expand_macros;
 
     /* Cache */
     expr_struct_map<expr>             m_cache;
@@ -131,9 +121,7 @@ class defeq_simplify_fn {
             case expr_kind::Var:
                 lean_unreachable();
             case expr_kind::Macro:
-                if (m_expand_macros) {
+                e = defeq_simplify_macro(e);
-                    if (auto m = m_tmp_tctx.expand_macro(e)) e = defeq_simplify(whnf_eta(*m));
-                }
                 break;
             case expr_kind::Lambda:
                 e = try_eta(defeq_simplify_binding(e));
@@ -152,12 +140,20 @@ class defeq_simplify_fn {
             if (!m_exhaustive || e == e_start) break;
         }
         if (m_memoize) cache_save(_e, e);
+        lean_assert(m_tmp_tctx->is_def_eq(_e, e));
         return e;
     }
 
+    expr defeq_simplify_macro(expr const & e) {
+        buffer<expr> new_args;
+        for (unsigned i = 0; i < macro_num_args(e); i++)
+            new_args.push_back(defeq_simplify(macro_arg(e, i)));
+        return update_macro(e, new_args.size(), new_args.data());
+    }
+
     expr defeq_simplify_binding(expr const & e) {
         expr d = defeq_simplify(binding_domain(e));
-        expr l = m_tmp_tctx.mk_tmp_local(binding_name(e), d, binding_info(e));
+        expr l = m_tmp_tctx->mk_tmp_local(binding_name(e), d, binding_info(e));
         expr b = abstract(defeq_simplify(instantiate(binding_body(e), l)), l);
         return update_binding(e, d, b);
     }
@@ -168,7 +164,7 @@ class defeq_simplify_fn {
         expr f = get_app_rev_args(e, args);
         for (expr & a : args) {
             expr new_a = a;
-            if (!m_tmp_tctx.is_prop(m_tmp_tctx.infer(a)))
+            if (!m_tmp_tctx->is_prop(m_tmp_tctx->infer(a)))
                 new_a = defeq_simplify(a);
             if (new_a != a)
                 modified = true;
@@ -176,15 +172,18 @@ class defeq_simplify_fn {
         }
 
         if (is_constant(f)) {
-            if (auto idx = inductive::get_elim_major_idx(m_tmp_tctx.env(), const_name(f))) {
+            if (auto idx = inductive::get_elim_major_idx(m_tmp_tctx->env(), const_name(f))) {
-                if (auto r = m_normalizer.unfold_recursor_major(f, *idx, args))
+                if (auto r = normalizer(*m_tmp_tctx).unfold_recursor_major(f, *idx, args))
                     return *r;
             }
         }
+
         if (!modified)
             return e;
+
         expr r = mk_rev_app(f, args);
-        if (is_constant(f) && m_tmp_tctx.env().is_recursor(const_name(f))) {
+
+        if (is_constant(f) && m_tmp_tctx->env().is_recursor(const_name(f))) {
             return defeq_simplify(r);
         } else {
             return r;
@@ -214,31 +213,32 @@ class defeq_simplify_fn {
     }
 
     expr rewrite(expr const & e, defeq_simp_lemma const & sl) {
-        tmp_type_context tmp_tctx(m_tmp_tctx.env(), m_options);
+        tmp_type_context * tmp_tctx = m_tmp_tctx_pool.mk_tmp_type_context();
-        tmp_tctx.clear();
+        tmp_tctx->clear();
-        tmp_tctx.set_next_uvar_idx(sl.get_num_umeta());
+        tmp_tctx->set_next_uvar_idx(sl.get_num_umeta());
-        tmp_tctx.set_next_mvar_idx(sl.get_num_emeta());
+        tmp_tctx->set_next_mvar_idx(sl.get_num_emeta());
 
-        if (!tmp_tctx.is_def_eq(e, sl.get_lhs())) return e;
+        if (!tmp_tctx->is_def_eq(e, sl.get_lhs())) return e;
 
         lean_trace(name({"defeq_simplifier", "rewrite"}),
-                   expr new_lhs = tmp_tctx.instantiate_uvars_mvars(sl.get_lhs());
+                   expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sl.get_lhs());
-                   expr new_rhs = tmp_tctx.instantiate_uvars_mvars(sl.get_rhs());
+                   expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sl.get_rhs());
                    tout() << "(" << sl.get_id() << ") "
                    << "[" << new_lhs << " --> " << new_rhs << "]\n";);
 
         if (!instantiate_emetas(tmp_tctx, sl.get_emetas(), sl.get_instances())) return e;
 
         for (unsigned i = 0; i < sl.get_num_umeta(); i++) {
-            if (!tmp_tctx.is_uvar_assigned(i)) return e;
+            if (!tmp_tctx->is_uvar_assigned(i)) return e;
         }
 
-        expr new_rhs = tmp_tctx.instantiate_uvars_mvars(sl.get_rhs());
+        expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sl.get_rhs());
+        m_tmp_tctx_pool.recycle_tmp_type_context(tmp_tctx);
         return new_rhs;
     }
 
 
-    bool instantiate_emetas(tmp_type_context & tmp_tctx, list<expr> const & _emetas, list<bool> const & _instances) {
+    bool instantiate_emetas(tmp_type_context * tmp_tctx, list<expr> const & _emetas, list<bool> const & _instances) {
         buffer<expr> emetas;
         buffer<bool> instances;
         to_buffer(_emetas, emetas);
@@ -248,17 +248,17 @@ class defeq_simplify_fn {
         for (unsigned i = 0; i < emetas.size(); ++i) {
             expr m = emetas[i];
             unsigned mvar_idx = emetas.size() - 1 - i;
-            expr m_type = tmp_tctx.instantiate_uvars_mvars(tmp_tctx.infer(m));
+            expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m));
             lean_assert(!has_metavar(m_type));
-            if (tmp_tctx.is_mvar_assigned(mvar_idx)) continue;
+            if (tmp_tctx->is_mvar_assigned(mvar_idx)) continue;
             if (instances[i]) {
-                if (auto v = tmp_tctx.mk_class_instance(m_type)) {
+                if (auto v = tmp_tctx->mk_class_instance(m_type)) {
-                    if (!tmp_tctx.assign(m, *v)) {
+                    if (!tmp_tctx->assign(m, *v)) {
                         lean_trace(name({"defeq_simplifier", "failure"}),
                                    tout() << "unable to assign instance for: " << m_type << "\n";);
                         return false;
                     } else {
-                        lean_assert(tmp_tctx.is_mvar_assigned(mvar_idx));
+                        lean_assert(tmp_tctx->is_mvar_assigned(mvar_idx));
                         continue;
                     }
                 } else {
@@ -276,22 +276,24 @@ class defeq_simplify_fn {
     }
 
     expr whnf_eta(expr const & e) {
-        return try_eta(m_tmp_tctx.whnf(e));
+        return try_eta(m_tmp_tctx->whnf(e));
     }
 
 public:
-    defeq_simplify_fn(environment const & env, options const & o, defeq_simp_lemmas const & simp_lemmas):
+    defeq_simplify_fn(tmp_type_context_pool & tmp_tctx_pool, options const & o, defeq_simp_lemmas const & simp_lemmas):
-        m_tmp_tctx(env, o),
+        m_tmp_tctx_pool(tmp_tctx_pool),
-        m_normalizer(m_tmp_tctx),
+        m_tmp_tctx(m_tmp_tctx_pool.mk_tmp_type_context()),
         m_simp_lemmas(simp_lemmas),
-        m_options(o),
         m_max_simp_rounds(get_simplify_max_simp_rounds(o)),
         m_max_rewrite_rounds(get_simplify_max_rewrite_rounds(o)),
         m_top_down(get_simplify_top_down(o)),
         m_exhaustive(get_simplify_exhaustive(o)),
-        m_memoize(get_simplify_memoize(o)),
+        m_memoize(get_simplify_memoize(o))
-        m_expand_macros(get_simplify_expand_macros(o)) {}
+        { }
 
+    ~defeq_simplify_fn() {
+        m_tmp_tctx_pool.recycle_tmp_type_context(m_tmp_tctx);
+    }
     expr operator()(expr const & e)  { return defeq_simplify(e); }
 };
 
@@ -307,7 +309,6 @@ void initialize_defeq_simplifier() {
     g_simplify_top_down           = new name{"defeq_simplify", "top_down"};
     g_simplify_exhaustive         = new name{"defeq_simplify", "exhaustive"};
     g_simplify_memoize            = new name{"defeq_simplify", "memoize"};
-    g_simplify_expand_macros      = new name{"defeq_simplify", "expand_macros"};
 
     register_unsigned_option(*g_simplify_max_simp_rounds, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS,
                              "(defeq_simplify) max allowed simplification rounds");
@@ -319,12 +320,9 @@ void initialize_defeq_simplifier() {
                          "(defeq_simplify) simplify exhaustively");
     register_bool_option(*g_simplify_memoize, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MEMOIZE,
                          "(defeq_simplify) memoize simplifications");
-    register_bool_option(*g_simplify_expand_macros, LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXPAND_MACROS,
-                         "(defeq_simplify) expand macros");
 }
 
 void finalize_defeq_simplifier() {
-    delete g_simplify_expand_macros;
     delete g_simplify_memoize;
     delete g_simplify_exhaustive;
     delete g_simplify_top_down;
@@ -333,9 +331,8 @@ void finalize_defeq_simplifier() {
 }
 
 /* Entry point */
-expr defeq_simplify(environment const & env, options const & o, defeq_simp_lemmas const & simp_lemmas, expr const & e) {
+expr defeq_simplify(tmp_type_context_pool & tmp_tctx_pool, options const & o, defeq_simp_lemmas const & simp_lemmas, expr const & e) {
-    return defeq_simplify_fn(env, o, simp_lemmas)(e);
+    return defeq_simplify_fn(tmp_tctx_pool, o, simp_lemmas)(e);
 }
 
-
 }

src/library/defeq_simplifier.h

@@ -5,11 +5,12 @@ Author: Daniel Selsam
 */
 #pragma once
 #include "kernel/expr.h"
+#include "library/tmp_type_context.h"
 #include "library/defeq_simp_lemmas.h"
 
 namespace lean {
 
-expr defeq_simplify(environment const & env, options const & o, defeq_simp_lemmas const & simp_lemmas, expr const & e);
+expr defeq_simplify(tmp_type_context_pool & tmp_tctx_pool, options const & o, defeq_simp_lemmas const & simp_lemmas, expr const & e);
 
 void initialize_defeq_simplifier();
 void finalize_defeq_simplifier();

src/library/tmp_type_context.h

@@ -90,4 +90,24 @@ public:
         return static_cast<bool>(m_eassignment[idx]);
     }
 };
+
+class tmp_type_context_pool {
+public:
+    virtual tmp_type_context * mk_tmp_type_context() =0;
+    virtual void recycle_tmp_type_context(tmp_type_context * tmp_tctx) =0;
+
+    virtual ~tmp_type_context_pool() {}
+};
+
+class default_tmp_type_context_pool : public tmp_type_context_pool {
+    environment m_env;
+    options     m_options;
+public:
+    default_tmp_type_context_pool(environment const & env, options const & o):
+        m_env(env), m_options(o) {}
+
+    virtual tmp_type_context * mk_tmp_type_context() override { return new tmp_type_context(m_env, m_options); }
+    virtual void recycle_tmp_type_context(tmp_type_context * tmp_tctx) override { delete tmp_tctx; }
+};
+
 }

src/library/type_context.cpp

@@ -170,7 +170,7 @@ optional<declaration> type_context::is_transparent(name const & n) {
 
 optional<expr> type_context::expand_macro(expr const & m) {
     lean_assert(is_macro(m));
-    if (should_unfold_macro(m))
+    if (m_in_is_def_eq || should_unfold_macro(m))
         return macro_def(m).expand(m, *m_ext_ctx);
     else
         return none_expr();
@@ -1064,6 +1064,7 @@ bool type_context::process_postponed(unsigned old_sz) {
 
 bool type_context::is_def_eq(expr const & e1, expr const & e2) {
     scope s(*this);
+    flet<bool> in_is_def_eq(m_in_is_def_eq, true);
     unsigned psz = m_postponed.size();
     if (!is_def_eq_core(e1, e2)) {
         return false;

src/library/type_context.h

@@ -116,6 +116,7 @@ class type_context : public abstract_type_context {
     // postponed universe constraints
     std::vector<pair<level, level>> m_postponed;
     name_map<projection_info>       m_proj_info;
+    bool                            m_in_is_def_eq{false};
 
     // Internal (configuration) options for customers
 

tests/lean/defeq_simp_lemmas1.lean

@@ -1,3 +1,4 @@
+namespace foo
 universe l
 constants (A : Type.{l})
 
@@ -12,4 +13,5 @@ definition g.def [defeq] (x y : A) : g x y = h y := rfl
 definition f.def [defeq] (x y z : A) : f x y z = g (g x y) z := rfl
 definition d.def [defeq] (x y z w : A) : d x y z w = f (f x y z) (f y z w) (f x w z) := rfl
 
-print [defeq]
+print [defeq] foo
+end foo

tests/lean/defeq_simp_lemmas1.lean.expected.out

@@ -1,5 +1,5 @@
-defeq simp lemmas:
+defeq simp lemmas at namespace 'foo':
-#2, g ?M_1 ?M_2 ↦ h ?M_2
 #4, d ?M_1 ?M_2 ?M_3 ?M_4 ↦ f (f ?M_1 ?M_2 ?M_3) (f ?M_2 ?M_3 ?M_4) (f ?M_1 ?M_4 ?M_3)
 #3, f ?M_1 ?M_2 ?M_3 ↦ g (g ?M_1 ?M_2) ?M_3
+#2, g ?M_1 ?M_2 ↦ h ?M_2
 #1, h ?M_1 ↦ q ?M_1

tests/lean/defeq_simp_lemmas2.lean

@@ -1,3 +1,4 @@
+namespace foo
 universe l
 constants (A : Type.{l})
 
@@ -18,7 +19,7 @@ definition f.def [defeq] (x y z : A) : f x y z = g (g x y) z := rfl
 definition d.def [defeq] (x y z w : A) : d x y z w = f (f x y z) (f y z w) (f x w z) := rfl
 
 -- Confirm that more recent annotations get priority
-print [defeq]
+print [defeq] foo
 
 attribute h.rfl [defeq] [priority 1001]
 attribute g.rfl [defeq] [priority 1001]
@@ -26,7 +27,7 @@ attribute f.rfl [defeq] [priority 1001]
 attribute d.rfl [defeq] [priority 1001]
 
 -- Confirm that priority annotations override
-print [defeq]
+print [defeq] foo
 
 attribute h.def [defeq] [priority 1001]
 attribute g.def [defeq] [priority 1001]
@@ -34,4 +35,5 @@ attribute f.def [defeq] [priority 1001]
 attribute d.def [defeq] [priority 1001]
 
 -- Confirm that most recent annotations get priority to break explicit priority ties
-print [defeq]
+print [defeq] foo
+end foo

tests/lean/defeq_simp_lemmas2.lean.expected.out

@@ -1,27 +1,27 @@
-defeq simp lemmas:
+defeq simp lemmas at namespace 'foo':
-#2, g ?M_1 ?M_2 ↦ h ?M_2
-#2, g ?M_1 ?M_2 ↦ ?M_2
 #4, d ?M_1 ?M_2 ?M_3 ?M_4 ↦ f (f ?M_1 ?M_2 ?M_3) (f ?M_2 ?M_3 ?M_4) (f ?M_1 ?M_4 ?M_3)
 #4, d ?M_1 ?M_2 ?M_3 ?M_4 ↦ ?M_3
 #3, f ?M_1 ?M_2 ?M_3 ↦ g (g ?M_1 ?M_2) ?M_3
 #3, f ?M_1 ?M_2 ?M_3 ↦ ?M_3
+#2, g ?M_1 ?M_2 ↦ h ?M_2
+#2, g ?M_1 ?M_2 ↦ ?M_2
 #1, h ?M_1 ↦ q ?M_1
 #1, h ?M_1 ↦ ?M_1
-defeq simp lemmas:
+defeq simp lemmas at namespace 'foo':
-#2 (1001), g ?M_1 ?M_2 ↦ ?M_2
-#2, g ?M_1 ?M_2 ↦ h ?M_2
 #4 (1001), d ?M_1 ?M_2 ?M_3 ?M_4 ↦ ?M_3
 #4, d ?M_1 ?M_2 ?M_3 ?M_4 ↦ f (f ?M_1 ?M_2 ?M_3) (f ?M_2 ?M_3 ?M_4) (f ?M_1 ?M_4 ?M_3)
 #3 (1001), f ?M_1 ?M_2 ?M_3 ↦ ?M_3
 #3, f ?M_1 ?M_2 ?M_3 ↦ g (g ?M_1 ?M_2) ?M_3
+#2 (1001), g ?M_1 ?M_2 ↦ ?M_2
+#2, g ?M_1 ?M_2 ↦ h ?M_2
 #1 (1001), h ?M_1 ↦ ?M_1
 #1, h ?M_1 ↦ q ?M_1
-defeq simp lemmas:
+defeq simp lemmas at namespace 'foo':
-#2 (1001), g ?M_1 ?M_2 ↦ h ?M_2
-#2 (1001), g ?M_1 ?M_2 ↦ ?M_2
 #4 (1001), d ?M_1 ?M_2 ?M_3 ?M_4 ↦ f (f ?M_1 ?M_2 ?M_3) (f ?M_2 ?M_3 ?M_4) (f ?M_1 ?M_4 ?M_3)
 #4 (1001), d ?M_1 ?M_2 ?M_3 ?M_4 ↦ ?M_3
 #3 (1001), f ?M_1 ?M_2 ?M_3 ↦ g (g ?M_1 ?M_2) ?M_3
 #3 (1001), f ?M_1 ?M_2 ?M_3 ↦ ?M_3
+#2 (1001), g ?M_1 ?M_2 ↦ h ?M_2
+#2 (1001), g ?M_1 ?M_2 ↦ ?M_2
 #1 (1001), h ?M_1 ↦ q ?M_1
 #1 (1001), h ?M_1 ↦ ?M_1