merge master

src/Init/Tactics.lean

@@ -894,6 +894,37 @@ The tactic `nomatch h` is shorthand for `exact nomatch h`.
 macro "nomatch " es:term,+ : tactic =>
   `(tactic| exact nomatch $es:term,*)
 
+/--
+Acts like `have`, but removes a hypothesis with the same name as
+this one if possible. For example, if the state is:
+
+```lean
+f : α → β
+h : α
+⊢ goal
+```
+
+Then after `replace h := f h` the state will be:
+
+```lean
+f : α → β
+h : β
+⊢ goal
+```
+
+whereas `have h := f h` would result in:
+
+```lean
+f : α → β
+h† : α
+h : β
+⊢ goal
+```
+
+This can be used to simulate the `specialize` and `apply at` tactics of Coq.
+-/
+syntax (name := replace) "replace" haveDecl : tactic
+
 /--
 `repeat' tac` runs `tac` on all of the goals to produce a new list of goals,
 then runs `tac` again on all of those goals, and repeats until `tac` fails on all remaining goals.

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -12,6 +12,7 @@ import Lean.Elab.Open
 import Lean.Elab.SetOption
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.ElabTerm
+import Lean.Elab.Do
 
 namespace Lean.Elab.Tactic
 open Meta
@@ -481,4 +482,18 @@ where
 @[builtin_tactic right] def evalRight : Tactic := fun _stx => do
   liftMetaTactic (fun g => g.nthConstructor `right 1 (some 2))
 
+@[builtin_tactic replace] def evalReplace : Tactic := fun stx => do
+  match stx with
+  | `(tactic| replace $decl:haveDecl) =>
+    withMainContext do
+      let vars ← Elab.Term.Do.getDoHaveVars <| mkNullNode #[.missing, decl]
+      let origLCtx ← getLCtx
+      evalTactic $ ← `(tactic| have $decl:haveDecl)
+      let mut toClear := #[]
+      for fv in vars do
+        if let some ldecl := origLCtx.findFromUserName? fv.getId then
+          toClear := toClear.push ldecl.fvarId
+      liftMetaTactic1 (·.tryClearMany toClear)
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Tactic

tests/lean/run/replace_tac.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2022 Arthur Paulino. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Arthur Paulino
+-/
+
+example (h : Int) : Nat := by
+  replace h : Nat := 0
+  exact h
+
+example (h : Nat) : Nat := by
+  have h : Int := 0
+  assumption -- original `h` is not absent but...
+
+example (h : Nat) : Nat := by
+  replace h : Int := 0
+  fail_if_success assumption -- original `h` is absent now
+  replace h : Nat := 0
+  exact h
+
+-- tests with `this`
+
+example : Nat := by
+  have : Int := 0
+  replace : Nat := 0
+  assumption
+
+example : Nat := by
+  have : Nat := 0
+  have : Int := 0
+  assumption -- original `this` is not absent but...
+
+example : Nat := by
+  have : Nat := 0
+  replace : Int := 0
+  fail_if_success assumption -- original `this` is absent now
+  replace : Nat := 0
+  assumption
+
+-- trying to replace the type of a variable when the goal depends on it
+
+example {a : Nat} : a = a := by
+  replace a : Int := 0
+  have : Nat := by assumption -- old `a` is not gone
+  have : Int := by exact a    -- new `a` is of type `Int`
+  simp