CI stalled, bumping

Update src/Lean/Meta/Tactic/Replace.lean

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

Update src/Lean/Meta/Tactic/Replace.lean

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

Update src/Lean/Elab/Tactic/Change.lean

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

Update src/Lean/Meta/Tactic/Replace.lean

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

Update src/Lean/Meta/Tactic/Replace.lean

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

src/Lean/Elab/Tactic.lean

@@ -25,3 +25,4 @@ import Lean.Elab.Tactic.Calc
 import Lean.Elab.Tactic.Congr
 import Lean.Elab.Tactic.Guard
 import Lean.Elab.Tactic.RCases
+import Lean.Elab.Tactic.Change

src/Lean/Elab/Tactic/Change.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+import Lean.Meta.Tactic.Replace
+import Lean.Elab.Tactic.Location
+
+namespace Lean.Elab.Tactic
+open Meta
+/-!
+# Implementation of the `change` tactic
+-/
+
+/-- `change` can be used to replace the main goal or its hypotheses with
+different, yet definitionally equal, goal or hypotheses.
+
+For example, if `n : Nat` and the current goal is `⊢ n + 2 = 2`, then
+```lean
+change _ + 1 = _
+```
+changes the goal to `⊢ n + 1 + 1 = 2`.
+
+The tactic also applies to hypotheses. If `h : n + 2 = 2` and `h' : n + 3 = 4`
+are hypotheses, then
+```lean
+change _ + 1 = _ at h h'
+```
+changes their types to be `h : n + 1 + 1 = 2` and `h' : n + 2 + 1 = 4`.
+
+Change is like `refine` in that every placeholder needs to be solved for by unification,
+but using named placeholders or `?_` results in `change` to creating new goals.
+
+The tactic `show e` is interchangeable with `change e`, where the pattern `e` is applied to
+the main goal. -/
+@[builtin_tactic change] elab_rules : tactic
+  | `(tactic| change $newType:term $[$loc:location]?) => do
+    withLocation (expandOptLocation (Lean.mkOptionalNode loc))
+      (atLocal := fun h => do
+        let hTy ← h.getType
+        -- This is a hack to get the new type to elaborate in the same sort of way that
+        -- it would for a `show` expression for the goal.
+        let mvar ← mkFreshExprMVar none
+        let (_, mvars) ← elabTermWithHoles
+                          (← `(term | show $newType from $(← Term.exprToSyntax mvar))) hTy `change
+        liftMetaTactic fun mvarId => do
+          return (← mvarId.changeLocalDecl h (← inferType mvar)) :: mvars)
+      (atTarget := evalTactic <| ← `(tactic| refine_lift show $newType from ?_))
+      (failed := fun _ => throwError "change tactic failed")
+
+end Lean.Elab.Tactic

src/Lean/Meta/Tactic/Replace.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Util.ForEachExpr
+import Lean.Elab.InfoTree.Main
 import Lean.Meta.AppBuilder
 import Lean.Meta.MatchUtil
 import Lean.Meta.Tactic.Util
@@ -139,29 +140,54 @@ def _root_.Lean.MVarId.change (mvarId : MVarId) (targetNew : Expr) (checkDefEq :
 def change (mvarId : MVarId) (targetNew : Expr) (checkDefEq := true) : MetaM MVarId := mvarId.withContext do
   mvarId.change targetNew checkDefEq
 
-/--
-Replace the type of the free variable `fvarId` with `typeNew`.
-If `checkDefEq = false`, this method assumes that `typeNew` is definitionally equal to `fvarId` type.
-If `checkDefEq = true`, throw an error if `typeNew` is not definitionally equal to `fvarId` type.
--/
-def _root_.Lean.MVarId.changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkDefEq := true) : MetaM MVarId := do
-  mvarId.checkNotAssigned `changeLocalDecl
-  let (xs, mvarId) ← mvarId.revert #[fvarId] true
+/-- Runs the continuation `k` after temporarily reverting some variables from the local context of a metavariable (identified by `mvarId`), then reintroduces local variables as specified by `k`.
+
+The argument `fvarIds` is an array of `fvarIds` to revert in the order specified. An error is thrown if they cannot be reverted in order.
+
+Once the local variables have been reverted, `k` is passed `mvarId` along with an array of local variables that were reverted. This array always has `fvarIds` as a prefix, but it may contain additional variables that were reverted due to dependencies. `k` returns a value, a goal, an array of _link variables_.
+
+Once `k` has completed, one variable is introduced for each link variable returned by `k`. If the returned variable is `none`, the variable is just introduced. If it is `some fv`, the variable is introduced and then linked as an alias of `fv` in the info tree. For example, having `k` return `fvars.map .some` as the link variables causes all reverted variables to be introduced and linked.
+
+Returns the value returned by `k` along with the resulting goal.
+ -/
+def _root_.Lean.MVarId.withReverted (mvarId : MVarId) (fvarIds : Array FVarId)
+    (k : MVarId → Array FVarId → MetaM (α × Array (Option FVarId) × MVarId))
+    (clearAuxDeclsInsteadOfRevert := false) : MetaM (α × MVarId) := do
+  let (xs, mvarId) ← mvarId.revert fvarIds true clearAuxDeclsInsteadOfRevert
+  let (r, xs', mvarId) ← k mvarId xs
+  let (ys, mvarId) ← mvarId.introNP xs'.size
   mvarId.withContext do
-    let numReverted := xs.size
-    let target ← mvarId.getType
+    for x? in xs', y in ys do
+      if let some x := x? then
+        Elab.pushInfoLeaf (.ofFVarAliasInfo { id := y, baseId := x, userName := ← y.getUserName })
+  return (r, mvarId)
+
+/--
+Replaces the type of the free variable `fvarId` with `typeNew`.
+
+If `checkDefEq` is `true` then an error is thrown if `typeNew` is not definitionally
+equal to the type of `fvarId`. Otherwise this function assumes `typeNew` and the type
+of `fvarId` are definitionally equal.
+
+This function is the same as `Lean.MVarId.changeLocalDecl` but makes sure to push substitution
+information into the info tree.
+-/
+def _root_.Lean.MVarId.changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr)
+    (checkDefEq := true) : MetaM MVarId := do
+  mvarId.checkNotAssigned `changeLocalDecl
+  let (_, mvarId) ← mvarId.withReverted #[fvarId] fun mvarId fvars => mvarId.withContext do
     let check (typeOld : Expr) : MetaM Unit := do
       if checkDefEq then
-        unless (← isDefEq typeNew typeOld) do
-          throwTacticEx `changeHypothesis mvarId m!"given type{indentExpr typeNew}\nis not definitionally equal to{indentExpr typeOld}"
-    let finalize (targetNew : Expr) : MetaM MVarId := do
-      let mvarId ← mvarId.replaceTargetDefEq targetNew
-      let (_, mvarId) ← mvarId.introNP numReverted
-      pure mvarId
-    match target with
-    | .forallE n d b c => do check d; finalize (mkForall n c typeNew b)
-    | .letE n t v b _  => do check t; finalize (mkLet n typeNew v b)
-    | _ => throwTacticEx `changeHypothesis mvarId "unexpected auxiliary target"
+        unless ← isDefEq typeNew typeOld do
+          throwTacticEx `changeLocalDecl mvarId
+            m!"given type{indentExpr typeNew}\nis not definitionally equal to{indentExpr typeOld}"
+    let finalize (targetNew : Expr) := do
+      return ((), fvars.map .some, ← mvarId.replaceTargetDefEq targetNew)
+    match ← mvarId.getType with
+    | .forallE n d b bi => do check d; finalize (.forallE n typeNew b bi)
+    | .letE n t v b ndep => do check t; finalize (.letE n typeNew v b ndep)
+    | _ => throwTacticEx `changeLocalDecl mvarId "unexpected auxiliary target"
+  return mvarId
 
 @[deprecated MVarId.changeLocalDecl]
 def changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkDefEq := true) : MetaM MVarId := do

tests/lean/run/change_tac.lean

@@ -0,0 +1,76 @@
+private axiom test_sorry : ∀ {α}, α
+
+example : n + 2 = m := by
+  change n + 1 + 1 = _
+  guard_target =ₛ n + 1 + 1 = m
+  exact test_sorry
+
+example (h : n + 2 = m) : False := by
+  change _ + 1 = _ at h
+  guard_hyp h :ₛ n + 1 + 1 = m
+  exact test_sorry
+
+example : n + 2 = m := by
+  fail_if_success change true
+  fail_if_success change _ + 3 = _
+  fail_if_success change _ * _ = _
+  change (_ : Nat) + _ = _
+  exact test_sorry
+
+-- `change ... at ...` allows placeholders to mean different things at different hypotheses
+example (h : n + 3 = m) (h' : n + 2 = m) : False := by
+  change _ + 1 = _ at h h'
+  guard_hyp h :ₛ n + 2 + 1 = m
+  guard_hyp h' :ₛ n + 1 + 1 = m
+  exact test_sorry
+
+-- `change ... at ...` preserves dependencies
+example (p : n + 2 = m → Type) (h : n + 2 = m) (x : p h) : false := by
+  change _ + 1 = _ at h
+  guard_hyp x :ₛ p h
+  exact test_sorry
+
+noncomputable example : Nat := by
+  fail_if_success change Type 1
+  exact test_sorry
+
+def foo (a b c : Nat) := if a < b then c else 0
+
+example : foo 1 2 3 = 3 := by
+  change (if _ then _ else _) = _
+  change ite _ _ _ = _
+  change (if _ < _ then _ else _) = _
+  change _ = (if true then 3 else 4)
+  rfl
+
+example (h : foo 1 2 3 = 4) : True := by
+  change ite _ _ _ = _ at h
+  guard_hyp h :ₛ ite (1 < 2) 3 0 = 4
+  trivial
+
+example (h : foo 1 2 3 = 4) : True := by
+  change (if _ then _ else _) = _ at h
+  guard_hyp h : (if 1 < 2 then 3 else 0) = 4
+  trivial
+
+example (α : Type) [LT α] (x : α) (h : x < x) : x < id x := by
+  change _ < _ -- can defer LT typeclass lookup, just like `show`
+  change _ < _ at h -- can defer LT typeclass lookup at h too
+  guard_target =ₛ x < id x
+  change _ < x
+  guard_target =ₛ x < x
+  exact h
+
+-- This example shows using named and anonymous placeholders to create a new goal.
+example (x y : Nat) (h : x = y) : True := by
+  change (if 1 < 2 then x else ?z + ?_) = y at h
+  rotate_left
+  · exact 4
+  · exact 37
+  guard_hyp h : (if 1 < 2 then x else 4 + 37) = y
+  · trivial
+
+example : let x := 22; let y : Nat := x; let z : Fin (y + 1) := 0; z.1 < y + 1 := by
+  intro x y z -- `z` was previously erroneously marked as unused
+  change _ at y
+  exact z.2