feat: change_matching ... with tactic

src/Init/Conv.lean

@@ -103,6 +103,10 @@ syntax (name := ext) "ext" (ppSpace colGt ident)* : conv
 assuming `t` and `t'` are definitionally equal. -/
 syntax (name := change) "change " term : conv
 
+/-- `change_matching p with t` replaces all occurrences of `p` in the target with `t`,
+assuming `p` and `t` are definitionally equal. -/
+syntax (name := changeMatching) "change_matching " term " with " term : conv
+
 /-- `delta id1 id2 ...` unfolds all occurrences of `id1`, `id2`, ... in the target.
 Like the `delta` tactic, this ignores any definitional equations and uses
 primitive delta-reduction instead, which may result in leaking implementation details.

src/Init/Tactics.lean

@@ -469,19 +469,38 @@ hypotheses or the goal. It can have one of the forms:
 syntax location := withPosition(ppGroup(" at" (locationWildcard <|> locationHyp)))
 
 /--
-* `change tgt'` will change the goal from `tgt` to `tgt'`,
-  assuming these are definitionally equal.
-* `change t' at h` will change hypothesis `h : t` to have type `t'`, assuming
+* `change tgt'` changes the target of the goal from `tgt` to `tgt'`,
+  assuming `tgt` and `tgt'` are definitionally equal.
+* `change t' at h` will change the hypothesis `h : t` to have type `t'`,
   assuming `t` and `t'` are definitionally equal.
+
+The types `tgt'` and `t'` may contain placeholders.
+The tactic `change tgt'` is equivalent to `refine show tgt' from ?_`.
+
+## Examples
+
+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`.
+Notice that the placeholders in `_ + 1 = _` are not constant across hypotheses.
 -/
 syntax (name := change) "change " term (location)? : tactic
 
 /--
-* `change a with b` will change occurrences of `a` to `b` in the goal,
+* `change_matching a with b` will change occurrences of `a` to `b` in the goal,
   assuming `a` and `b` are definitionally equal.
-* `change a with b at h` similarly changes `a` to `b` in the type of hypothesis `h`.
+* `change_matching a with b at h` similarly changes occurrences of `a` to `b` in the type of hypothesis `h`.
 -/
-syntax (name := changeWith) "change " term " with " term (location)? : tactic
+syntax (name := changeMatching) "change_matching " term " with " term (location)? : tactic
 
 /--
 If `thm` is a theorem `a = b`, then as a rewrite rule,

src/Lean/Elab/Tactic/Change.lean

@@ -4,13 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
 prelude
+import Lean.Meta.KAbstract
 import Lean.Meta.Tactic.Replace
 import Lean.Elab.Tactic.Location
 
 namespace Lean.Elab.Tactic
 open Meta
 /-!
-# Implementation of the `change` tactic
+# Implementations of the `change` tactics
 -/
 
 /--
@@ -32,44 +33,75 @@ def elabChange (e : Expr) (p : Term) : TacticM Expr := do
     pure p
   withAssignableSyntheticOpaque do
     unless ← isDefEq p e do
-      let (p, tgt) ← addPPExplicitToExposeDiff p e
+      let (p, e) ← addPPExplicitToExposeDiff p e
       throwError "\
         'change' tactic failed, pattern{indentExpr p}\n\
-        is not definitionally equal to target{indentExpr tgt}"
+        is not definitionally equal to target{indentExpr e}"
     instantiateMVars p
 
-/-- `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', mvars) ← withCollectingNewGoalsFrom (elabChange (← h.getType) newType) (← getMainTag) `change
         liftMetaTactic fun mvarId => do
-          return (← mvarId.changeLocalDecl h hTy') :: mvars)
+          if ← occursCheck mvarId hTy' then
+            return (← mvarId.changeLocalDecl h hTy') :: mvars
+          else
+            throwError "occurs check failed, expression{indentExpr hTy'}\ncontains the goal {Expr.mvar mvarId}")
       (atTarget := do
         let (tgt', mvars) ← withCollectingNewGoalsFrom (elabChange (← getMainTarget) newType) (← getMainTag) `change
         liftMetaTactic fun mvarId => do
-          return (← mvarId.replaceTargetDefEq tgt') :: mvars)
+          if ← occursCheck mvarId tgt' then
+            return (← mvarId.replaceTargetDefEq tgt') :: mvars
+          else
+            throwError "occurs check failed, expression{indentExpr tgt'}\ncontains the goal {Expr.mvar mvarId}")
       (failed := fun _ => throwError "'change' tactic failed")
 
+/--
+Replaces each occurrence of `p` in `e` with `t`.
+This is roughly like doing `rewrite [show p = t by rfl]` on `e`, but it does not require a type-correct motive.
+-/
+def elabChangeMatching (e : Expr) (p t : Term) : TacticM Expr := do
+  -- Set `mayPostpone := true` like when elaborating `rewrite` rules.
+  let (p, t) ← runTermElab (mayPostpone := true) do
+    let p ← Term.elabTerm p none
+    let t ← Term.elabTermEnsuringType t (← inferType p)
+    return (p, t)
+  let p ← instantiateMVars p
+  let e' ← kabstract e p
+  unless e'.hasLooseBVars do
+    throwError "\
+      'change_matching' tactic failed, did not find instance of the pattern{indentExpr p}\n\
+      in the expression{indentExpr e}"
+  -- Now that `kabstract` has unified `p` with a subterm of `e`, make sure elaboration is complete.
+  Term.synthesizeSyntheticMVarsNoPostponing
+  withAssignableSyntheticOpaque do
+    unless ← isDefEq p t do
+      let (p, t) ← addPPExplicitToExposeDiff p t
+      throwError "\
+        'change_matching' tactic failed, pattern{indentExpr p}\n\
+        is not definitionally equal to replacement{indentExpr t}"
+    instantiateMVars (e'.instantiate1 t)
+
+@[builtin_tactic changeMatching] elab_rules : tactic
+  | `(tactic| change_matching $p:term with $t:term $[$loc:location]?) => do
+    withLocation (expandOptLocation (mkOptionalNode loc))
+      (atLocal := fun h => do
+        let hTy ← h.getType
+        let (hTy', mvars) ← withCollectingNewGoalsFrom (elabChangeMatching hTy p t) (← getMainTag) `change_matching
+        liftMetaTactic fun mvarId => do
+          if ← occursCheck mvarId hTy' then
+            return (← mvarId.changeLocalDecl h hTy') :: mvars
+          else
+            throwError "occurs check failed, expression{indentExpr hTy'}\ncontains the goal {Expr.mvar mvarId}")
+      (atTarget := do
+        let (tgt', mvars) ← withCollectingNewGoalsFrom (elabChangeMatching (← getMainTarget) p t) (← getMainTag) `change_matching
+        liftMetaTactic fun mvarId => do
+          if ← occursCheck mvarId tgt' then
+            return (← mvarId.replaceTargetDefEq tgt') :: mvars
+          else
+            throwError "occurs check failed, expression{indentExpr tgt'}\ncontains the goal {Expr.mvar mvarId}")
+      (failed := fun _ => throwError "'change_matching' tactic failed")
+
 end Lean.Elab.Tactic

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

@@ -7,6 +7,7 @@ prelude
 import Lean.Elab.Tactic.ElabTerm
 import Lean.Elab.Tactic.Change
 import Lean.Elab.Tactic.Conv.Basic
+import Lean.Elab.Tactic.Change
 
 namespace Lean.Elab.Tactic.Conv
 open Meta
@@ -21,4 +22,13 @@ open Meta
     changeLhs lhs'
   | _ => throwUnsupportedSyntax
 
+@[builtin_tactic Lean.Parser.Tactic.Conv.changeMatching] def evalChangeMatching : Tactic
+  | `(conv| change_matching $p:term with $t:term) => do
+    let lhs ← getLhs
+    let mvarCounterSaved := (← getMCtx).mvarCounter
+    let lhs' ← elabChangeMatching lhs p t
+    logUnassignedAndAbort (← filterOldMVars (← getMVars lhs') mvarCounterSaved)
+    changeLhs lhs'
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Tactic.Conv

stage0/src/stdlib_flags.h

@@ -8,7 +8,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);

tests/lean/run/change.lean

@@ -1,7 +1,9 @@
+/-!
+# Tests for the `change` tactics
+-/
 
 private axiom test_sorry : ∀ {α}, α
 
-set_option linter.missingDocs false
 set_option pp.mvars false
 
 example : n + 2 = m := by