change with -> change_matching with

src/Init/Conv.lean

@@ -103,9 +103,9 @@ syntax (name := ext) "ext" (ppSpace colGt ident)* : conv
 assuming `t` and `t'` are definitionally equal. -/
 syntax (name := change) "change " term : conv
 
-/-- `change p with t` replaces all occurrences of `p` in the target with `t`,
+/-- `change_matching p with t` replaces all occurrences of `p` in the target with `t`,
 assuming `p` and `t` are definitionally equal. -/
-syntax (name := changeWith) "change " term " with " term : conv
+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

src/Init/Tactics.lean

@@ -496,11 +496,11 @@ 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 occurrences of `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

@@ -33,10 +33,10 @@ 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
 
 @[builtin_tactic change] elab_rules : tactic
@@ -45,18 +45,24 @@ def elabChange (e : Expr) (p : Term) : TacticM Expr := do
       (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 the same as doing `rewrite [show p = t by rfl]` on `e`.
+This is roughly like doing `rewrite [show p = t by rfl]` on `e`, but it does not require a type-correct motive.
 -/
-def elabChangeWith (e : Expr) (p t : Term) : TacticM Expr := do
+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
@@ -66,30 +72,36 @@ def elabChangeWith (e : Expr) (p t : Term) : TacticM Expr := do
   let e' ← kabstract e p
   unless e'.hasLooseBVars do
     throwError "\
-      'change with' tactic failed, did not find instance of the pattern{indentExpr p}\n\
+      '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 with' tactic failed, pattern{indentExpr p}\n\
+        'change_matching' tactic failed, pattern{indentExpr p}\n\
         is not definitionally equal to replacement{indentExpr t}"
     instantiateMVars (e'.instantiate1 t)
 
-@[builtin_tactic changeWith] elab_rules : tactic
-  | `(tactic| change $p:term with $t:term $[$loc:location]?) => do
+@[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 (elabChangeWith hTy p t) (← getMainTag) `change
+        let (hTy', mvars) ← withCollectingNewGoalsFrom (elabChangeMatching hTy p t) (← getMainTag) `change_matching
         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 g ← popMainGoal
-        let (e', mvars) ← withCollectingNewGoalsFrom (elabChangeWith (← g.getType) p t) (← g.getTag) `change
-        let g ← g.replaceTargetDefEq e'
-        pushGoals (g :: mvars))
-      (failed := fun _ => throwError "'change with' tactic failed")
+        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

@@ -22,11 +22,11 @@ open Meta
     changeLhs lhs'
   | _ => throwUnsupportedSyntax
 
-@[builtin_tactic Lean.Parser.Tactic.Conv.changeWith] def evalChangeWith : Tactic
-  | `(conv| change $p:term with $t:term) => do
+@[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' ← elabChangeWith lhs p t
+    let lhs' ← elabChangeMatching lhs p t
     logUnassignedAndAbort (← filterOldMVars (← getMVars lhs') mvarCounterSaved)
     changeLhs lhs'
   | _ => throwUnsupportedSyntax

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

@@ -4,7 +4,6 @@
 
 private axiom test_sorry : ∀ {α}, α
 
-set_option linter.missingDocs false
 set_option pp.mvars false
 
 example : n + 2 = m := by
@@ -212,199 +211,3 @@ example (a b c d : Nat) : a + b + c = d := by
   let e := ?mvar
   trace_state
   exact test_sorry
-
-
-/-!
-`change with`, basic test
--/
-example : 1 + 2 = 3 := by
-  change 2 with 1 + 1
-  guard_target =ₛ 1 + (1 + 1) = 3
-  rfl
-
-/-!
-`change with`, new `let` binding
--/
-example : 1 + 2 = 3 := by
-  let x := 2
-  change 2 with x
-  guard_target =ₛ 1 + x = 3
-  rfl
-
-/-!
-`change with`, no change throws error
--/
-/--
-error: 'change with' tactic failed, did not find instance of the pattern
-  4
-in the expression
-  1 + 2 = 3
--/
-#guard_msgs in example : 1 + 2 = 3 := by
-  change 4 with 2 + 2
-
-/-!
-`change with`, basic test at hypothesis
--/
-example (h : 1 + 2 = 3) : True := by
-  change 2 with 1 + 1 at h
-  guard_hyp h :ₛ 1 + (1 + 1) = 3
-  trivial
-
-/-!
-`change with`, new `let` binding at hypothesis
--/
-example (h : 1 + 2 = 3) : True := by
-  let x := 2
-  change 2 with x at h
-  guard_hyp h :ₛ 1 + x = 3
-  trivial
-
-/-!
-`change with`, no change at hypothesis throws error
--/
-/--
-error: 'change with' tactic failed, did not find instance of the pattern
-  4
-in the expression
-  1 + 2 = 3
--/
-#guard_msgs in example (h : 1 + 2 = 3) : True := by
-  change 4 with 2 + 2 at h
-
-/-!
-`change with at *`
--/
-/--
-info: x : Nat := 2
-h : 1 + x = 3
-⊢ 1 + x = 3
--/
-#guard_msgs in example (h : 1 + 2 = 3) : 1 + 2 = 3 := by
-  let x := 2
-  change 2 with x at *
-  trace_state
-  exact h
-
-/-!
-`change with at *`, no change at hypothesis, no permutation of hypotheses
--/
-/--
-info: _h : 1 + 2 = 3
-x : Nat := 2
-⊢ 4 + 2 = 6
--/
-#guard_msgs in example (_h : 1 + 2 = 3) : 4 + 2 = 6 := by
-  let x := 2
-  change 4 with 4 at *
-  trace_state
-  rfl
-
-/-!
-`change with`, not-defeq replacement
--/
-/--
-error: 'change with' tactic failed, pattern
-  1
-is not definitionally equal to replacement
-  2
--/
-#guard_msgs in example : 1 = 2 := by
-  change 1 with 2
-
-/-!
-`change with`, replacement doesn't have correct type
--/
-/--
-error: type mismatch
-  Nat.zero
-has type
-  Nat : Type
-but is expected to have type
-  Bool : Type
--/
-#guard_msgs in example : true = true := by
-  change true with Nat.zero
-  fail "should not get here"
-
-/-!
-`change with`, replacement has a metavariable
--/
-example : 1 + 2 = 3 := by
-  change 2 with _ + 1
-  guard_target =ₛ 1 + (1 + 1) = 3
-  rfl
-
-/-!
-`change with at *`, pattern and replacement have metavariables, different solutions each time
--/
-/--
-info: h : 4 + 1 + 6 = 11
-⊢ 0 + 1 + 2 = 3
--/
-#guard_msgs in example (h : 5 + 6 = 11) : 1 + 2 = 3 := by
-  change OfNat.ofNat _ with _ + 1 at *
-  trace_state
-  rfl
-
-/-!
-`change with` can get the type from the target expression
--/
-example : (1 : Int) + 2 = 3 := by
-  change 2 with 1 + 1
-  guard_target =ₛ (1 : Int) + (1 + 1) = 3
-  rfl
-
-/-!
-## Conv mode
--/
-
-/-!
-conv `change with`
--/
-
-example (a : Nat) : 2 + (2 + 2) = a := by
-  conv =>
-    enter [1,2]
-    change 2 with 1 + 1
-  guard_target =ₛ 2 + ((1 + 1) + (1 + 1)) = a
-  conv =>
-    enter [1,2,1]
-    change 1 with 0 + 1
-  guard_target =ₛ 2 + (((0 + 1) + (0 + 1)) + (1 + 1)) = a
-  exact test_sorry
-
-/-!
-conv `change with` doesn't allow unsolved metavariables
--/
-/--
-error: don't know how to synthesize placeholder for argument 'e'
-context:
-case foo
-a : Nat
-⊢ Nat
----
-error: unsolved goals
-a : Nat
-⊢ 2 = a
--/
-#guard_msgs in
-example (a : Nat) : 2 = a := by
-  conv =>
-    change 2 with (if True then 2 else ?foo)
-
-/-!
-conv `change with` allows metavariables if they're solved for
--/
-/--
-info: a : Nat
-x : Nat := 2
-⊢ 2 = a
--/
-#guard_msgs in
-example (a : Nat) : 2 = a := by
-  conv =>
-    change 2 with ?two
-  let x := ?two
-  trace_state
-  exact test_sorry