From b1c1d2dfa409e2d279ce3e709826ec0f01649c2a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 9 Jan 2017 17:31:12 -0800
Subject: [PATCH] feat(library/init/meta): improve dsimp tactic notation

---
 library/init/meta/interactive.lean | 10 ++--
 library/init/meta/simp_tactic.lean | 16 +++---
 tests/lean/run/dsimp_test.lean     | 82 ++++++++++++++++++++++++++++++
 3 files changed, 97 insertions(+), 11 deletions(-)
 create mode 100644 tests/lean/run/dsimp_test.lean

diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 7bfa098b60..1dc15384de 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -391,13 +391,13 @@ meta def simp_using_hs (hs : opt_qexpr_list) (attr_names : with_ident_list) (ids
 do ctx ← collect_ctx_simps,
    simp_core default_simplify_config ctx hs attr_names ids []
 
-private meta def dsimp_hyps : location → tactic unit
+private meta def dsimp_hyps (s : simp_lemmas) : location → tactic unit
 | []      := skip
-| (h::hs) := get_local h >>= dsimp_at
+| (h::hs) := get_local h >>= dsimp_at_core s
 
-meta def dsimp : location → tactic unit
-| [] := tactic.dsimp
-| hs := dsimp_hyps hs
+meta def dsimp (es : opt_qexpr_list) (attr_names : with_ident_list) (ids : without_ident_list) : location → tactic unit
+| [] := do s ← mk_simp_set attr_names es ids, tactic.dsimp_core s
+| hs := do s ← mk_simp_set attr_names es ids, dsimp_hyps s hs
 
 meta def reflexivity : tactic unit :=
 tactic.reflexivity
diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index 6b08578ef5..69a3efae22 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -224,18 +224,22 @@ simplify_goal default_simplify_config hs >> try triv
 meta def ctx_simp : tactic unit :=
 simplify_goal {default_simplify_config with contextual := tt} [] >> try triv >> try (reflexivity_core reducible)
 
-meta def dsimp : tactic unit :=
-do S ← simp_lemmas.mk_default,
-   target >>= S^.dsimplify >>= change
+meta def dsimp_core (s : simp_lemmas) : tactic unit :=
+target >>= s^.dsimplify >>= change
 
-meta def dsimp_at (h : expr) : tactic unit :=
+meta def dsimp : tactic unit :=
+simp_lemmas.mk_default >>= dsimp_core
+
+meta def dsimp_at_core (s : simp_lemmas) (h : expr) : tactic unit :=
 do num_reverted : ℕ ← revert h,
    (expr.pi n bi d b : expr) ← target | failed,
-   S      ← simp_lemmas.mk_default,
-   h_simp ← S^.dsimplify d,
+   h_simp ← s^.dsimplify d,
    change $ expr.pi n bi h_simp b,
    intron num_reverted
 
+meta def dsimp_at (h : expr) : tactic unit :=
+do s ← simp_lemmas.mk_default, dsimp_at_core s h
+
 private meta def is_equation : expr → bool
 | (expr.pi n bi d b) := is_equation b
 | e                  := match (expr.is_eq e) with (some a) := tt | none := ff end
diff --git a/tests/lean/run/dsimp_test.lean b/tests/lean/run/dsimp_test.lean
new file mode 100644
index 0000000000..6e6e51c56f
--- /dev/null
+++ b/tests/lean/run/dsimp_test.lean
@@ -0,0 +1,82 @@
+def f : nat → nat
+| 0     := 10
+| (n+1) := 20 + n
+
+open list tactic
+
+meta def check_expr (p : pexpr) (t : expr) : tactic unit :=
+do e ← to_expr p, guard (t = e)
+
+meta def check_target (p : pexpr) : tactic unit :=
+do t ← target, check_expr p t
+
+example (a b c : nat) : head (map f [1, 2, 3]) = 20 :=
+begin
+  dsimp [map],
+  check_target `(head [f 1, f 2, f 3] = 20),
+  dsimp [f],
+  check_target `(head [20 + 0, 20 + 1,  20 + 2] = 20),
+  dsimp [head],
+  check_target `(20 + 0 = 20),
+  reflexivity
+end
+
+example (a b c : nat) : head (map f [1, 2, 3]) = 20 :=
+begin
+  dsimp [map, f, head],
+  check_target `(20 + 0 = 20),
+  reflexivity
+end
+
+@[simp] lemma succ_zero_eq_one : nat.succ 0 = 1 :=
+rfl
+
+def g : nat × nat → nat
+| (a, b) := a + b
+
+lemma gax (x y) : g (x, y) = x + y :=
+rfl
+
+attribute [simp] gax
+
+example (a b c : nat) : g (f 1, f 2) = 41 :=
+begin
+  dsimp,
+  check_target `(f 1 + f 2 = 41),
+  dsimp [f],
+  reflexivity
+end
+
+example (a b c : nat) : g (f 1, f 2) = 41 :=
+begin
+  dsimp [f],
+  check_target `(20 + 0 + (20 + 1) = 41),
+  reflexivity
+end
+
+example (a b c : nat) : g (f 1, f 2) = 41 :=
+begin
+  dsimp [f] without gax,
+  check_target `(g (20 + 0, 20 + 1) = 41),
+  dsimp [g],
+  check_target `(20 + 0 + (20 + 1) = 41),
+  reflexivity
+end
+
+local attribute [-simp] gax
+
+example (a b c : nat) : g (f 1, f 2) = 41 :=
+begin
+  dsimp [f],
+  check_target `(g (20 + 0, 20 + 1) = 41),
+  dsimp [gax],
+  check_target `(20 + 0 + (20 + 1) = 41),
+  reflexivity
+end
+
+example (a b c : nat) : g (f 1, f 2) = 41 :=
+begin
+  dsimp [f, gax],
+  check_target `(20 + 0 + (20 + 1) = 41),
+  reflexivity
+end