diff --git a/doc/changes.md b/doc/changes.md
index d5d11352bb..79dbc55413 100644
--- a/doc/changes.md
+++ b/doc/changes.md
@@ -34,7 +34,10 @@ master branch (aka work in progress branch)
    tries to discharge the subgoal by reducing it to `true`.
    Example: `simp {discharger := assumption}`.
 
-* `simp` can be used to unfold projection applications. Example: `simp [has_add.add]`.
+* `simp` can be used to unfold projection applications when the argument is a type class instance.
+   Example: `simp [has_add.add]` will replace `@has_add.add nat nat.has_add a b` with `nat.add a b`
+
+* `dsimp` has several new configuration options to control reduction (e.g., `iota`, `beta`, `zeta`, ...).
 
 *Changes*
 
@@ -56,6 +59,10 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
 * All `dsimp` tactics fail if they did not change anything.
   We can simulate the v3.2.0 using `dsimp {fail_if_unchaged := ff}` or `try dsimp`.
 
+* `dsimp` does not unfold reducible definitions by default anymore.
+  Example: `function.comp` applications will not be unfolded by default.
+  We should use `dsimp [f]` if we want to reduce a reducible definition `f`.
+
 * All `dunfold` and `unfold` tactics fail if they did not unfold anything.
   We can simulate the v3.2.0 using `unfold f {fail_if_unchaged := ff}` or `try {unfold f}`.
 
diff --git a/library/data/hash_map.lean b/library/data/hash_map.lean
index 9d795f6656..aed3a17cf4 100644
--- a/library/data/hash_map.lean
+++ b/library/data/hash_map.lean
@@ -445,7 +445,7 @@ structure hash_map (α : Type u) [decidable_eq α] (β : α → Type v) :=
 
 def mk_hash_map {α : Type u} [decidable_eq α] {β : α → Type v} (hash_fn : α → nat) (nbuckets := 8) : hash_map α β :=
 let n := if nbuckets = 0 then 8 else nbuckets in
-let nz : n > 0 := by abstract {dsimp, cases nbuckets, {simp, tactic.comp_val}, simp [if_pos, nat.succ_ne_zero], apply nat.zero_lt_succ} in
+let nz : n > 0 := by abstract { cases nbuckets, {simp, tactic.comp_val}, simp [if_pos, nat.succ_ne_zero], apply nat.zero_lt_succ} in
 { hash_fn  := hash_fn,
   size     := 0,
   nbuckets := ⟨n, nz⟩,
diff --git a/library/init/data/list/instances.lean b/library/init/data/list/instances.lean
index 08009b92c4..80de070766 100644
--- a/library/init/data/list/instances.lean
+++ b/library/init/data/list/instances.lean
@@ -36,7 +36,7 @@ instance : monad list :=
  id_map := begin
    intros _ xs, induction xs with x xs ih,
    { refl },
-   { dsimp at ih, dsimp, simph }
+   { dsimp [function.comp] at ih, dsimp [function.comp], simph }
  end,
  pure_bind := by simp_intros,
  bind_assoc := begin
diff --git a/library/init/data/nat/bitwise.lean b/library/init/data/nat/bitwise.lean
index 3cf887f709..a3b4048062 100644
--- a/library/init/data/nat/bitwise.lean
+++ b/library/init/data/nat/bitwise.lean
@@ -203,13 +203,15 @@ namespace nat
     binary_rec z f (bit b n) = f b n (binary_rec z f n) :=
   begin
     rw [binary_rec.equations._eqn_1],
-    cases (by apply_instance : decidable (bit b n = 0)) with b0 b0; dsimp [dite],
-    { generalize (binary_rec._main._pack._proof_2 (bit b n)) e,
-      rw [bodd_bit, div2_bit], intro e, refl },
-    { generalize (binary_rec._main._pack._proof_1 (bit b n) b0) e,
-      have bf := bodd_bit b n, have n0 := div2_bit b n,
-      rw b0 at bf n0, simp at bf n0, rw [-bf, -n0, binary_rec_zero],
-      exact λe, h.symm },
+    cases (by apply_instance : decidable (bit b n = 0)) with b0 b0,
+    {rw [dif_neg],
+     generalize (binary_rec._main._pack._proof_2 (bit b n)) e,
+     rw [bodd_bit, div2_bit], intro e, refl, assumption},
+    {rw [dif_pos],
+     generalize (binary_rec._main._pack._proof_1 (bit b n) b0) e,
+     have bf := bodd_bit b n, have n0 := div2_bit b n,
+     rw b0 at bf n0, simp at bf n0, rw [-bf, -n0, binary_rec_zero],
+     exact λe, h.symm }
   end
 
   lemma bitwise_bit_aux {f : bool → bool → bool} (h : f ff ff = ff) :
diff --git a/library/init/data/set.lean b/library/init/data/set.lean
index a7fbe9b633..fd664192de 100644
--- a/library/init/data/set.lean
+++ b/library/init/data/set.lean
@@ -90,7 +90,7 @@ instance : functor set :=
  end,
  map_comp := begin
    intros, apply funext, intro c,
-   dsimp [image, set_of],
+   dsimp [image, set_of, function.comp],
    exact propext ⟨λ ⟨a, ⟨h₁, h₂⟩⟩, ⟨g a, ⟨⟨a, ⟨h₁, rfl⟩⟩, h₂⟩⟩,
                   λ ⟨b, ⟨⟨a, ⟨h₁, h₂⟩⟩, h₃⟩⟩, ⟨a, ⟨h₁, h₂.symm ▸ h₃⟩⟩⟩
  end}
diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index a17a1ae9ee..175ee6ed3b 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -69,6 +69,10 @@ structure dsimp_config :=
 (single_pass : bool        := ff)
 (fail_if_unchanged         := tt)
 (eta                       := tt)
+(zeta : bool               := tt)
+(beta : bool               := tt)
+(proj : bool               := tt) -- reduce projections
+(iota : bool               := tt)
 (memoize                   := tt)
 end tactic
 
@@ -195,6 +199,7 @@ structure simp_config :=
 (beta : bool               := tt)
 (eta  : bool               := tt)
 (proj : bool               := tt) -- reduce projections
+(iota : bool               := tt)
 (single_pass : bool        := ff)
 (fail_if_unchanged         := tt)
 (memoize                   := tt)
diff --git a/library/init/native/result.lean b/library/init/native/result.lean
index 0f9e058262..a60c95703f 100644
--- a/library/init/native/result.lean
+++ b/library/init/native/result.lean
@@ -49,7 +49,7 @@ section resultT
   {pure := @resultT.pure M m E, bind := @resultT.and_then M m E,
    id_map := begin
      intros, cases x,
-     dsimp [resultT.and_then],
+     dsimp [resultT.and_then, function.comp],
      have h : @resultT.and_then._match_1 _ m E α _ resultT.pure = pure,
      { apply funext, intro x,
        cases x; simp [resultT.and_then, resultT.pure, resultT.and_then] },
diff --git a/src/library/tactic/dsimplify.cpp b/src/library/tactic/dsimplify.cpp
index ae6129cbd5..c411d31e23 100644
--- a/src/library/tactic/dsimplify.cpp
+++ b/src/library/tactic/dsimplify.cpp
@@ -24,6 +24,40 @@ Author: Leonardo de Moura
 #endif
 
 namespace lean {
+expr reduce_beta_eta_proj_iota(type_context & ctx, expr e, bool beta, bool eta, bool proj, bool iota) {
+    bool p;
+    do {
+        p = false;
+        if (beta) {
+            expr new_e = head_beta_reduce(e);
+            if (!is_eqp(new_e, e)) {
+                e = new_e;
+                p = true;
+            }
+        }
+        if (proj) {
+            if (auto v = ctx.reduce_projection(e)) {
+                e = *v;
+                p = true;
+            }
+        }
+        if (eta) {
+            expr new_e = try_eta(e);
+            if (!is_eqp(new_e, e)) {
+                e = new_e;
+                p = true;
+            }
+        }
+        if (iota) {
+            if (auto v = ctx.reduce_recursor(e)) {
+                e = *v;
+                p = true;
+            }
+        }
+    } while (p);
+    return e;
+}
+
 dsimp_config::dsimp_config():
     m_md(transparency_mode::Reducible),
     m_max_steps(LEAN_DEFAULT_DSIMPLIFY_MAX_STEPS),
@@ -31,6 +65,10 @@ dsimp_config::dsimp_config():
     m_single_pass(false),
     m_fail_if_unchanged(true),
     m_eta(false),
+    m_zeta(false),
+    m_beta(true),
+    m_proj(true),
+    m_iota(true),
     m_memoize(true) {
 }
 dsimp_config::dsimp_config(vm_obj const & o) {
@@ -40,7 +78,11 @@ dsimp_config::dsimp_config(vm_obj const & o) {
     m_single_pass        = to_bool(cfield(o, 3));
     m_fail_if_unchanged  = to_bool(cfield(o, 4));
     m_eta                = to_bool(cfield(o, 5));
-    m_memoize            = to_bool(cfield(o, 6));
+    m_zeta               = to_bool(cfield(o, 6));
+    m_beta               = to_bool(cfield(o, 7));
+    m_proj               = to_bool(cfield(o, 8));
+    m_iota               = to_bool(cfield(o, 9));
+    m_memoize            = to_bool(cfield(o, 10));
 }
 
 #define lean_dsimp_trace(CTX, N, CODE) lean_trace(N, scope_trace_env _scope1(CTX.env(), CTX); CODE)
@@ -82,25 +124,29 @@ expr dsimplify_core_fn::visit_binding(expr const & e) {
 }
 
 expr dsimplify_core_fn::visit_let(expr const & e) {
-    type_context::tmp_locals locals(m_ctx);
-    expr b = e;
-    bool modified = false;
-    while (is_let(b)) {
-        expr t     = instantiate_rev(let_type(b), locals.size(), locals.data());
-        expr v     = instantiate_rev(let_value(b), locals.size(), locals.data());
-        expr new_t = visit(t);
-        expr new_v = visit(v);
-        if (!is_eqp(t, new_t) || !is_eqp(v, new_v)) modified = true;
-        locals.push_let(let_name(b), new_t, new_v);
-        b = let_body(b);
+    if (m_cfg.m_zeta) {
+        return visit(instantiate(let_body(e), let_value(e)));
+    } else {
+        type_context::tmp_locals locals(m_ctx);
+        expr b = e;
+        bool modified = false;
+        while (is_let(b)) {
+            expr t     = instantiate_rev(let_type(b), locals.size(), locals.data());
+            expr v     = instantiate_rev(let_value(b), locals.size(), locals.data());
+            expr new_t = visit(t);
+            expr new_v = visit(v);
+            if (!is_eqp(t, new_t) || !is_eqp(v, new_v)) modified = true;
+            locals.push_let(let_name(b), new_t, new_v);
+            b = let_body(b);
+        }
+        b = instantiate_rev(b, locals.size(), locals.data());
+        expr new_b = visit(b);
+        if (!is_eqp(b, new_b)) modified = true;
+        if (modified)
+            return locals.mk_lambda(new_b);
+        else
+            return e;
     }
-    b = instantiate_rev(b, locals.size(), locals.data());
-    expr new_b = visit(b);
-    if (!is_eqp(b, new_b)) modified = true;
-    if (modified)
-        return locals.mk_lambda(new_b);
-    else
-        return e;
 }
 
 expr dsimplify_core_fn::visit_app(expr const & e) {
@@ -232,18 +278,15 @@ metavar_context const & dsimplify_core_fn::mctx() const {
     return m_ctx.mctx();
 }
 
-expr dsimplify_fn::whnf(expr const & e) {
-    expr new_e = m_ctx.whnf(e);
-    if (m_cfg.m_eta)
-        new_e = try_eta(new_e);
-    return new_e;
+expr dsimplify_fn::reduce(expr const & e) {
+    return reduce_beta_eta_proj_iota(m_ctx, e, m_cfg.m_beta, m_cfg.m_eta, m_cfg.m_proj, m_cfg.m_iota);
 }
 
 optional<pair<expr, bool>> dsimplify_fn::pre(expr const & e) {
     type_context::transparency_scope s(m_ctx, m_cfg.m_md);
-    expr new_e = whnf(e);
+    expr new_e = reduce(e);
     if (new_e != e) {
-        lean_dsimp_trace(m_ctx, "dsimplify", tout() << "whnf\n" << e << "\n==>\n" << new_e << "\n";);
+        lean_dsimp_trace(m_ctx, "dsimplify", tout() << "reduce\n" << e << "\n==>\n" << new_e << "\n";);
         return optional<pair<expr, bool>>(new_e, true);
     } else {
         return optional<pair<expr, bool>>();
@@ -254,9 +297,9 @@ optional<pair<expr, bool>> dsimplify_fn::post(expr const & e) {
     expr curr_e;
     {
         type_context::transparency_scope s(m_ctx, m_cfg.m_md);
-        curr_e = whnf(e);
+        curr_e = reduce(e);
         if (curr_e != e) {
-            lean_dsimp_trace(m_ctx, "dsimplify", tout() << "whnf\n" << e << "\n==>\n" << curr_e << "\n";);
+            lean_dsimp_trace(m_ctx, "dsimplify", tout() << "reduce\n" << e << "\n==>\n" << curr_e << "\n";);
         }
     }
     while (true) {
diff --git a/src/library/tactic/dsimplify.h b/src/library/tactic/dsimplify.h
index 3457c050e9..750e8bd844 100644
--- a/src/library/tactic/dsimplify.h
+++ b/src/library/tactic/dsimplify.h
@@ -17,8 +17,12 @@ structure dsimp_config :=
 (canonize_instances : bool := tt)
 (canonize_proofs : bool    := ff)
 (single_pass : bool        := ff)
-(fail_if_unchaged          := tt)
-(eta                       := ff)
+(fail_if_unchaged : bool   := tt)
+(eta : bool                := ff)
+(zeta : bool               := ff)
+(beta : bool               := tt)
+(proj : bool               := tt) -- reduce projections
+(iota : bool               := tt)
 (memoize                   := tt)
 */
 struct dsimp_config {
@@ -28,6 +32,10 @@ struct dsimp_config {
     bool                      m_single_pass;
     bool                      m_fail_if_unchanged;
     bool                      m_eta;
+    bool                      m_zeta;
+    bool                      m_beta;
+    bool                      m_proj;
+    bool                      m_iota;
     bool                      m_memoize;
     dsimp_config();
     dsimp_config(vm_obj const & o);
@@ -61,7 +69,7 @@ public:
 
 class dsimplify_fn : public dsimplify_core_fn {
     simp_lemmas_for   m_simp_lemmas;
-    expr whnf(expr const & e);
+    expr reduce(expr const & e);
     virtual optional<pair<expr, bool>> pre(expr const & e) override;
     virtual optional<pair<expr, bool>> post(expr const & e) override;
 public:
@@ -69,6 +77,8 @@ public:
                  simp_lemmas_for const & lemmas, dsimp_config const & cfg);
 };
 
+expr reduce_beta_eta_proj_iota(type_context & ctx, expr e, bool beta, bool eta, bool proj, bool iota);
+
 void initialize_dsimplify();
 void finalize_dsimplify();
 }
diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp
index bd6816bae8..38ac324629 100644
--- a/src/library/tactic/simplify.cpp
+++ b/src/library/tactic/simplify.cpp
@@ -44,6 +44,7 @@ Author: Daniel Selsam, Leonardo de Moura
 #include "library/tactic/app_builder_tactics.h"
 #include "library/tactic/simp_lemmas.h"
 #include "library/tactic/simplify.h"
+#include "library/tactic/dsimplify.h"
 
 #ifndef LEAN_DEFAULT_SIMPLIFY_MAX_STEPS
 #define LEAN_DEFAULT_SIMPLIFY_MAX_STEPS 1000000
@@ -73,6 +74,7 @@ simp_config::simp_config():
     m_beta(false),
     m_eta(true),
     m_proj(true),
+    m_iota(true),
     m_single_pass(false),
     m_fail_if_unchanged(true),
     m_memoize(true) {
@@ -89,9 +91,10 @@ simp_config::simp_config(vm_obj const & obj) {
     m_beta               = to_bool(cfield(obj, 7));
     m_eta                = to_bool(cfield(obj, 8));
     m_proj               = to_bool(cfield(obj, 9));
-    m_single_pass        = to_bool(cfield(obj, 10));
-    m_fail_if_unchanged  = to_bool(cfield(obj, 11));
-    m_memoize            = to_bool(cfield(obj, 12));
+    m_iota               = to_bool(cfield(obj, 10));
+    m_single_pass        = to_bool(cfield(obj, 11));
+    m_fail_if_unchanged  = to_bool(cfield(obj, 12));
+    m_memoize            = to_bool(cfield(obj, 13));
 }
 
 /* -----------------------------------
@@ -736,31 +739,7 @@ simp_result simplify_core_fn::visit_fn(expr const & e) {
 }
 
 expr simplify_core_fn::reduce(expr e) {
-    bool p;
-    do {
-        p = false;
-        if (m_cfg.m_beta) {
-            expr new_e = head_beta_reduce(e);
-            if (!is_eqp(new_e, e)) {
-                e = new_e;
-                p = true;
-            }
-        }
-        if (m_cfg.m_proj) {
-            if (auto v = m_ctx.reduce_projection(e)) {
-                e = *v;
-                p = true;
-            }
-        }
-        if (m_cfg.m_eta) {
-            expr new_e = try_eta(e);
-            if (!is_eqp(new_e, e)) {
-                e = new_e;
-                p = true;
-            }
-        }
-    } while (p);
-    return e;
+    return reduce_beta_eta_proj_iota(m_ctx, e, m_cfg.m_beta, m_cfg.m_eta, m_cfg.m_proj, m_cfg.m_iota);
 }
 
 simp_result simplify_core_fn::reduce(simp_result r) {
diff --git a/src/library/tactic/simplify.h b/src/library/tactic/simplify.h
index 9f084b0b6e..5e284e4363 100644
--- a/src/library/tactic/simplify.h
+++ b/src/library/tactic/simplify.h
@@ -25,6 +25,7 @@ structure simp_config :=
 (beta : bool)
 (eta  : bool)
 (proj : bool)
+(iota : bool)
 (single_pass : bool)
 (fail_if_unchaged : bool)
 (memoize : bool)
@@ -40,6 +41,7 @@ struct simp_config {
     bool                      m_beta;
     bool                      m_eta;
     bool                      m_proj;
+    bool                      m_iota;
     bool                      m_single_pass;
     bool                      m_fail_if_unchanged;
     bool                      m_memoize;
diff --git a/src/library/tactic/unfold_tactic.cpp b/src/library/tactic/unfold_tactic.cpp
index 3322df72d4..1872ffee7b 100644
--- a/src/library/tactic/unfold_tactic.cpp
+++ b/src/library/tactic/unfold_tactic.cpp
@@ -96,6 +96,7 @@ public:
     unfold_core_fn(type_context & ctx, defeq_canonizer::state & dcs, list<name> const & cs, dsimp_config const & cfg):
         dsimplify_core_fn(ctx, dcs, cfg),
         m_cs(to_name_set(cs)) {
+        m_cfg.m_zeta = false;
     }
 };
 
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index b8c3026813..fb4b32d8a8 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -794,6 +794,16 @@ bool type_context::use_zeta() const {
     return m_zeta;
 }
 
+optional<expr> type_context::reduce_recursor(expr const & e) {
+    if (auto r = norm_ext(e))
+        return r;
+    if (auto r = reduce_aux_recursor(e))
+        return r;
+    if (auto r = reduce_large_elim_recursor(e))
+        return r;
+    return none_expr();
+}
+
 /*
   Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction,
   unfold macros, expand let-expressions, expand assigned meta-variables.
diff --git a/src/library/type_context.h b/src/library/type_context.h
index fa710c0b58..cb4b7274f8 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -406,6 +406,7 @@ public:
     optional<expr> reduce_large_elim_recursor(expr const & e);
     optional<expr> reduce_projection(expr const & e);
     optional<expr> norm_ext(expr const & e) { return env().norm_ext()(e, *this); }
+    optional<expr> reduce_recursor(expr const & e);
 
     /** Similar to whnf, but ignores transparency annotations, and use
         the given predicate to decide whether a constant should be unfolded or not.
diff --git a/tests/lean/1467.lean b/tests/lean/1467.lean
index d3be6badbe..0e0fd6abfa 100644
--- a/tests/lean/1467.lean
+++ b/tests/lean/1467.lean
@@ -4,7 +4,7 @@ axiom H_f_g : ∀ n, f (g n) = n
 example (m : ℕ) : h m = h m :=
 begin
 let n : ℕ := g m,
-have H : f n = m := begin dsimp, rw H_f_g end,
+have H : f n = m := begin rw H_f_g end,
 subst H, -- Error here
 end
 
@@ -14,14 +14,14 @@ example (m : ℕ) : h m = h m :=
 begin
 let n : ℕ, -- add metavar
 exact g m,
-have H : f n = m := begin dsimp, rw H_f_g end,
+have H : f n = m := begin rw H_f_g end,
 subst H, -- Error here
 end
 
 example (m : ℕ) : h m = h m :=
 begin
 let n : ℕ := g m,
-have H : f n = m := begin dsimp, rw H_f_g end,
+have H : f n = m := begin rw H_f_g end,
 subst m, -- Error here
 end
 
@@ -31,7 +31,7 @@ example (m : ℕ) : h m = h m :=
 begin
 let n : ℕ, -- add metavar
 exact g m,
-have H : f n = m := begin dsimp, rw H_f_g end,
+have H : f n = m := begin rw H_f_g end,
 subst m, -- Error here
 end
 
diff --git a/tests/lean/hinst_lemmas1.lean.expected.out b/tests/lean/hinst_lemmas1.lean.expected.out
index f70e085e03..fcda80ef2d 100644
--- a/tests/lean/hinst_lemmas1.lean.expected.out
+++ b/tests/lean/hinst_lemmas1.lean.expected.out
@@ -1,3 +1 @@
-{[foo1, patterns: {{?x_1 < ?x_2, ?x_0 < ?x_1}}],
- [foo2, patterns: {{?x_1 < ?x_2, ?x_1 > ?x_0}}],
- [foo3, patterns: {{?x_0 < ?x_1, ?x_1 < ?x_2 + ?x_2}}]}
+{[foo2, patterns: {{?x_1 < ?x_2, ?x_1 > ?x_0}}], [foo3, patterns: {{?x_1 > ?x_0, ?x_1 < ?x_2 + ?x_2}}]}
diff --git a/tests/lean/interactive/info_tactic.lean.expected.out b/tests/lean/interactive/info_tactic.lean.expected.out
index a8738b43ef..0db9b09f16 100644
--- a/tests/lean/interactive/info_tactic.lean.expected.out
+++ b/tests/lean/interactive/info_tactic.lean.expected.out
@@ -1,7 +1,7 @@
 {"msgs":[{"caption":"","file_name":"f","pos_col":2,"pos_line":5,"severity":"error","text":"simplify tactic failed to simplify\nstate:\n⊢ false"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n   The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n   This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n   but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"state":"⊢ false","tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":6}
-{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n   The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n   This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n   but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":0,"tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":8}
-{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n   The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n   This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n   but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":1,"tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":10}
-{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n   The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n   This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n   but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":2,"tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":12}
+{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n   The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n   This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n   but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"state":"⊢ false","tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":6}
+{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n   The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n   This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n   but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":0,"tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":8}
+{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n   The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n   This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n   but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":1,"tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":10}
+{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n   The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n   This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n   but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":2,"tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config_ext?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config_ext {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt}, discharger := failed unit} → tactic unit"},"response":"ok","seq_num":12}
 {"record":{"full-id":"tactic.get_env","source":,"tactic_params":[],"type":"tactic environment"},"response":"ok","seq_num":14}
diff --git a/tests/lean/run/dsimp_options.lean b/tests/lean/run/dsimp_options.lean
new file mode 100644
index 0000000000..d8e95dda44
--- /dev/null
+++ b/tests/lean/run/dsimp_options.lean
@@ -0,0 +1,80 @@
+example (b c : nat) : c = @bool.cases_on (λ _, nat) tt b c  :=
+begin
+  fail_if_success {dsimp {iota := ff}},
+  dsimp {iota := tt},
+  guard_target c = c,
+  reflexivity
+end
+
+example (b c : nat) : c = @bool.cases_on (λ _, nat) tt b c  :=
+begin
+  dsimp, -- iota is tt by default
+  guard_target c = c,
+  reflexivity
+end
+
+example (b c : nat) : c = (λ x : nat, x) c  :=
+begin
+  fail_if_success {dsimp {beta := ff}},
+  dsimp {beta := tt},
+  guard_target c = c,
+  reflexivity
+end
+
+example (b c : nat) : c = (λ x : nat, x) c  :=
+begin
+  dsimp, -- beta is tt by default
+  guard_target c = c,
+  reflexivity
+end
+
+example (b c : nat) : c = (b, c).2  :=
+begin
+  fail_if_success {dsimp {proj := ff}},
+  dsimp {proj := tt},
+  guard_target c = c,
+  reflexivity
+end
+
+example (b c : nat) : c = (b, c).2  :=
+begin
+  dsimp, -- projection reduction is true by default IF argument is a constructor
+  guard_target c = c,
+  reflexivity
+end
+
+example (f g : nat → nat) : f ∘ g = λ x, f (g x) :=
+begin
+  fail_if_success {dsimp}, -- reducible definition (e.g., function.comp) are not unfolded by default
+  dsimp [(∘)],
+  guard_target (λ x, f (g x)) = λ x, f (g x),
+  reflexivity
+end
+
+example (f g : nat → nat) : f ∘ g = λ x, f (g x) :=
+begin
+  dsimp [function.comp],
+  guard_target (λ x, f (g x)) = λ x, f (g x),
+  reflexivity
+end
+
+example (a : nat) : (let x := a in x) = a :=
+begin
+  fail_if_success{dsimp {zeta := ff}},
+  dsimp {zeta := tt},
+  guard_target a = a,
+  reflexivity
+end
+
+example (a : nat) : (let x := a in x) = a :=
+begin
+  dsimp, -- zeta is tt by default
+  guard_target a = a,
+  reflexivity
+end
+
+example (a b : nat) : a + b = b + a :=
+begin
+  fail_if_success{dsimp}, -- will not unfold has_add.add applications
+  apply add_comm
+end
diff --git a/tests/lean/run/u_eq_max_u_v.lean b/tests/lean/run/u_eq_max_u_v.lean
index 80bf5e1ca4..f24e42df5f 100644
--- a/tests/lean/run/u_eq_max_u_v.lean
+++ b/tests/lean/run/u_eq_max_u_v.lean
@@ -23,7 +23,7 @@ attribute [simp] semigroup_morphism.multiplicative
   ( f: semigroup_morphism s t ) ( g: semigroup_morphism t u ) : semigroup_morphism s u :=
 {
   map := λ x, g (f x),
-  multiplicative := begin blast, simp end
+  multiplicative := begin intros, simp [coe_fn] end
 }
 
 @[reducible] definition semigroup_product { α β : Type u } ( s : semigroup α ) ( t: semigroup β ) : semigroup (α × β) := {
@@ -45,7 +45,7 @@ definition semigroup_morphism_product
       -- cf https://groups.google.com/d/msg/lean-user/bVs5FdjClp4/tfHiVjLIBAAJ
       intros,
       unfold has_mul.mul,
-      dsimp,
+      dsimp [coe_fn],
       simp
     end
 }
diff --git a/tests/lean/run/using_smt1.lean b/tests/lean/run/using_smt1.lean
index b1414206c5..d66cfce35b 100644
--- a/tests/lean/run/using_smt1.lean
+++ b/tests/lean/run/using_smt1.lean
@@ -12,7 +12,7 @@ lemma ex3 (p q r : Prop) : p → q → ¬p → r :=
 by using_smt intros
 
 lemma ex4 (a b c : nat) : a > nat.zero → 0 < a :=
-by using_smt intros
+by simp [(>)]; using_smt intros
 
 lemma ex5 (a b c d : nat) : a ≠ d → a = b ∧ b = c → a = c :=
 by using_smt intros