From 5e8068b2b2e1b572c6218e4d4e4cde24dc6d1553 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Mon, 16 Nov 2015 08:54:21 -0800
Subject: [PATCH] feat(library/blast/simplifier): draft of fusion

---
 library/algebra/simplifier.lean           | 116 ++++--
 src/frontends/lean/builtin_cmds.cpp       |  12 +-
 src/library/app_builder.cpp               |  66 +++
 src/library/app_builder.h                 |   7 +
 src/library/blast/blast.cpp               |  39 ++
 src/library/blast/blast.h                 |  18 +
 src/library/blast/simplifier.cpp          | 482 ++++++++++++++++------
 src/library/blast/simplifier.h            |  13 +-
 src/library/constants.cpp                 |  16 +
 src/library/constants.h                   |   4 +
 src/library/constants.txt                 |   4 +
 src/library/simplifier/simp_rule_set.cpp  |   2 +-
 tests/lean/simplifier12.lean              |   2 +-
 tests/lean/simplifier14.lean              |  29 ++
 tests/lean/simplifier14.lean.expected.out |   1 +
 tests/lean/simplifier15.lean              |  19 +
 tests/lean/simplifier15.lean.expected.out |  24 ++
 tests/lean/simplifier16.lean              |  15 +
 tests/lean/simplifier16.lean.expected.out |   2 +
 19 files changed, 719 insertions(+), 152 deletions(-)
 create mode 100644 tests/lean/simplifier14.lean
 create mode 100644 tests/lean/simplifier14.lean.expected.out
 create mode 100644 tests/lean/simplifier15.lean
 create mode 100644 tests/lean/simplifier15.lean.expected.out
 create mode 100644 tests/lean/simplifier16.lean
 create mode 100644 tests/lean/simplifier16.lean.expected.out

diff --git a/library/algebra/simplifier.lean b/library/algebra/simplifier.lean
index 8f7d4d6c6..f51d8ab94 100644
--- a/library/algebra/simplifier.lean
+++ b/library/algebra/simplifier.lean
@@ -7,23 +7,30 @@ import algebra.ring algebra.numeral
 
 namespace simplifier
 
-namespace sum_of_monomials
+-- TODO(dhs): refactor this once we fix `export` command
+-- TODO(dhs): make these [simp] rules in the global namespace
+namespace neg_helper
+    open algebra
+    variables {A : Type} [s : ring A] (a b : A)
+    include s
+    lemma neg_mul1 : (- a) * b = - (a * b) := eq.symm !algebra.neg_mul_eq_neg_mul
+    lemma neg_mul2 : a * (- b) = - (a * b) := eq.symm !algebra.neg_mul_eq_mul_neg
+    lemma sub_def : a - b = a + (- b) := rfl
+    lemma
+end neg_helper
 
-attribute algebra.add.assoc [simp]
-attribute algebra.add.comm [simp]
-attribute algebra.add.left_comm [simp]
+namespace ac
 
-attribute algebra.mul.left_comm [simp]
-attribute algebra.mul.comm [simp]
-attribute algebra.mul.assoc [simp]
+-- iff
+lemma eq_iff_true [simp] {A : Type} (a : A) : a = a ↔ true := sorry
 
-attribute algebra.left_distrib [simp]
-attribute algebra.right_distrib [simp]
-
-end sum_of_monomials
-
-namespace units
+-- neg
+attribute neg_helper.neg_mul1 [simp]
+attribute neg_helper.neg_mul2 [simp]
+attribute neg_helper.sub_def [simp]
+attribute algebra.neg_neg [simp]
 
+-- unit
 attribute algebra.zero_add [simp]
 attribute algebra.add_zero [simp]
 
@@ -33,7 +40,54 @@ attribute algebra.mul_zero [simp]
 attribute algebra.one_mul [simp]
 attribute algebra.mul_one [simp]
 
-end units
+-- ac
+attribute algebra.add.assoc [simp]
+attribute algebra.add.comm [simp]
+attribute algebra.add.left_comm [simp]
+
+attribute algebra.mul.left_comm [simp]
+attribute algebra.mul.comm [simp]
+attribute algebra.mul.assoc [simp]
+
+end ac
+
+namespace som
+
+-- iff
+lemma eq_iff_true [simp] {A : Type} (a : A) : a = a ↔ true := sorry
+
+-- neg
+attribute neg_helper.neg_mul1 [simp]
+attribute neg_helper.neg_mul2 [simp]
+attribute neg_helper.sub_def [simp]
+attribute algebra.neg_neg [simp]
+
+-- unit
+attribute algebra.zero_add [simp]
+attribute algebra.add_zero [simp]
+
+attribute algebra.zero_mul [simp]
+attribute algebra.mul_zero [simp]
+
+attribute algebra.one_mul [simp]
+attribute algebra.mul_one [simp]
+
+-- ac
+attribute algebra.add.assoc [simp]
+attribute algebra.add.comm [simp]
+attribute algebra.add.left_comm [simp]
+
+attribute algebra.mul.left_comm [simp]
+attribute algebra.mul.comm [simp]
+attribute algebra.mul.assoc [simp]
+
+-- distrib
+attribute algebra.left_distrib [simp]
+attribute algebra.right_distrib [simp]
+
+end som
+
+namespace numeral
 
 -- TODO(dhs): remove `add1` from the original lemmas and delete this
 namespace numeral_helper
@@ -69,8 +123,32 @@ lemma mul_bit1_helper1 [simp] {A : Type} [s : comm_ring A] (a b : A)
 
 end numeral_helper
 
-namespace numeral
+-- neg
+attribute neg_helper.neg_mul1 [simp]
+attribute neg_helper.neg_mul2 [simp]
+attribute neg_helper.sub_def [simp]
+attribute algebra.neg_neg [simp]
 
+-- unit
+attribute algebra.zero_add [simp]
+attribute algebra.add_zero [simp]
+
+attribute algebra.zero_mul [simp]
+attribute algebra.mul_zero [simp]
+
+attribute algebra.one_mul [simp]
+attribute algebra.mul_one [simp]
+
+-- ac
+attribute algebra.add.assoc [simp]
+attribute algebra.add.comm [simp]
+attribute algebra.add.left_comm [simp]
+
+attribute algebra.mul.left_comm [simp]
+attribute algebra.mul.comm [simp]
+attribute algebra.mul.assoc [simp]
+
+-- numerals
 attribute norm_num.bit0_add_bit0 [simp]
 attribute numeral_helper.bit1_add_one [simp]
 attribute norm_num.bit1_add_bit0 [simp]
@@ -78,9 +156,6 @@ attribute numeral_helper.bit1_add_bit1 [simp]
 attribute norm_num.bit0_add_bit1 [simp]
 attribute numeral_helper.one_add_bit1 [simp]
 
-attribute algebra.zero_add [simp]
-attribute algebra.add_zero [simp]
-
 attribute norm_num.one_add_one [simp]
 attribute numeral_helper.one_add_bit0 [simp]
 attribute numeral_helper.bit0_add_one [simp]
@@ -90,11 +165,6 @@ attribute numeral_helper.mul_bit0_helper1 [simp]
 attribute numeral_helper.mul_bit1_helper0 [simp]
 attribute numeral_helper.mul_bit1_helper1 [simp]
 
-attribute algebra.zero_mul [simp]
-attribute algebra.mul_zero [simp]
-attribute algebra.one_mul [simp]
-attribute algebra.mul_one [simp]
-
 end numeral
 
 end simplifier
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 1e6db8747..920caf2aa 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -1329,13 +1329,19 @@ static environment congr_cmd(parser & p) {
 
 static environment simplify_cmd(parser & p) {
     name rel = p.check_constant_next("invalid #simplify command, constant expected");
+    name ns = p.check_id_next("invalid #simplify command, id 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::simp::result r = blast::simplify(rel, e, get_simp_rule_sets(p.env()));
+    simp_rule_sets srss;
+    if (ns == name("null")) { }
+    if (ns == name("env")) { srss = get_simp_rule_sets(p.env()); }
+    else { srss = get_simp_rule_sets(p.env(), p.ios(), ns); }
+
+    blast::simp::result r = blast::simplify(rel, e, srss);
 
     flycheck_information info(p.regular_stream());
     if (info.enabled()) {
@@ -1343,8 +1349,8 @@ static environment simplify_cmd(parser & p) {
         p.regular_stream() << "simplify result:\n";
     }
 
-    if (r.is_none()) {
-        p.regular_stream() << "<refl>" << endl;
+    if (!r.has_proof()) {
+        p.regular_stream() << "(refl): " << r.get_new() << endl;
     } else {
         auto tc = mk_type_checker(p.env(), p.mk_ngen());
 
diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp
index 577527581..12007a57f 100644
--- a/src/library/app_builder.cpp
+++ b/src/library/app_builder.cpp
@@ -459,6 +459,48 @@ struct app_builder::imp {
         return mk_app(get_congr_name(), {H1, H2});
     }
 
+    expr mk_partial_add(expr const & A) {
+        level lvl = get_level(A);
+        auto A_has_add = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_has_add_name(), {lvl}), A));
+        if (!A_has_add) throw app_builder_exception();
+        return ::lean::mk_app(mk_constant(get_add_name(), {lvl}), A, *A_has_add);
+    }
+
+    expr mk_partial_mul(expr const & A) {
+        level lvl = get_level(A);
+        auto A_has_mul = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_has_mul_name(), {lvl}), A));
+        if (!A_has_mul) throw app_builder_exception();
+        return ::lean::mk_app(mk_constant(get_mul_name(), {lvl}), A, *A_has_mul);
+    }
+
+    expr mk_zero(expr const & A) {
+        level lvl = get_level(A);
+        auto A_has_zero = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_has_zero_name(), {lvl}), A));
+        if (!A_has_zero) throw app_builder_exception();
+        return ::lean::mk_app(mk_constant(get_zero_name(), {lvl}), A, *A_has_zero);
+    }
+
+    expr mk_one(expr const & A) {
+        level lvl = get_level(A);
+        auto A_has_one = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_has_one_name(), {lvl}), A));
+        if (!A_has_one) throw app_builder_exception();
+        return ::lean::mk_app(mk_constant(get_one_name(), {lvl}), A, *A_has_one);
+    }
+
+    expr mk_partial_left_distrib(expr const & A) {
+        level lvl = get_level(A);
+        auto A_distrib = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_algebra_distrib_name(), {lvl}), A));
+        if (!A_distrib) throw app_builder_exception();
+        return ::lean::mk_app(mk_constant(get_algebra_left_distrib_name(), {lvl}), A, *A_distrib);
+    }
+
+    expr mk_partial_right_distrib(expr const & A) {
+        level lvl = get_level(A);
+        auto A_distrib = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_algebra_distrib_name(), {lvl}), A));
+        if (!A_distrib) throw app_builder_exception();
+        return ::lean::mk_app(mk_constant(get_algebra_right_distrib_name(), {lvl}), A, *A_distrib);
+    }
+
     expr mk_false_rec(expr const & c, expr const & H) {
         level c_lvl = get_level(c);
         if (is_standard(m_ctx->env())) {
@@ -560,6 +602,30 @@ expr app_builder::mk_congr(expr const & H1, expr const & H2) {
     return m_ptr->mk_congr(H1, H2);
 }
 
+expr app_builder::mk_partial_add(expr const & A) {
+    return m_ptr->mk_partial_add(A);
+}
+
+expr app_builder::mk_partial_mul(expr const & A) {
+    return m_ptr->mk_partial_mul(A);
+}
+
+expr app_builder::mk_zero(expr const & A) {
+    return m_ptr->mk_zero(A);
+}
+
+expr app_builder::mk_one(expr const & A) {
+    return m_ptr->mk_one(A);
+}
+
+expr app_builder::mk_partial_left_distrib(expr const & A) {
+    return m_ptr->mk_partial_left_distrib(A);
+}
+
+expr app_builder::mk_partial_right_distrib(expr const & A) {
+    return m_ptr->mk_partial_right_distrib(A);
+}
+
 expr app_builder::mk_sorry(expr const & type) {
     return mk_app(get_sorry_name(), type);
 }
diff --git a/src/library/app_builder.h b/src/library/app_builder.h
index ee196ac13..690314a56 100644
--- a/src/library/app_builder.h
+++ b/src/library/app_builder.h
@@ -116,6 +116,13 @@ public:
     expr mk_congr_fun(expr const & H, expr const & a);
     expr mk_congr(expr const & H1, expr const & H2);
 
+    expr mk_partial_add(expr const & A);
+    expr mk_partial_mul(expr const & A);
+    expr mk_zero(expr const & A);
+    expr mk_one(expr const & A);
+    expr mk_partial_left_distrib(expr const & A);
+    expr mk_partial_right_distrib(expr const & A);
+
     /** \brief Create (@sorry type) */
     expr mk_sorry(expr const & type);
 
diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp
index db44e0674..f0bcb49e1 100644
--- a/src/library/blast/blast.cpp
+++ b/src/library/blast/blast.cpp
@@ -16,6 +16,7 @@ Author: Leonardo de Moura
 #include "library/type_context.h"
 #include "library/relation_manager.h"
 #include "library/congr_lemma_manager.h"
+#include "library/abstract_expr_manager.h"
 #include "library/projection.h"
 #include "library/tactic/goal.h"
 #include "library/blast/expr.h"
@@ -56,6 +57,7 @@ class blastenv {
     app_builder                m_app_builder;
     fun_info_manager           m_fun_info_manager;
     congr_lemma_manager        m_congr_lemma_manager;
+    abstract_expr_manager      m_abstract_expr_manager;
 
     class tctx : public type_context {
         blastenv &                              m_benv;
@@ -410,6 +412,7 @@ public:
         m_app_builder(*m_tmp_ctx),
         m_fun_info_manager(*m_tmp_ctx),
         m_congr_lemma_manager(m_app_builder, m_fun_info_manager),
+        m_abstract_expr_manager(m_fun_info_manager),
         m_tctx(*this),
         m_normalizer(m_tctx) {
         init_uref_mref_href_idxs();
@@ -482,6 +485,14 @@ public:
         return m_congr_lemma_manager.mk_congr_simp(fn);
     }
 
+    optional<congr_lemma> mk_congr_lemma(expr const & fn, unsigned num_args) {
+        return m_congr_lemma_manager.mk_congr(fn, num_args);
+    }
+
+    optional<congr_lemma> mk_congr_lemma(expr const & fn) {
+        return m_congr_lemma_manager.mk_congr(fn);
+    }
+
     fun_info get_fun_info(expr const & fn) {
         return m_fun_info_manager.get(fn);
     }
@@ -490,6 +501,14 @@ public:
         return m_fun_info_manager.get(fn, nargs);
     }
 
+    unsigned abstract_hash(expr const & e) {
+        return m_abstract_expr_manager.hash(e);
+    }
+
+    bool abstract_is_equal(expr const & e1, expr const & e2) {
+        return m_abstract_expr_manager.is_equal(e1, e2);
+    }
+
     /** \brief Convert an external expression into a blast expression
         It converts meta-variables to blast meta-variables, and ensures the expressions
         are maximally shared.
@@ -629,6 +648,16 @@ optional<congr_lemma> mk_congr_lemma_for_simp(expr const & fn) {
     return g_blastenv->mk_congr_lemma_for_simp(fn);
 }
 
+optional<congr_lemma> mk_congr_lemma(expr const & fn, unsigned num_args) {
+    lean_assert(g_blastenv);
+    return g_blastenv->mk_congr_lemma(fn, num_args);
+}
+
+optional<congr_lemma> mk_congr_lemma(expr const & fn) {
+    lean_assert(g_blastenv);
+    return g_blastenv->mk_congr_lemma(fn);
+}
+
 fun_info get_fun_info(expr const & fn) {
     lean_assert(g_blastenv);
     return g_blastenv->get_fun_info(fn);
@@ -639,6 +668,16 @@ fun_info get_fun_info(expr const & fn, unsigned nargs) {
     return g_blastenv->get_fun_info(fn, nargs);
 }
 
+unsigned abstract_hash(expr const & e) {
+    lean_assert(g_blastenv);
+    return g_blastenv->abstract_hash(e);
+}
+
+bool abstract_is_equal(expr const & e1, expr const & e2) {
+    lean_assert(g_blastenv);
+    return g_blastenv->abstract_is_equal(e1, e2);
+}
+
 void display_curr_state() {
     curr_state().display(env(), ios());
     display("\n");
diff --git a/src/library/blast/blast.h b/src/library/blast/blast.h
index b444fa149..6f9850cf5 100644
--- a/src/library/blast/blast.h
+++ b/src/library/blast/blast.h
@@ -79,12 +79,30 @@ optional<congr_lemma> mk_congr_lemma_for_simp(expr const & fn, unsigned num_args
 /** \brief Similar to previous procedure, but num_args == arith of fn */
 optional<congr_lemma> mk_congr_lemma_for_simp(expr const & fn);
 
+/** \brief Create a congruence lemma for the given function.
+    \pre num_args <= arity of fn
+    \remark The procedure may fail when app_builder used by it fails.
+    Example: it fail to infer the type of fn.
+
+    \remark The generated lemma is useful for proving that two terms
+    that are definitionally equal upto subsingletons are propositionally
+    equal.
+
+    \remark The type \c congr_lemma is defined at library/congr_lemma_manager.h */
+optional<congr_lemma> mk_congr_lemma(expr const & fn, unsigned num_args);
+/** \brief Similar to previous procedure, but num_args == arith of fn */
+optional<congr_lemma> mk_congr_lemma(expr const & fn);
+
 /** \brief Retrieve information for the given function. */
 fun_info get_fun_info(expr const & fn);
 /** \brief Retrieve information for the given function.
     \pre nargs <= arity fn. */
 fun_info get_fun_info(expr const & fn, unsigned nargs);
 
+/** \brief Hash and equality test for abstract expressions */
+unsigned abstract_hash(expr const & e);
+bool abstract_is_equal(expr const & e1, expr const & e2);
+
 /** \brief Display the current state of the blast tactic in the diagnostic channel. */
 void display_curr_state();
 /** \brief Display the given expression in the diagnostic channel. */
diff --git a/src/library/blast/simplifier.cpp b/src/library/blast/simplifier.cpp
index bb4eef946..7315eedd4 100644
--- a/src/library/blast/simplifier.cpp
+++ b/src/library/blast/simplifier.cpp
@@ -1,7 +1,7 @@
 /*
-Copyright (c) 2015 Daniel Selsam. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Daniel Selsam
+  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"
@@ -17,6 +17,7 @@ Author: Daniel Selsam
 #include "library/simplifier/simp_rule_set.h"
 #include "library/simplifier/ceqv.h"
 #include "library/app_builder.h"
+#include "library/num.h"
 #include "util/flet.h"
 #include "util/pair.h"
 #include "util/sexpr/option_declarations.h"
@@ -53,6 +54,13 @@ namespace blast {
 
 using simp::result;
 
+/* Names */
+
+static name * g_simplify_unit_namespace      = nullptr;
+static name * g_simplify_ac_namespace        = nullptr;
+static name * g_simplify_som_namespace       = nullptr;
+static name * g_simplify_numeral_namespace   = nullptr;
+
 /* Options */
 
 static name * g_simplify_max_steps     = nullptr;
@@ -98,11 +106,6 @@ bool get_simplify_fuse() {
 
 /* Miscellaneous helpers */
 
-static bool is_const_app(expr const & e, name const & n, unsigned nargs) {
-    expr const & f = get_app_fn(e);
-    return is_constant(f) && const_name(f) == n && get_app_num_args(e) == nargs;
-}
-
 static bool is_add_app(expr const & e) {
     return is_const_app(e, get_add_name(), 4);
 }
@@ -140,15 +143,13 @@ class simplifier {
     bool                                         m_fuse{get_simplify_fuse()};
 
     /* Cache */
-    static std::hash<simp_rule_set*> m_srss_hash;
-
     struct key {
         name              m_rel;
         expr              m_e;
         unsigned          m_hash;
 
         key(name const & rel, expr const & e):
-            m_rel(rel), m_e(e), m_hash(hash(rel.hash(), e.hash())) { }
+            m_rel(rel), m_e(e), m_hash(hash(rel.hash(), abstract_hash(e))) { }
     };
 
     struct key_hash_fn {
@@ -157,7 +158,7 @@ class simplifier {
 
     struct key_eq_fn {
         bool operator()(key const & k1, key const & k2) const {
-            return k1.m_rel == k2.m_rel && k1.m_e == k2.m_e;
+            return k1.m_rel == k2.m_rel && abstract_is_equal(k1.m_e, k2.m_e);
         }
     };
 
@@ -186,17 +187,19 @@ class simplifier {
         return srss;
     }
 
+    expr unfold_reducible_instances(expr const & e);
 
     bool instantiate_emetas(blast_tmp_type_context & tmp_tctx, unsigned num_emeta,
                             list<expr> const & emetas, list<bool> const & instances);
 
     /* Results */
-    result lift_from_eq(expr const & x, result const & r);
+    result lift_from_eq(expr const & e_old, result const & r_eq);
     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, simp_rule_sets const & srss);
     result simplify(expr const & e, bool is_root);
     result simplify_lambda(expr const & e);
     result simplify_pi(expr const & e);
@@ -205,6 +208,7 @@ class simplifier {
 
     /* Proving */
     optional<expr> prove(expr const & thm);
+    optional<expr> prove(expr const & thm, simp_rule_sets const & srss);
 
     /* Rewriting */
     result rewrite(expr const & e);
@@ -212,6 +216,7 @@ class simplifier {
     result rewrite(expr const & e, simp_rule const & sr);
 
     /* Congruence */
+    result congr_fun_arg(result const & r_f, result const & r_arg);
     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);
@@ -230,45 +235,91 @@ class simplifier {
 
 
 public:
-    simplifier(name const & rel, simp_rule_sets const & srss);
-    result operator()(expr const & e) { return simplify(e, true); }
+    simplifier(name const & rel): m_app_builder(*m_tmp_tctx), m_rel(rel) { }
+    result operator()(expr const & e, simp_rule_sets const & srss)  { return simplify(e, srss); }
 };
 
-/* Constructor */
-
-simplifier::simplifier(name const & rel, simp_rule_sets const & srss):
-    m_app_builder(*m_tmp_tctx), m_rel(rel), m_srss(srss) { }
-
 /* Cache */
 
 optional<result> simplifier::cache_lookup(expr const & e) {
     auto it = m_cache.find(key(m_rel, e));
-    if (it != m_cache.end()) return optional<result>(it->second);
-    return optional<result>();
+    if (it == m_cache.end()) return optional<result>();
+    /* The cache ignores subsingletons, so we may need to
+       synthesize a congruence lemma. */
+    expr e_old = it->first.m_e;
+    result r_old = it->second;
+    lean_assert(abstract_is_equal(e, e_old));
+    if (e == e_old) return optional<result>(r_old);
+    lean_assert(is_app(e_old));
+    buffer<expr> new_args, old_args;
+    expr const & f_new = get_app_args(e, new_args);
+    lean_verify(f_new == get_app_args(e_old, old_args));
+    auto congr_lemma = mk_congr_lemma(f_new, new_args.size());
+    if (!congr_lemma) return optional<result>();
+    expr proof = congr_lemma->get_proof();
+    expr type = congr_lemma->get_type();
+
+    unsigned i = 0;
+    for_each(congr_lemma->get_arg_kinds(), [&](congr_arg_kind const & ckind) {
+            if (ckind != congr_arg_kind::Cast) {
+                lean_assert(new_args[i] == old_args[i]);
+            }
+            proof = mk_app(proof, new_args[i]);
+            type = instantiate(binding_body(type), new_args[i]);
+            expr rfl;
+            switch (ckind) {
+            case congr_arg_kind::Fixed:
+                break;
+            case congr_arg_kind::Eq:
+                rfl = m_app_builder.mk_eq_refl(old_args[i]);
+                proof = mk_app(proof, old_args[i], rfl);
+                type = instantiate(binding_body(type), old_args[i]);
+                type = instantiate(binding_body(type), rfl);
+                break;
+            case congr_arg_kind::Cast:
+                proof = mk_app(proof, old_args[i]);
+                type = instantiate(binding_body(type), old_args[i]);
+                break;
+            }
+            i++;
+        });
+
+    lean_assert(is_eq(type));
+    result r_congr = result(e_old, proof);
+    return optional<result>(join(r_congr, r_old));
 }
+
 void simplifier::cache_save(expr const & e, result const & r) {
     m_cache.insert(mk_pair(key(m_rel, e), r));
 }
 
 /* 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));
-    expr motive_local = m_app_builder.mk_app(m_rel, x, l);
+result simplifier::lift_from_eq(expr const & e_old, result const & r_eq) {
+    if (!r_eq.has_proof()) return r_eq;
+    lean_assert(r_eq.has_proof());
+    /* r_eq.get_proof() : e_old = r_eq.get_new() */
+    /* goal : e_old <m_rel> r_eq.get_new() */
+    expr l = m_tmp_tctx->mk_tmp_local(m_tmp_tctx->infer(e_old));
+    expr motive_local = m_app_builder.mk_app(m_rel, e_old, l);
+    /* motive = fun y, e_old <m_rel> y */
     expr motive = Fun(l, motive_local);
-    expr Rxx = m_app_builder.mk_refl(m_rel, x);
-    expr pf = m_app_builder.mk_eq_rec(motive, Rxx, r.get_proof());
-    return result(r.get_new(), pf);
+    /* Rxx = x <m_rel> x */
+    expr Rxx = m_app_builder.mk_refl(m_rel, e_old);
+    expr pf = m_app_builder.mk_eq_rec(motive, Rxx, r_eq.get_proof());
+    return result(r_eq.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()) {
+    if (!r1.has_proof()) {
         return r2;
-    } else if (r2.is_none()) {
-        return r1;
+    } else if (!r2.has_proof()) {
+        lean_assert(r1.has_proof());
+        return result(r2.get_new(), r1.get_proof());
     } else {
+        /* If they both have proofs, we need to glue them together with transitivity. */
+        lean_assert(r1.has_proof() && r2.has_proof());
         expr trans = m_app_builder.mk_trans(m_rel, r1.get_proof(), r2.get_proof());
         return result(r2.get_new(), trans);
     }
@@ -276,20 +327,27 @@ result simplifier::join(result const & r1, result const & r2) {
 
 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 (!r.has_proof()) return result(e);
     expr pf = m_app_builder.mk_app(get_funext_name(), Fun(l, r.get_proof()));
     return result(e, pf);
 }
 
 result simplifier::finalize(result const & r) {
-    if (!r.is_none()) return r;
+    if (r.has_proof()) return r;
     expr pf = m_app_builder.mk_refl(m_rel, r.get_new());
     return result(r.get_new(), pf);
 }
 
 /* Simplification */
 
+result simplifier::simplify(expr const & e, simp_rule_sets const & srss) {
+    flet<simp_rule_sets> set_srss(m_srss, srss);
+    simplify_cache fresh_cache;
+    flet<simplify_cache> set_simplify_cache(m_cache, fresh_cache);
+    return simplify(e, true);
+}
+
 result simplifier::simplify(expr const & e, bool is_root) {
     m_num_steps++;
     flet<unsigned> inc_depth(m_depth, m_depth+1);
@@ -339,39 +397,37 @@ result simplifier::simplify(expr const & e, bool is_root) {
     if (!m_top_down) r = join(r, rewrite(whnf(r.get_new())));
 
     if (r.get_new() == e && !using_eq()) {
+        result r_eq;
         {
             flet<name> use_eq(m_rel, get_eq_name());
-            r = simplify(r.get_new(), is_root);
+            r_eq = simplify(r.get_new(), is_root);
         }
-        if (!r.is_none()) r = lift_from_eq(e, r);
+        r = join(r, lift_from_eq(r.get_new(), r_eq));
     }
 
-    if (m_exhaustive && r.get_new() != e) r = join(r, simplify(r.get_new(), is_root));
-
-    if (m_fuse && using_eq()) r = join(r, maybe_fuse(r.get_new(), is_root));
+    if (m_exhaustive && r.has_proof()) r = join(r, simplify(r.get_new(), is_root));
 
     if (m_memoize) cache_save(e, r);
 
+    if (m_fuse && using_eq()) r = join(r, maybe_fuse(r.get_new(), is_root));
+
     return r;
 }
 
-result simplifier::simplify_lambda(expr const & _e) {
-    lean_assert(is_lambda(_e));
-    expr e = _e;
+result simplifier::simplify_lambda(expr const & e) {
+    lean_assert(is_lambda(e));
+    expr t = 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));
+    while (is_lambda(t)) {
+        expr d = instantiate_rev(binding_domain(t), ls.size(), ls.data());
+        expr l = m_tmp_tctx->mk_tmp_local(d, binding_info(t));
         ls.push_back(l);
-        e = instantiate(binding_body(e), l);
+        t = instantiate(binding_body(t), l);
     }
 
-    result r = simplify(e, false);
-    if (r.is_none()) { return result(_e); }
-
+    result r = simplify(t, false);
     for (int i = ls.size() - 1; i >= 0; --i) r = funext(r, ls[i]);
-
     return r;
 }
 
@@ -380,14 +436,31 @@ result simplifier::simplify_pi(expr const & e) {
     return try_congrs(e);
 }
 
-result simplifier::simplify_app(expr const & e) {
-    lean_assert(is_app(e));
+expr simplifier::unfold_reducible_instances(expr const & e) {
+    buffer<expr> args;
+    expr f = get_app_args(e, args);
+    fun_info f_info = get_fun_info(f, args.size());
+    int i = -1;
+    for_each(f_info.get_params_info(), [&](param_info const & p_info) {
+            i++;
+            if (p_info.is_inst_implicit() && !p_info.is_subsingleton()) {
+//                ios().get_diagnostic_channel() << "normalize: "
+//                                               << args[i] << "\n==>\n" << blast::normalize(args[i]) << "\n";
+                args[i] = blast::normalize(args[i]);
+            }
+        });
+    return mk_app(f, args);
+}
+
+result simplifier::simplify_app(expr const & _e) {
+    lean_assert(is_app(_e));
+    expr e = unfold_reducible_instances(_e);
 
     /* (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;
+    result r_user = try_congrs(e);
+    if (r_user.has_proof()) {
+        if (using_eq()) return join(r_user, simplify_fun(r_user.get_new()));
+        else return r_user;
     }
 
     /* (2) Synthesize congruence lemma */
@@ -409,17 +482,13 @@ result simplifier::simplify_app(expr const & e) {
         result r_f = simplify(f, false);
 
         if (is_dependent_fn(f)) {
-            if (r_f.is_none()) return e;
-            else return congr_fun(r_f, arg);
+            if (r_f.has_proof()) return congr_fun(r_f, arg);
+            else return mk_app(r_f.get_new(), arg);
         } else {
             result r_arg = simplify(arg, false);
-            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 congr_fun_arg(r_f, r_arg);
         }
     }
-
     return result(e);
 }
 
@@ -428,8 +497,7 @@ result simplifier::simplify_fun(expr const & e) {
     buffer<expr> args;
     expr const & f = get_app_args(e, args);
     result r_f = simplify(f, true);
-    if (r_f.is_none()) return result(e);
-    else return congr_funs(r_f, args);
+    return congr_funs(r_f, args);
 }
 
 /* Proving */
@@ -446,6 +514,18 @@ optional<expr> simplifier::prove(expr const & thm) {
     return none_expr();
 }
 
+optional<expr> simplifier::prove(expr const & thm, simp_rule_sets const & srss) {
+    flet<name> set_name(m_rel, get_iff_name());
+    result r_cond = simplify(thm, srss);
+    if (is_constant(r_cond.get_new()) && const_name(r_cond.get_new()) == get_true_name()) {
+        expr pf = m_app_builder.mk_app(get_iff_elim_right_name(),
+                                       finalize(r_cond).get_proof(),
+                                       mk_constant(get_true_intro_name()));
+        return some_expr(pf);
+    }
+    return none_expr();
+}
+
 /* Rewriting */
 
 result simplifier::rewrite(expr const & e) {
@@ -453,7 +533,7 @@ result simplifier::rewrite(expr const & e) {
     while (true) {
         result r_ctx = rewrite(r.get_new(), m_ctx_srss);
         result r_new = rewrite(r_ctx.get_new(), m_srss);
-        if (r_ctx.is_none() && r_new.is_none()) break;
+        if (!r_ctx.has_proof() && !r_new.has_proof()) break;
         r = join(join(r, r_ctx), r_new);
     }
     return r;
@@ -470,7 +550,7 @@ result simplifier::rewrite(expr const & e, simp_rule_sets const & srss) {
 
     for_each(*srs, [&](simp_rule const & sr) {
             result r_new = rewrite(r.get_new(), sr);
-            if (r_new.is_none()) return;
+            if (!r_new.has_proof()) return;
             r = join(r, r_new);
         });
     return r;
@@ -504,13 +584,20 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
     }
 
     expr pf = tmp_tctx->instantiate_uvars_mvars(sr.get_proof());
-    return result(result(new_rhs, pf));
+    return result(new_rhs, pf);
 }
 
 /* Congruence */
 
+result simplifier::congr_fun_arg(result const & r_f, result const & r_arg) {
+    if (!r_f.has_proof() && !r_arg.has_proof()) return result(mk_app(r_f.get_new(), r_arg.get_new()));
+    else if (!r_f.has_proof()) return congr_arg(r_f.get_new(), r_arg);
+    else if (!r_arg.has_proof()) return congr_fun(r_f, r_arg.get_new());
+    else return congr(r_f, r_arg);
+}
+
 result simplifier::congr(result const & r_f, result const & r_arg) {
-    lean_assert(!r_f.is_none() && !r_arg.is_none());
+    lean_assert(r_f.has_proof() && r_arg.has_proof());
     // theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂
     expr e  = mk_app(r_f.get_new(), r_arg.get_new());
     expr pf = m_app_builder.mk_congr(r_f.get_proof(), r_arg.get_proof());
@@ -518,7 +605,7 @@ result simplifier::congr(result const & r_f, result const & r_arg) {
 }
 
 result simplifier::congr_fun(result const & r_f, expr const & arg) {
-    lean_assert(!r_f.is_none());
+    lean_assert(r_f.has_proof());
     // theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a
     expr e  = mk_app(r_f.get_new(), arg);
     expr pf = m_app_builder.mk_congr_fun(r_f.get_proof(), arg);
@@ -526,20 +613,23 @@ result simplifier::congr_fun(result const & r_f, expr const & arg) {
 }
 
 result simplifier::congr_arg(expr const & f, result const & r_arg) {
-    lean_assert(!r_arg.is_none());
+    lean_assert(r_arg.has_proof());
     // theorem congr_arg {A B : Type} {a₁ a₂ : A} (f : A → B) : a₁ = a₂ → f a₁ = f a₂
     expr e  = mk_app(f, r_arg.get_new());
     expr pf = m_app_builder.mk_congr_arg(f, r_arg.get_proof());
     return result(e, pf);
 }
 
+/* Note: handles reflexivity */
 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]);
+    }
+    if (!r_f.has_proof()) return result(e);
+    expr pf = r_f.get_proof();
+    for (unsigned i = 0; i < args.size(); ++i) {
         pf = m_app_builder.mk_app(get_congr_fun_name(), pf, args[i]);
     }
     return result(e, pf);
@@ -554,7 +644,7 @@ result simplifier::try_congrs(expr const & e) {
 
     result r(e);
     for_each(*crs, [&](congr_rule const & cr) {
-            if (!r.is_none()) return;
+            if (r.has_proof()) return;
             r = try_congr(e, cr);
         });
     return r;
@@ -575,42 +665,34 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) {
     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->instantiate_uvars_mvars(tmp_tctx->infer(m));
+            if (failed) return;
+            buffer<expr> ls;
+            expr m_type = tmp_tctx->instantiate_uvars_mvars(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(m_type));
-            lean_assert(!has_metavar(l));
-            ls.push_back(l);
-            m_type = instantiate(binding_body(m_type), l);
-        }
-
-        expr h_rel, h_lhs, h_rhs;
-        lean_verify(is_simp_relation(env(), m_type, h_rel, h_lhs, h_rhs) && is_constant(h_rel));
-        {
-            flet<name> set_name(m_rel, const_name(h_rel));
-            flet<simp_rule_sets> set_ctx_srss(m_ctx_srss, add_to_srss(m_ctx_srss, ls));
-
-            /* We need a new cache when we add to the context */
-            simplify_cache fresh_cache;
-            flet<simplify_cache> set_simplify_cache(m_cache, fresh_cache);
-
-            h_lhs = tmp_tctx->instantiate_uvars_mvars(h_lhs);
-            lean_assert(!has_metavar(h_lhs));
-
-            result r_congr_hyp = simplify(h_lhs, true);
-            expr hyp;
-            if (r_congr_hyp.is_none()) {
-                hyp = finalize(r_congr_hyp).get_proof();
-            } else {
-                hyp = r_congr_hyp.get_proof();
-                simplified = true;
+            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(m_type));
+                lean_assert(!has_metavar(l));
+                ls.push_back(l);
+                m_type = instantiate(binding_body(m_type), l);
             }
 
-            if (!tmp_tctx->is_def_eq(m, Fun(ls, hyp))) failed = true;
-        }
+            expr h_rel, h_lhs, h_rhs;
+            lean_verify(is_simp_relation(env(), m_type, h_rel, h_lhs, h_rhs) && is_constant(h_rel));
+            {
+                flet<name> set_name(m_rel, const_name(h_rel));
+                flet<simp_rule_sets> set_ctx_srss(m_ctx_srss, add_to_srss(m_ctx_srss, ls));
+
+                h_lhs = tmp_tctx->instantiate_uvars_mvars(h_lhs);
+                lean_assert(!has_metavar(h_lhs));
+
+                result r_congr_hyp = simplify(h_lhs, m_srss);
+                if (r_congr_hyp.has_proof()) simplified = true;
+                r_congr_hyp = finalize(r_congr_hyp);
+                expr hyp = finalize(r_congr_hyp).get_proof();
+
+                if (!tmp_tctx->is_def_eq(m, Fun(ls, hyp))) failed = true;
+            }
         });
 
     if (failed || !simplified) return result(e);
@@ -693,7 +775,7 @@ optional<result> simplifier::synth_congr(expr const & e, F && simp) {
             type = instantiate(binding_body(type), args[i]);
             if (ckind == congr_arg_kind::Eq) {
                 result r_arg = simp(args[i]);
-                if (!r_arg.is_none()) simplified = true;
+                if (r_arg.has_proof()) simplified = true;
                 r_arg = finalize(r_arg);
                 proof = mk_app(proof, r_arg.get_new(), r_arg.get_proof());
                 type = instantiate(binding_body(type), r_arg.get_new());
@@ -701,25 +783,25 @@ optional<result> simplifier::synth_congr(expr const & e, F && simp) {
             }
             i++;
         });
-    if (simplified) {
-        lean_assert(is_eq(type));
-        buffer<expr> type_args;
-        get_app_args(type, type_args);
-        expr & new_e = type_args[2];
-        return optional<result>(result(new_e, proof));
-    } else {
-        return optional<result>(result(e));
-    }
+    lean_assert(is_eq(type));
+    buffer<expr> type_args;
+    get_app_args(type, type_args);
+    expr & new_e = type_args[2];
+    if (simplified) return optional<result>(result(new_e, proof));
+    else return optional<result>(result(new_e));
 }
 
 /* Fusion */
 
 result simplifier::maybe_fuse(expr const & e, bool is_root) {
+//    ios().get_diagnostic_channel() << "maybe_fuse(" << e << ", " << is_root << ")\n";
     if (!is_app(e)) return result(e);
     if (is_root && is_add_app(e)) return fuse(e);
     if (!is_root && is_add_app(e)) return result(e);
+    lean_assert(!is_add_app(e));
     /* At this point we know we are an application of something other than + */
     optional<result> r = synth_congr(e, [&](expr const & arg) {
+//            ios().get_diagnostic_channel() << "synth_fuse: " << arg << "\n";
             if (is_add_app(arg)) return fuse(arg);
             else return result(arg);
         });
@@ -729,14 +811,169 @@ result simplifier::maybe_fuse(expr const & e, bool is_root) {
 
 result simplifier::fuse(expr const & e) {
     lean_assert(is_add_app(e));
-    // TODO(dhs): implement fusion
-    return result(e);
+//    ios().get_diagnostic_channel() << "FUSE: " << e << "\n\n";
+    flet<bool> no_recursive_fusion(m_fuse, false);
+
+    /* Note: we assume all negations are on the outside of the summands */
+
+    /* Example
+       1. Input (e): n1 * x1 * n2 * x2 + x3 + - (x1 * x2 * n3) + (- x3) + x4
+       2. Split summands: (n1 * n2) * (x1 * x2) + 1 * x3 + (- n3) * (x1 * x2) + (- 1) * x3 + 1 * x4
+       3. Group by variable (e_grp): ((n1 * n2) * (x1 * x2) + (- n3) * (x1 * x2)) + (1 * x3 + (-1) * x3) + x4
+       4. Introduce locals (e_grp_ls): ((n1 * n2) * l1 + (- n3) * l1) + (1 * l2 + (-1) * l2) + l3
+       5. Fuse (e_fused_ls): (n1 * n2 + (- n3)) * l1 + (1 + (- 1)) * l2 + 1 * l3
+       6. Simplify coefficients (e_simp_ls): (n1 * n2 + (- n3)) * l1 + l3
+       7. Instantiate locals (e_simp): (n1 * n2 + (- n3)) * (x1 * x2) + x4
+
+       Proofs
+       1. Prove (1) == (3) using simplify with [ac]
+       2. Prove (4) == (5) using simplify with [som]
+       3. Prove (5) == (6) using simplify with [numeral]
+       4. Prove (4) == (6) by transitivity of proofs (2) and (3)
+       5. Prove (3) == (7) by instantiating proof (4)
+       6. Prove (1) == (7) by transitivity of proofs (1) and (5)
+    */
+
+    /* Construct useful expressions */
+    buffer<expr> args;
+    get_app_args(e,args);
+    expr T = args[0];
+    expr f_add, f_mul, zero, one;
+    try {
+        f_add = m_app_builder.mk_partial_add(T);
+        f_mul = m_app_builder.mk_partial_mul(T);
+        zero = m_app_builder.mk_zero(T);
+        one = m_app_builder.mk_one(T);
+        expr left_distrib = m_app_builder.mk_partial_left_distrib(T);
+    } catch (app_builder_exception & ex) {
+        ios().get_diagnostic_channel() << "Cannot synthesize necessary instances\n";
+        return result(e);
+    }
+
+    /* (1 ==> 2) Split each summand into (a) numerals and (b) variables */
+    buffer<expr> numerals;
+    buffer<expr> variables;
+    expr s = e;
+    while (is_add_app(s)) {
+        buffer<expr> args;
+        expr f = get_app_args(s,args);
+        auto n_v = split_summand(args[2], f_mul, one);
+        numerals.push_back(n_v.first);
+        variables.push_back(n_v.second);
+        s = args[3];
+    }
+    auto n_v = split_summand(s, f_mul, one);
+    numerals.push_back(n_v.first);
+    variables.push_back(n_v.second);
+    lean_assert(numerals.size() == variables.size());
+
+    /* (2 ==> 3, 4, 5) Group the summands by variable */
+    expr_bi_struct_map<list<expr> > variable_to_numerals;
+    for (unsigned i = 0; i < numerals.size(); i++) {
+        auto it = variable_to_numerals.find(variables[i]);
+        if (it != variable_to_numerals.end()) it->second = cons(numerals[i], it->second);
+        else variable_to_numerals.insert({variables[i],list<expr>(numerals[i])});
+    }
+
+    expr e_grp = zero;
+    expr e_grp_ls = zero;
+    expr e_fused_ls = zero;
+
+    buffer<expr> locals;
+    variables.clear();
+    for (auto v_ns : variable_to_numerals) {
+        expr local = m_tmp_tctx->mk_tmp_local(T);
+        locals.push_back(local);
+        variables.push_back(v_ns.first);
+
+        expr term = zero;
+        expr term_ls = zero;
+        expr term_fused_ls = zero;
+        for_each(v_ns.second, [&](expr const & n) {
+                term = mk_app(f_add, mk_app(f_mul, v_ns.first, n), term);
+                term_ls = mk_app(f_add, mk_app(f_mul, local, n), term_ls);
+                term_fused_ls = mk_app(f_add, n, term_fused_ls);
+            });
+        e_grp = mk_app(f_add, term, e_grp);
+        e_grp_ls = mk_app(f_add, term_ls, e_grp_ls);
+        e_fused_ls = mk_app(f_add, mk_app(f_mul, term_fused_ls, local), e_fused_ls);
+    }
+
+    /* Prove (1) == (3) using simplify with [ac] */
+    auto pf_1_3 = prove(m_app_builder.mk_eq(e, e_grp),
+                        get_simp_rule_sets(env(), ios(), *g_simplify_ac_namespace));
+    if (!pf_1_3) {
+        diagnostic(env(), ios()) << e << "\n\n =?=\n\n" << e_grp << "\n";
+        throw blast_exception("Failed to prove (1) == (3) during fusion", e);
+    }
+
+    /* Prove (4) == (5) using simplify with [som] */
+    auto pf_4_5 = prove(m_app_builder.mk_eq(e_grp_ls, e_fused_ls),
+                        get_simp_rule_sets(env(), ios(), *g_simplify_som_namespace));
+    if (!pf_4_5) {
+        diagnostic(env(), ios()) << e_grp_ls << "\n\n =?=\n\n" << e_fused_ls << "\n";
+        throw blast_exception("Failed to prove (4) == (5) during fusion", e);
+    }
+
+    /* Prove (5) == (6) using simplify with [numeral] */
+    result r_simp_ls = simplify(e_fused_ls,
+                                get_simp_rule_sets(env(), ios(), *g_simplify_numeral_namespace));
+
+    /* Prove (4) == (6) by transitivity of proofs (2) and (3) */
+    expr pf_4_6;
+    if (!r_simp_ls.has_proof()) pf_4_6 = *pf_4_5;
+    else pf_4_6 = m_app_builder.mk_eq_trans(*pf_4_5, r_simp_ls.get_proof());
+
+    /* Prove (3) == (7) by instantiating proof (4) */
+    expr pf_3_7 = mk_app(Fun(locals, pf_4_6), variables);
+
+    /* Prove (1) == (7) by transitivity of proofs (1) and (5) */
+    expr pf_1_7 = m_app_builder.mk_eq_trans(*pf_1_3, pf_3_7);
+
+    return result(mk_app(Fun(locals, r_simp_ls.get_new()), variables), pf_1_7);
 }
 
+expr_pair simplifier::split_summand(expr const & e, expr const & f_mul, expr const & one) {
+    /* [e] is a possibly negated, possibly null product, where some of the multiplicands are numerals
+       and the rest are treated as variables. This method does the following conversion:
+       - (x1 * n1 * x2 * n3) ==> (-1 * n1 * n3) * (x1 * x2) */
+    expr s = e;
+    expr numeral = one;
+    expr variable = one;
+    if (is_neg_app(s)) {
+        buffer<expr> args;
+        get_app_args(s,args);
+        numeral = m_app_builder.mk_app(get_neg_name(), one);
+        s = args[2];
+    }
+    while (is_mul_app(s)) {
+        buffer<expr> args;
+        get_app_args(s,args);
+        expr const & multiplicand = args[2];
+        if (is_num(multiplicand)) numeral = mk_app(f_mul, multiplicand, numeral);
+        else {
+            if (variable == one) variable = multiplicand;
+            else variable = mk_app(f_mul, multiplicand, variable);
+        }
+        s = args[3];
+    }
+    if (is_num(s)) numeral = mk_app(f_mul, s, numeral);
+    else {
+        if (variable == one) variable = s;
+        else variable = mk_app(f_mul, s, variable);
+    }
+    return mk_pair(numeral, variable);
+}
 
 /* Setup and teardown */
 
 void initialize_simplifier() {
+    g_simplify_unit_namespace      = new name{"simplifier","unit"};
+    g_simplify_ac_namespace        = new name{"simplifier","ac"};
+    g_simplify_som_namespace       = new name{"simplifier","som"};
+    g_simplify_numeral_namespace   = new name{"simplifier","numeral"};
+
+
     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"};
@@ -773,11 +1010,16 @@ void finalize_simplifier() {
     delete g_simplify_exhaustive;
     delete g_simplify_top_down;
     delete g_simplify_max_steps;
+
+    delete g_simplify_numeral_namespace;
+    delete g_simplify_som_namespace;
+    delete g_simplify_ac_namespace;
+    delete g_simplify_unit_namespace;
 }
 
 /* Entry point */
 result simplify(name const & rel, expr const & e, simp_rule_sets const & srss) {
-    return simplifier(rel, srss)(e);
+    return simplifier(rel)(e, srss);
 }
 
 }}
diff --git a/src/library/blast/simplifier.h b/src/library/blast/simplifier.h
index 139f33edf..93f933294 100644
--- a/src/library/blast/simplifier.h
+++ b/src/library/blast/simplifier.h
@@ -16,22 +16,27 @@ namespace simp {
 /* Struct to store results of simplification */
 struct result {
     /* Invariant [m_pf : m_orig <rel> m_new] */
+    /* Note: we only keep [m_old] to make the code easier to understand.
+       It could be optimized away in the future. */
     expr m_new;
+
+    /* If proof is not provided, it is assumed to be reflexivity */
     optional<expr> m_proof;
 
 public:
+    result() {}
     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) {}
+    result(expr const & e, expr const & proof): m_new(e), m_proof(proof) {}
+    result(expr const & e, optional<expr> const & proof): m_new(e), m_proof(proof) {}
+
+    bool has_proof() const { return static_cast<bool>(m_proof); }
 
-    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(name const & rel, expr const & e, simp_rule_sets const & srss);
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index b03cee53d..7051c8401 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -4,6 +4,9 @@
 #include "util/name.h"
 namespace lean{
 name const * g_absurd = nullptr;
+name const * g_algebra_distrib = nullptr;
+name const * g_algebra_left_distrib = nullptr;
+name const * g_algebra_right_distrib = nullptr;
 name const * g_add = nullptr;
 name const * g_and = nullptr;
 name const * g_and_elim_left = nullptr;
@@ -45,6 +48,7 @@ name const * g_has_one = nullptr;
 name const * g_has_zero_zero = nullptr;
 name const * g_has_one_one = nullptr;
 name const * g_has_add = nullptr;
+name const * g_has_mul = nullptr;
 name const * g_heq = nullptr;
 name const * g_heq_refl = nullptr;
 name const * g_heq_to_eq = nullptr;
@@ -173,6 +177,9 @@ name const * g_well_founded = nullptr;
 name const * g_zero = nullptr;
 void initialize_constants() {
     g_absurd = new name{"absurd"};
+    g_algebra_distrib = new name{"algebra", "distrib"};
+    g_algebra_left_distrib = new name{"algebra", "left_distrib"};
+    g_algebra_right_distrib = new name{"algebra", "right_distrib"};
     g_add = new name{"add"};
     g_and = new name{"and"};
     g_and_elim_left = new name{"and", "elim_left"};
@@ -214,6 +221,7 @@ void initialize_constants() {
     g_has_zero_zero = new name{"has_zero", "zero"};
     g_has_one_one = new name{"has_one", "one"};
     g_has_add = new name{"has_add"};
+    g_has_mul = new name{"has_mul"};
     g_heq = new name{"heq"};
     g_heq_refl = new name{"heq", "refl"};
     g_heq_to_eq = new name{"heq", "to_eq"};
@@ -343,6 +351,9 @@ void initialize_constants() {
 }
 void finalize_constants() {
     delete g_absurd;
+    delete g_algebra_distrib;
+    delete g_algebra_left_distrib;
+    delete g_algebra_right_distrib;
     delete g_add;
     delete g_and;
     delete g_and_elim_left;
@@ -384,6 +395,7 @@ void finalize_constants() {
     delete g_has_zero_zero;
     delete g_has_one_one;
     delete g_has_add;
+    delete g_has_mul;
     delete g_heq;
     delete g_heq_refl;
     delete g_heq_to_eq;
@@ -512,6 +524,9 @@ void finalize_constants() {
     delete g_zero;
 }
 name const & get_absurd_name() { return *g_absurd; }
+name const & get_algebra_distrib_name() { return *g_algebra_distrib; }
+name const & get_algebra_left_distrib_name() { return *g_algebra_left_distrib; }
+name const & get_algebra_right_distrib_name() { return *g_algebra_right_distrib; }
 name const & get_add_name() { return *g_add; }
 name const & get_and_name() { return *g_and; }
 name const & get_and_elim_left_name() { return *g_and_elim_left; }
@@ -553,6 +568,7 @@ name const & get_has_one_name() { return *g_has_one; }
 name const & get_has_zero_zero_name() { return *g_has_zero_zero; }
 name const & get_has_one_one_name() { return *g_has_one_one; }
 name const & get_has_add_name() { return *g_has_add; }
+name const & get_has_mul_name() { return *g_has_mul; }
 name const & get_heq_name() { return *g_heq; }
 name const & get_heq_refl_name() { return *g_heq_refl; }
 name const & get_heq_to_eq_name() { return *g_heq_to_eq; }
diff --git a/src/library/constants.h b/src/library/constants.h
index a838ca55c..b5e88e9e2 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -6,6 +6,9 @@ namespace lean {
 void initialize_constants();
 void finalize_constants();
 name const & get_absurd_name();
+name const & get_algebra_distrib_name();
+name const & get_algebra_left_distrib_name();
+name const & get_algebra_right_distrib_name();
 name const & get_add_name();
 name const & get_and_name();
 name const & get_and_elim_left_name();
@@ -47,6 +50,7 @@ name const & get_has_one_name();
 name const & get_has_zero_zero_name();
 name const & get_has_one_one_name();
 name const & get_has_add_name();
+name const & get_has_mul_name();
 name const & get_heq_name();
 name const & get_heq_refl_name();
 name const & get_heq_to_eq_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index 05c6a027d..f4208ff29 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -1,4 +1,7 @@
 absurd
+algebra.distrib
+algebra.left_distrib
+algebra.right_distrib
 add
 and
 and.elim_left
@@ -40,6 +43,7 @@ has_one
 has_zero.zero
 has_one.one
 has_add
+has_mul
 heq
 heq.refl
 heq.to_eq
diff --git a/src/library/simplifier/simp_rule_set.cpp b/src/library/simplifier/simp_rule_set.cpp
index 68afd9206..c6581c492 100644
--- a/src/library/simplifier/simp_rule_set.cpp
+++ b/src/library/simplifier/simp_rule_set.cpp
@@ -532,8 +532,8 @@ simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios,
     simp_rule_sets set;
     list<pair<bool, name>> const * cnames = rrs_ext::get_entries(env, ns);
     if (cnames) {
-        tmp_type_context tctx(env, ios);
         for (pair<bool, name> const & p : *cnames) {
+            tmp_type_context tctx(env, ios);
             set = add_core(tctx, set, p.second);
         }
     }
diff --git a/tests/lean/simplifier12.lean b/tests/lean/simplifier12.lean
index dcde14082..f3c95f756 100644
--- a/tests/lean/simplifier12.lean
+++ b/tests/lean/simplifier12.lean
@@ -1,5 +1,5 @@
 import algebra.simplifier
-open algebra simplifier.sum_of_monomials simplifier.units
+open algebra simplifier.som
 
 set_option simplify.max_steps 1000
 universe l
diff --git a/tests/lean/simplifier14.lean b/tests/lean/simplifier14.lean
new file mode 100644
index 000000000..c61f172dc
--- /dev/null
+++ b/tests/lean/simplifier14.lean
@@ -0,0 +1,29 @@
+-- Basic fusion
+import algebra.simplifier
+open algebra
+
+universe l
+constants (T : Type.{l}) (s : algebra.comm_ring T)
+constants (x1 x2 x3 x4 : T) (f g : T → T)
+attribute s [instance]
+set_option simplify.max_steps 10000
+set_option simplify.fuse true
+
+#simplify eq simplifier.som 0 x1
+#simplify eq simplifier.som 0 x1 + x1
+#simplify eq simplifier.som 0 (x1 + x1) + x1
+#simplify eq simplifier.som 0 (x1 + x1) + (x1 + x1)
+#simplify eq simplifier.som 0 x1 + x1 + x1 + x1
+#simplify eq simplifier.som 0 x1 + x1 + (x1 + x1) + x1
+#simplify eq simplifier.som 0 x1 - x1
+#simplify eq simplifier.som 0 (x1 - x1) + x1
+#simplify eq simplifier.som 0 (x1 + x1) - (x1 + x1)
+#simplify eq simplifier.som 0 x1 + x1 - x1 - x1
+#simplify eq simplifier.som 0 x1 + x1 + (x1 + x1) + x1
+#simplify eq simplifier.som 0 (x1 - x2) + x2 - x1
+#simplify eq simplifier.som 0 (x1 + x1 + x2 + x1) - 2* x2 + 1 * x2 - 3 * x1
+#simplify eq simplifier.som 0 x2 + x1 - x2 - - x1
+#simplify eq simplifier.som 0 x2 * x1 + 3 * x1 + (2 * x2 - 8 * x2 * 4 * x1) + x1 * x2
+#simplify eq simplifier.som 0 (x1 - 2 * x3 * x2) + x2 * x3 * 3 - 1 * 0 * x1 * x2
+#simplify eq simplifier.som 0 (x1 * x3 + x1 * 2 + x2 * 3 * x3 + x1 * x2) - 2* x2 * x1 + 1 * x2 * x1 - 3 * x1 * x3
+#simplify eq simplifier.som 0 x2 + x1 - x2 - - x1
diff --git a/tests/lean/simplifier14.lean.expected.out b/tests/lean/simplifier14.lean.expected.out
new file mode 100644
index 000000000..30404ce4c
--- /dev/null
+++ b/tests/lean/simplifier14.lean.expected.out
@@ -0,0 +1 @@
+TODO
\ No newline at end of file
diff --git a/tests/lean/simplifier15.lean b/tests/lean/simplifier15.lean
new file mode 100644
index 000000000..6f619b176
--- /dev/null
+++ b/tests/lean/simplifier15.lean
@@ -0,0 +1,19 @@
+-- normalizing reducible non-subsingleton instances
+import algebra.simplifier
+open algebra
+
+universe l
+constants (T : Type.{l}) (s : algebra.comm_ring T)
+constants (x1 x2 x3 x4 : T) (f g : T → T)
+attribute s [instance]
+
+set_option pp.all true
+
+#simplify eq null 0 x1
+#simplify eq null 0 x1 + x1
+#simplify eq null 0 x1 + x1 + x1
+#simplify eq null 0 x1 + x1 + x1 + x1
+#simplify eq null 0 x1 + x1 + (x1 + x1) + x1
+#simplify eq simplifier.ac 0 x1 + x1 + x1
+#simplify eq simplifier.ac 0 x1 + x1 + x1 + x1
+#simplify eq simplifier.ac 0 x1 + x1 + (x1 + x1) + x1
diff --git a/tests/lean/simplifier15.lean.expected.out b/tests/lean/simplifier15.lean.expected.out
new file mode 100644
index 000000000..134429183
--- /dev/null
+++ b/tests/lean/simplifier15.lean.expected.out
@@ -0,0 +1,24 @@
+(refl): x1
+(refl): @add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1
+(refl): @add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s))
+  (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1)
+  x1
+(refl): @add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s))
+  (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s))
+     (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1)
+     x1)
+  x1
+(refl): @add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s))
+  (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s))
+     (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1)
+     (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1))
+  x1
+@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1
+  (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1)
+@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1
+  (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1
+     (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1))
+@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1
+  (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1
+     (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1
+        (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1)))
diff --git a/tests/lean/simplifier16.lean b/tests/lean/simplifier16.lean
new file mode 100644
index 000000000..b06086f4c
--- /dev/null
+++ b/tests/lean/simplifier16.lean
@@ -0,0 +1,15 @@
+-- Canonicalizing subsingletons
+import algebra.ring
+open algebra
+
+set_option pp.all true
+universes l j k
+constants (A : Type.{l}) (s : comm_ring A)
+attribute s [instance]
+constants (x y : A) (P : A → Type.{j}) (P_ss : ∀ a, subsingleton (P a))
+constants (f : Π a, P a → A) (Px1 Px2 Px3 : P x)
+constants (g : A → A → A)
+attribute P_ss [instance]
+
+#simplify eq env 0 g (f x Px1) (f x Px2)
+#simplify eq env 0 g (f x Px1) (g (f x Px2) (f x Px3))
diff --git a/tests/lean/simplifier16.lean.expected.out b/tests/lean/simplifier16.lean.expected.out
new file mode 100644
index 000000000..099f8f9d8
--- /dev/null
+++ b/tests/lean/simplifier16.lean.expected.out
@@ -0,0 +1,2 @@
+g (f x Px1) (f x Px1)
+g (f x Px1) (g (f x Px1) (f x Px1))