feat(library/init/meta/converter): add support for dsimp parameters for conv mode

library/init/meta/converter/conv.lean

@@ -67,12 +67,13 @@ reflexivity
 meta def whnf : conv unit :=
 lhs >>= tactic.whnf >>= change
 
-meta def dsimp (s : option simp_lemmas := none) : conv unit :=
+meta def dsimp (s : option simp_lemmas := none) (cfg : dsimp_config := {}) : conv unit :=
 do s ← match s with
        | some s := return s
        | none   := simp_lemmas.mk_default
        end,
-   lhs >>= s.dsimplify >>= change
+   l ← lhs,
+   s.dsimplify l cfg >>= change
 
 private meta def congr_aux : list congr_arg_kind → list expr → tactic (list expr × list expr)
 | []      []      := return ([], [])

library/init/meta/converter/interactive.lean

@@ -39,8 +39,10 @@ conv.skip
 meta def whnf : conv unit :=
 conv.whnf
 
-meta def dsimp : conv unit :=
-conv.dsimp
+meta def dsimp (no_dflt : parse only_flag) (es : parse opt_qexpr_list) (attr_names : parse with_ident_list)
+               (ids : parse without_ident_list) (cfg : tactic.dsimp_config := {}) : conv unit :=
+do s ← tactic.mk_simp_set no_dflt attr_names es ids,
+   conv.dsimp (some s) cfg
 
 meta def trace_lhs : conv unit :=
 lhs >>= tactic.trace

tests/lean/run/conv_tac1.lean

@@ -82,3 +82,22 @@ begin
   conv { to_rhs, rw [h₁, -add_zero 0, -h₁], },
   exact h₂ x
 end
+
+lemma addz (x : nat) : x + 0 = x :=
+rfl
+
+example (x : nat) (g : nat → nat) (f : nat → (nat → nat) → nat) (h : f (x + 0) (λ x, g x) = x) : f x g = x :=
+begin
+  conv at h {dsimp [addz] {eta := ff}},
+  conv at h {dsimp},
+  exact h,
+end
+
+example (x : nat) (g : nat → nat) (f : nat → (nat → nat) → nat) (h : f (x + 0) (λ x, g x) = x) : f x g = x :=
+begin
+  conv at h {dsimp [addz] {eta := ff},
+             guard_lhs f x (λ x, g x) = x,
+             dsimp,
+             guard_lhs f x g = x},
+  exact h,
+end