refactor(library/init/meta/simp_tactic): tactic.simp_at => tactic.simp_hyp

doc/changes.md

@@ -88,6 +88,9 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
 * `tactic.unfold_projections` => `tactic.unfold_projs_target`
 * `tactic.unfold_projections_at` => `tactic.unfold_projs_hyp`
 * `tactic.simp_intros_using`, `tactic.simph_intros_using`, `tactic.simp_intro_lst_using`, `tactic.simph_intro_lst_using` => `tactic.simp_intros`
+* `tactic.simp_at` => `tactic.simp_hyp`
+* deleted `tactic.simp_at_using`
+* deleted `tactic.simph_at`
 
 v3.2.0 (18 June 2017)
 -------------

library/init/meta/interactive.lean

@@ -709,20 +709,9 @@ end mk_simp_set
 namespace interactive
 open interactive interactive.types expr
 
-private meta def simp_goal (cfg : simp_config) (discharger : tactic unit) (s : simp_lemmas) (u : list name) : tactic unit :=
-do (new_target, pr) ← target >>= λ t, simplify s u t cfg `eq discharger,
-   replace_target new_target pr
-
-private meta def simp_hyp (cfg : simp_config) (discharger : tactic unit) (s : simp_lemmas) (u : list name) (h_name : name) : tactic unit :=
-do h      ← get_local h_name,
-   h_type ← infer_type h,
-   (h_new_type, pr) ← simplify s u h_type cfg `eq discharger,
-   replace_hyp h h_new_type pr,
-   return ()
-
 private meta def simp_hyps (cfg : simp_config) (discharger : tactic unit) (s : simp_lemmas) (u : list name) : list name → tactic unit
 | []      := skip
-| (h::hs) := simp_hyp cfg discharger s u h >> simp_hyps hs
+| (h::hs) := do h ← get_local h, simp_hyp s u h cfg discharger, simp_hyps hs
 
 meta def simp_core (cfg : simp_config) (discharger : tactic unit)
                    (no_dflt : bool) (ctx : list expr) (hs : list pexpr) (attr_names : list name) (ids : list name)
@@ -739,11 +728,11 @@ do (s, u) ← mk_simp_set no_dflt attr_names hs ids,
                 mk_eq_mp pr h >>= tactic.exact >> return tt)
             <|>
             (return ff) },
-        goal_simplified ← (simp_goal cfg discharger s u >> return tt) <|> (return ff),
+        goal_simplified ← (simp_target s u cfg discharger >> return tt) <|> (return ff),
         guard (cfg.fail_if_unchanged = ff ∨ to_remove.length > 0 ∨ goal_simplified) <|> fail "simplify tactic failed to simplify",
         to_remove.mfor' (λ h, try (clear h)),
         return ()
-   | (loc.ns []) := simp_goal cfg discharger s u
+   | (loc.ns []) := simp_target s u cfg discharger
    | (loc.ns hs) := simp_hyps cfg discharger s u hs
    end,
    try tactic.triv, try (tactic.reflexivity reducible)

library/init/meta/simp_tactic.lean

@@ -215,14 +215,20 @@ structure simp_config :=
    The parameter `to_unfold` specifies definitions that should be delta-reduced,
    and projection applications that should be unfolded.
 -/
-meta constant simplify (s : simp_lemmas) (to_unfold : list name) (e : expr) (cfg : simp_config := {}) (r : name := `eq)
+meta constant simplify (s : simp_lemmas) (to_unfold : list name := []) (e : expr) (cfg : simp_config := {}) (r : name := `eq)
                        (discharger : tactic unit := failed) : tactic (expr × expr)
 
-meta def simp_target (S : simp_lemmas) (to_unfold : list name := []) (cfg : simp_config := {}) (discharger : tactic unit := failed) : tactic unit :=
+meta def simp_target (s : simp_lemmas) (to_unfold : list name := []) (cfg : simp_config := {}) (discharger : tactic unit := failed) : tactic unit :=
 do t ← target,
-   (new_t, pr) ← simplify S to_unfold t cfg `eq discharger,
+   (new_t, pr) ← simplify s to_unfold t cfg `eq discharger,
    replace_target new_t pr
 
+meta def simp_hyp (s : simp_lemmas) (to_unfold : list name := []) (h : expr) (cfg : simp_config := {}) (discharger : tactic unit := failed) : tactic expr :=
+do when (expr.is_local_constant h = ff) (fail "tactic simp_at failed, the given expression is not a hypothesis"),
+   htype ← infer_type h,
+   (h_new_type, pr) ← simplify s to_unfold htype cfg `eq discharger,
+   replace_hyp h h_new_type pr
+
 meta constant ext_simplify_core
   /- The user state type. -/
   {α : Type}
@@ -319,21 +325,6 @@ step $ simp_intros_aux cfg.to_simp_config cfg.use_hyps to_unfold s (bnot ids.emp
 
 end simp_intros
 
-meta def simp_at (h : expr) (extra_lemmas : list expr := []) (cfg : simp_config := {}) : tactic expr :=
-do when (expr.is_local_constant h = ff) (fail "tactic simp_at failed, the given expression is not a hypothesis"),
-   htype ← infer_type h,
-   S     ← simp_lemmas.mk_default,
-   S     ← S.append extra_lemmas,
-   (h_new_type, pr) ← simplify S [] htype cfg,
-   replace_hyp h h_new_type pr
-
-meta def simp_at_using_hs (h : expr) (extra_lemmas : list expr := []) (cfg : simp_config := {}) : tactic expr :=
-do hs ← collect_ctx_simps,
-   simp_at h (list.filter (≠ h) hs ++ extra_lemmas) cfg
-
-meta def simph_at (h : expr) (extra_lemmas : list expr := []) (cfg : simp_config := {}) : tactic expr :=
-simp_at_using_hs h extra_lemmas cfg
-
 meta def mk_eq_simp_ext (simp_ext : expr → tactic (expr × expr)) : tactic unit :=
 do (lhs, rhs)     ← target >>= match_eq,
    (new_rhs, heq) ← simp_ext lhs,