feat(library/init/meta/interactive): add show_goal tactic for structuring proofs in interactive tactic mode

library/init/meta/interactive.lean

@@ -853,5 +853,16 @@ tactic.by_contradiction >> return ()
 meta def done : tactic unit :=
 tactic.done
 
+private meta def show_goal_aux (p : pexpr) : list expr → list expr → tactic unit
+| []      r := fail "show_goal tactic failed"
+| (g::gs) r := do
+  do {set_goals [g], g_ty ← target, ty ← i_to_expr_strict p, is_def_eq g_ty ty >> set_goals (g :: r.reverse ++ gs) }
+  <|>
+  show_goal_aux gs (g::r)
+
+meta def show_goal (q : parse texpr) : tactic unit :=
+do gs ← get_goals,
+   show_goal_aux q gs []
+
 end interactive
 end tactic

tests/lean/run/show_goal.lean

@@ -0,0 +1,9 @@
+open tactic
+
+lemma ex (a b c : nat) : a + 0 = 0 + a ∧ 0 + b = b ∧ c + b = b + c :=
+begin
+  repeat {any_goals {constructor}},
+  show_goal c + b = b + c, { apply add_comm },
+  show_goal a + 0 = 0 + a, { simp },
+  show_goal 0 + b = b,     { rw [zero_add] }
+end