feat: rename_bvar tactic (leanprover#342)

Co-authored-by: Jannis Limperg <jannis@limperg.de>

Mathlib.lean

@@ -102,6 +102,7 @@ import Mathlib.Tactic.PrintPrefix
 import Mathlib.Tactic.RCases
 import Mathlib.Tactic.Recover
 import Mathlib.Tactic.Rename
+import Mathlib.Tactic.RenameBVar
 import Mathlib.Tactic.Replace
 import Mathlib.Tactic.RestateAxiom
 import Mathlib.Tactic.Ring

Mathlib/Lean/Expr/Basic.lean

@@ -1,7 +1,8 @@
 /-
 Copyright (c) 2019 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Simon Hudon, Scott Morrison, Keeley Hoek, Robert Y. Lewis, Floris van Doorn, E.W.Ayers
+Authors: Mario Carneiro, Simon Hudon, Scott Morrison, Keeley Hoek, Robert Y. Lewis,
+Floris van Doorn, E.W.Ayers, Arthur Paulino
 -/
 import Lean
 
@@ -148,6 +149,16 @@ def modifyArgM [Monad M] (modifier : Expr → M Expr) (e : Expr) (i : Nat) (n :=
   let a ← modifier a
   return modifyArg (fun _ => a) e i n
 
+/-- Traverses an expression `e` and renames bound variables named `old` to `new`. -/
+def renameBVar (e : Expr) (old new : Name) : Expr :=
+  match e with
+  | app fn arg => app (fn.renameBVar old new) (arg.renameBVar old new)
+  | lam n ty bd bi =>
+    lam (if n == old then new else n) (ty.renameBVar old new) (bd.renameBVar old new) bi
+  | forallE n ty bd bi =>
+    forallE (if n == old then new else n) (ty.renameBVar old new) (bd.renameBVar old new) bi
+  | e => e
+
 end Expr
 
 end Lean

Mathlib/Mathport/Syntax.lean

@@ -336,8 +336,6 @@ syntax termList := " [" term,* "]"
 
 /- E -/ syntax (name := byContra') "by_contra'" (ppSpace ident)? Term.optType : tactic
 
-/- E -/ syntax (name := renameVar) "rename_var " ident " → " ident (ppSpace location)? : tactic
-
 /- M -/ syntax (name := assocRw) "assoc_rw " rwRuleSeq (ppSpace location)? : tactic
 
 /- N -/ syntax (name := dsimpResult) "dsimp_result " (&"only ")? ("[" Tactic.simpArg,* "]")?

Mathlib/Tactic/RenameBVar.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2019 Patrick Massot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Arthur Paulino, Patrick Massot
+-/
+
+import Lean
+import Mathlib.Util.Tactic
+
+namespace Mathlib.Tactic
+
+open Lean Meta Parser Elab Tactic
+
+/-- Renames a bound variable in a hypothesis. -/
+def renameBVarHyp (mvarId : MVarId) (fvarId : FVarId) (old new : Name) :
+    MetaM Unit :=
+  modifyLocalDecl mvarId fvarId fun ldecl =>
+    ldecl.setType $ ldecl.type.renameBVar old new
+
+/-- Renames a bound variable in the target. -/
+def renameBVarTarget (mvarId : MVarId) (old new : Name) : MetaM Unit :=
+  modifyTarget mvarId fun e => e.renameBVar old new
+
+/--
+* `rename_bvar old new` renames all bound variables named `old` to `new` in the target.
+* `rename_bvar old new at h` does the same in hypothesis `h`.
+
+```lean
+example (P : ℕ →  ℕ → Prop) (h : ∀ n, ∃ m, P n m) : ∀ l, ∃ m, P l m :=
+begin
+  rename_bvar n q at h, -- h is now ∀ (q : ℕ), ∃ (m : ℕ), P q m,
+  rename_bvar m n, -- target is now ∀ (l : ℕ), ∃ (n : ℕ), P k n,
+  exact h -- Lean does not care about those bound variable names
+end
+```
+Note: name clashes are resolved automatically.
+-/
+elab "rename_bvar " old:ident " → " new:ident loc?:(ppSpace location)? : tactic => do
+  let mvarId ← getMainGoal
+  match loc? with
+  | none => renameBVarTarget mvarId old.getId new.getId
+  | some loc =>
+    withLocation (expandLocation loc)
+      (fun fvarId => renameBVarHyp mvarId fvarId old.getId new.getId)
+      (renameBVarTarget mvarId old.getId new.getId)
+      fun _ => throwError "unexpected location syntax"

Mathlib/Tactic/SwapVar.lean

@@ -6,6 +6,8 @@ Authors: Arthur Paulino
 
 import Mathlib.Util.Tactic
 
+open Lean Meta Elab.Tactic
+
 namespace Mathlib.Tactic
 
 /-- The parser for swap rules -/
@@ -23,10 +25,18 @@ example {P Q : Prop} (q : P) (p : Q) : P ∧ Q := by
   exact ⟨p, q⟩
 ```
 -/
-elab "swap_var " vars:(colGt swapRule),+ : tactic =>
-  modifyLocalContext fun ctx =>
-    vars.getElems.foldlM (init := ctx) fun ctx stx => do
-      let `(swapRule| $n₁:ident $[↔]? $n₂:ident) := stx | unreachable!
-      let (n₁, fvarId₁) ← getNameAndFVarId ctx n₁
-      let (n₂, fvarId₂) ← getNameAndFVarId ctx n₂
-      pure $ ctx.setUserName fvarId₁ n₂ |>.setUserName fvarId₂ n₁
+elab "swap_var " swapRules:(colGt swapRule),+ : tactic => do
+  let mvarId ← getMainGoal
+  let mdecl ← getMVarDecl mvarId
+  let localInstances := mdecl.localInstances
+  let lctx ← swapRules.getElems.foldlM (init := mdecl.lctx) fun lctx swapRule => do
+    withLCtx lctx localInstances do
+      let `(swapRule| $n₁:ident $[↔]? $n₂:ident) := swapRule
+        | unreachable!
+      let n₁ := n₁.getId
+      let n₂ := n₂.getId
+      let fvarId₁ := (← getLocalDeclFromUserName n₁).fvarId
+      let fvarId₂ := (← getLocalDeclFromUserName n₂).fvarId
+      return lctx.setUserName fvarId₁ n₂ |>.setUserName fvarId₂ n₁
+  let mdecl := { mdecl with lctx := lctx }
+  modifyMCtx fun mctx => { mctx with decls := mctx.decls.insert mvarId mdecl }

Mathlib/Util/Tactic.lean

@@ -1,10 +1,10 @@
 /-
 Copyright (c) 2022 Arthur Paulino. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Arthur Paulino
+Authors: Arthur Paulino, Jannis Limperg
 -/
 
-import Lean
+import Mathlib.Lean.Expr.Basic
 
 /-!
 # Miscellaneous helper functions for tactics.
@@ -16,21 +16,59 @@ namespace Mathlib.Tactic
 
 open Lean Meta Elab Tactic
 
-/-- Finds the `Name` and the `FVarId` of a variable given a `LocalContext` and a `Syntax.ident`. -/
-def getNameAndFVarId [Monad m] [MonadError m] (ctx : LocalContext) (stx : Syntax) :
-    m (Name × FVarId) :=
-  if stx.isIdent then
-    let name := stx.getId
-    match ctx.findFromUserName? name with
-    | some decl => return (name, decl.fvarId)
-    | none => throwErrorAt stx "unknown variable {name}"
-  else
-    throwErrorAt stx "not an identifier"
-
-/-- Updates the current `LocalContext` with a transformation function in `MetaM`. -/
-def modifyLocalContext (fLCtx : LocalContext → MetaM LocalContext) : TacticM Unit :=
-  liftMetaTactic fun goal => do
-    let newGoal ← mkFreshExprMVarAt (← fLCtx (← getLCtx)) (← getLocalInstances)
-      (← goal.getType) .syntheticOpaque (← goal.getTag)
-    goal.assign newGoal
-    return [newGoal.mvarId!]
+variable [Monad m]
+
+/--
+`modifyMetavarDecl mvarId f` updates the `MetavarDecl` for `mvarId` with `f`.
+Conditions on `f`:
+
+- The target of `f mdecl` is defeq to the target of `mdecl`.
+- The local context of `f mdecl` must contain the same fvars as the local
+  context of `mdecl`. For each fvar in the local context of `f mdecl`, the type
+  (and value, if any) of the fvar must be defeq to the corresponding fvar in
+  the local context of `mdecl`.
+
+If `mvarId` does not refer to a declared metavariable, nothing happens.
+-/
+def modifyMetavarDecl [MonadMCtx m] (mvarId : MVarId)
+    (f : MetavarDecl → MetavarDecl) : m Unit := do
+  modifyMCtx λ mctx =>
+    match mctx.decls.find? mvarId with
+    | none => mctx
+    | some mdecl => { mctx with decls := mctx.decls.insert mvarId (f mdecl) }
+
+/--
+`modifyTarget mvarId f` updates the target of the metavariable `mvarId` with
+`f`. For any `e`, `f e` must be defeq to `e`. If `mvarId` does not refer to
+a declared metvariable, nothing happens.
+-/
+def modifyTarget [MonadMCtx m] (mvarId : MVarId) (f : Expr → Expr) : m Unit :=
+  modifyMetavarDecl mvarId fun mdecl =>
+    { mdecl with type := f mdecl.type }
+
+/--
+`modifyLocalContext mvarId f` updates the local context of the metavariable
+`mvarId` with `f`. The new local context must contain the same fvars as the old
+local context and the types (and values, if any) of the fvars in the new local
+context must be defeq to their equivalents in the old local context.
+
+If `mvarId` does not refer to a declared metavariable, nothing happens.
+-/
+def modifyLocalContext [MonadMCtx m] (mvarId : MVarId)
+    (f : LocalContext → LocalContext) : m Unit :=
+  modifyMetavarDecl mvarId fun mdecl =>
+    { mdecl with lctx := f mdecl.lctx }
+
+/--
+`modifyLocalDecl mvarId fvarId f` updates the local decl `fvarId` in the local
+context of `mvarId` with `f`. `f` must leave the `fvarId` and `index` of the
+`LocalDecl` unchanged. The type of the new `LocalDecl` must be defeq to the type
+of the old `LocalDecl` (and the same applies to the value of the `LocalDecl`, if
+any).
+
+If `mvarId` does not refer to a declared metavariable or if `fvarId` does not
+exist in the local context of `mvarId`, nothing happens.
+-/
+def modifyLocalDecl [MonadMCtx m] (mvarId : MVarId) (fvarId : FVarId)
+    (f : LocalDecl → LocalDecl) : m Unit :=
+  modifyLocalContext mvarId fun lctx => lctx.modifyLocalDecl fvarId f