From 6aba80d3890e95b869e0fb9754de27c2bd49a552 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@anu.edu.au>
Date: Sat, 29 Apr 2017 23:01:50 +1000
Subject: [PATCH] 
 feat(library/init/meta/simp_tactic,library/init/meta/interactive) interactive
 tactics for unfold_projection

---
 library/init/meta/interactive.lean | 11 +++++++++++
 library/init/meta/simp_tactic.lean | 17 +++++++++++++++++
 2 files changed, 28 insertions(+)

diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index f74fe62bcb..962b2d3c17 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -773,6 +773,17 @@ meta def delta : parse ident* → parse location → tactic unit
                           tactic.delta new_cs,
                           intron n
 
+private meta def unfold_projections_hyps : list name → tactic unit
+| []      := skip
+| (h::hs) := get_local h >>= unfold_projections_at >> unfold_projections_hyps hs
+
+/--
+This tactic unfolds all structure projections.
+-/
+meta def unfold_projections : parse location → tactic unit
+| [] := tactic.unfold_projections
+| hs := unfold_projections_hyps hs
+
 meta def apply_opt_param : tactic unit :=
 tactic.apply_opt_param
 
diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index cfc74c5233..3ad01cc9d7 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -177,6 +177,23 @@ do num_reverted ← revert h,
    unsafe_change $ expr.pi n bi new_d b,
    intron num_reverted
 
+meta def unfold_projections_core (m : transparency) (max_steps : nat) (e : expr) : tactic expr :=
+let unfold (changed : bool) (e : expr) : tactic (bool × expr × bool) := do
+  new_e ← unfold_projection_core m e,
+  return (tt, new_e, tt)
+in do (tt, new_e) ← dsimplify_core ff default_max_steps tt (λ c e, failed) unfold e | fail "no projections to unfold",
+      return new_e
+
+meta def unfold_projections : tactic unit :=
+target >>= unfold_projections_core semireducible default_max_steps >>= change
+
+meta def unfold_projections_at (h : expr) : tactic unit :=
+do num_reverted ← revert h,
+   (expr.pi n bi d b : expr) ← target,
+   new_d ← unfold_projections_core semireducible default_max_steps d,
+   change $ expr.pi n bi new_d b,
+   intron num_reverted
+
 structure simp_config :=
 (max_steps : nat           := default_max_steps)
 (contextual : bool         := ff)