feat(tactic/rename): Add improved renaming tactic (#1916)

* feat(tactic/rename): Add improved renaming tactic

We add a tactic `rename'` which works like `rename`, with the following
improvements:

* Multiple hypotheses can be renamed at once.
* Renaming always preserve the position of a hypothesis in the context.

* Move private def `drop_until_inclusive` to `list.after`

* Change `rename'` docs to rely less on knowledge of `rename`

* Improve formatting of list.after docs

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

docs/tactics.md

@@ -1390,7 +1390,7 @@ An improved version of the standard `clear` tactic. `clear` is sensitive to the
 order of its arguments: `clear x y` may fail even though both `x` and `y` could
 be cleared (if the type of `y` depends on `x`). `clear'` lifts this limitation.
 
-```
+```lean
 example {α} {β : α → Type} (a : α) (b : β a) : unit :=
 begin
   try { clear a b }, -- fails since `b` depends on `a`
@@ -1404,7 +1404,7 @@ end
 A variant of `clear'` which clears not only the given hypotheses, but also any
 other hypotheses depending on them.
 
-```
+```lean
 example {α} {β : α → Type} (a : α) (b : β a) : unit :=
 begin
   try { clear' a },  -- fails since `b` depends on `a`
@@ -1433,3 +1433,25 @@ by simp_rw [set.image_subset_iff, set.subset_def]
 ```
 
 Lemmas passed to `simp_rw` must be expressions that are valid arguments to `simp`.
+
+## rename'
+
+Renames one or more hypotheses in the context.
+
+```lean
+example {α β} (a : α) (b : β) : unit :=
+begin
+  rename' a a',              -- result: a' : α, b  : β
+  rename' a' → a,            --         a  : α, b  : β
+  rename' [a a', b b'],      --         a' : α, b' : β
+  rename' [a' → a, b' → b],  --         a  : α, b  : β
+  exact ()
+end
+```
+
+Compared to the standard `rename` tactic, this tactic makes the following
+improvements:
+
+- You can rename multiple hypotheses at once.
+- Renaming a hypothesis always preserves its location in the context (whereas
+  `rename` may reorder hypotheses).

src/data/list/defs.lean

@@ -101,6 +101,18 @@ def take_while (p : α → Prop) [decidable_pred p] : list α → list α
 | []     := []
 | (a::l) := if p a then a :: take_while l else []
 
+/-- `after p xs` is the suffix of `xs` after the first element that satisfies
+  `p`, not including that element.
+
+  ```lean
+  after      (eq 1)       [0, 1, 2, 3] = [2, 3]
+  drop_while (not ∘ eq 1) [0, 1, 2, 3] = [1, 2, 3]
+  ```
+-/
+def after (p : α → Prop) [decidable_pred p] : list α → list α
+| [] := []
+| (x :: xs) := if p x then xs else after xs
+
 /-- Fold a function `f` over the list from the left, returning the list
   of partial results.
 

src/tactic/basic.lean

@@ -13,6 +13,7 @@ import
   tactic.mk_iff_of_inductive_prop
   tactic.push_neg
   tactic.rcases
+  tactic.rename
   tactic.replacer
   tactic.restate_axiom
   tactic.rewrite

src/tactic/rename.lean

@@ -0,0 +1,106 @@
+/-
+Copyright (c) 2020 Jannis Limperg. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Jannis Limperg
+-/
+import tactic.core
+
+
+/-!
+# Better `rename` tactic
+
+This module defines a variant of the standard `rename` tactic, with the
+following improvements:
+
+* You can rename multiple hypotheses at the same time.
+* Renaming a hypothesis does not change its location in the context.
+-/
+
+
+open lean lean.parser interactive native
+
+
+namespace tactic
+
+/-- Get the revertible part of the local context. These are the hypotheses that
+appear after the last frozen local instance in the local context. We call them
+revertible because `revert` can revert them, unlike those hypotheses which occur
+before a frozen instance. -/
+meta def revertible_local_context : tactic (list expr) := do
+  ctx ← local_context,
+  frozen ← frozen_local_instances,
+  pure $
+    match frozen with
+    | none := ctx
+    | some [] := ctx
+    | some (h :: _) := ctx.after (eq h)
+    end
+
+/-- Rename local hypotheses according to the given `name_map`. The `name_map`
+contains as keys those hypotheses that should be renamed; the associated values
+are the new names.
+
+This tactic can only rename hypotheses which occur after the last frozen local
+instance. If you need to rename earlier hypotheses, try
+`unfreeze_local_instances`.
+
+If `strict` is true, we fail if `name_map` refers to hypotheses that do not
+appear in the local context or that appear before a frozen local instance.
+Conversely, if `strict` is false, some entries of `name_map` may be silently
+ignored.
+
+Note that we allow shadowing, so renamed hypotheses may have the same name
+as other hypotheses in the context.
+-/
+meta def rename' (renames : name_map name) (strict := tt) : tactic unit := do
+  ctx ← revertible_local_context,
+  when strict (do
+    let ctx_names := rb_map.set_of_list (ctx.map expr.local_pp_name),
+    let invalid_renames :=
+      (renames.to_list.map prod.fst).filter (λ h, ¬ ctx_names.contains h),
+    when ¬ invalid_renames.empty $ fail $ format.join
+      [ "Cannot rename these hypotheses:\n"
+      , format.intercalate ", " (invalid_renames.map to_fmt)
+      , format.line
+      , "This is because these hypotheses either do not occur in the\n"
+      , "context or they occur before a frozen local instance.\n"
+      , "In the latter case, try `tactic.unfreeze_local_instances`."
+      ]),
+  let new_name := λ current_name,
+    (renames.find current_name).get_or_else current_name,
+  let intro_names := list.map (new_name ∘ expr.local_pp_name) ctx,
+  revert_lst ctx,
+  intro_lst intro_names,
+  pure ()
+
+end tactic
+
+
+namespace tactic.interactive
+
+/-- Parse a current name and new name for `rename'`. -/
+meta def rename'_arg_parser : parser (name × name) :=
+  prod.mk <$> ident <*> (optional (tk "->") *> ident)
+
+/-- Parse the arguments of `rename'`. -/
+meta def rename'_args_parser : parser (list (name × name)) :=
+  (functor.map (λ x, [x]) rename'_arg_parser)
+  <|>
+  (tk "[" *> sep_by (tk ",") rename'_arg_parser <* tk "]")
+
+/--
+Rename one or more local hypotheses. The renamings are given as follows:
+
+```
+rename' x y             -- rename x to y
+rename' x → y           -- ditto
+rename' [x y, a b]      -- rename x to y and a to b
+rename' [x → y, a → b]  -- ditto
+```
+
+Brackets are necessary if multiple hypotheses should be renamed in parallel.
+-/
+meta def rename' (renames : parse rename'_args_parser) : tactic unit :=
+  tactic.rename' (rb_map.of_list renames)
+
+end tactic.interactive

test/tactics.lean

@@ -500,3 +500,33 @@ section simp_rw
     (∀ s, f '' s ⊆ t) = ∀ s : set α, ∀ x ∈ s, x ∈ f ⁻¹' t :=
   by simp_rw [set.image_subset_iff, set.subset_def]
 end simp_rw
+
+section rename'
+
+example {α β} (a : α) (b : β) : unit :=
+begin
+  rename' a a',              -- rename-compatible syntax
+  guard_hyp a' := α,
+
+  rename' a' → a,            -- more suggestive syntax
+  guard_hyp a := α,
+
+  rename' [a a', b b'],      -- parallel renaming
+  guard_hyp a' := α,
+  guard_hyp b' := β,
+
+  rename' [a' → a, b' → b],  -- ditto with alternative syntax
+  guard_hyp a := α,
+  guard_hyp b := β,
+
+  rename' [a → b, b → a],    -- renaming really is parallel
+  guard_hyp a := β,
+  guard_hyp b := α,
+
+  rename' b a,               -- shadowing is allowed (but guard_hyp doesn't like it)
+
+  success_if_fail { rename' d e }, -- cannot rename nonexistent hypothesis
+  exact ()
+end
+
+end rename'