fix: improvements to change tactic

This PR makes the `change` tactic and conv tactic use the same new elaboration strategy that works uniformly for both the target and local hypotheses. Fixes an issue where the following example would fail due to `a` being defined after `h`:
```lean
example (x y z w : Nat) (h : x + y = z + w) : True := by
  let a := x + y
  change a = _ at h
  trivial
```
Breaking change: `change` no longer creates goals if there are unassigned metavariables. Instead it throws "don't know how to synthesize placeholder" errors.

src/Lean/Elab/Tactic/Change.lean

@@ -13,6 +13,22 @@ open Meta
 # Implementation of the `change` tactic
 -/
 
+/-- Elaborates the pattern `p` and ensures that it is defeq to `e`. -/
+def elabChange (e : Expr) (p : Term) : TacticM Expr := do
+  let mvarCounterSaved := (← getMCtx).mvarCounter
+  let p ← elabTermEnsuringType p (← inferType e) (mayPostpone := true)
+  -- Discretionary `isDefEq` before synthesizing remaining metavariables. Save the result to avoid a final `isDefEq` check if it passes.
+  let defeq ← isDefEq p e
+  Term.synthesizeSyntheticMVarsNoPostponing
+  withAssignableSyntheticOpaque do
+    unless ← pure defeq <||> isDefEq p e do
+      let (p, tgt) ← addPPExplicitToExposeDiff p e
+      throwError "\
+        'change' tactic failed, pattern{indentExpr p}\n\
+        is not definitionally equal to target{indentExpr tgt}"
+    logUnassignedAndAbort (← filterOldMVars (← getMVars p) mvarCounterSaved)
+    instantiateMVars p
+
 /-- `change` can be used to replace the main goal or its hypotheses with
 different, yet definitionally equal, goal or hypotheses.
 
@@ -38,15 +54,13 @@ the main goal. -/
   | `(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")
+        let hTy' ← elabChange (← h.getType) newType
+        liftMetaTactic1 fun mvarId => do
+          mvarId.changeLocalDecl h hTy')
+      (atTarget := do
+        let tgt' ← elabChange (← getMainTarget) newType
+        liftMetaTactic1 fun mvarId => do
+          mvarId.replaceTargetDefEq tgt')
+      (failed := fun _ => throwError "'change' tactic failed")
 
 end Lean.Elab.Tactic

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

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Elab.Tactic.ElabTerm
+import Lean.Elab.Tactic.Change
 import Lean.Elab.Tactic.Conv.Basic
 
 namespace Lean.Elab.Tactic.Conv
@@ -14,12 +15,8 @@ open Meta
   match stx with
   | `(conv| change $e) => withMainContext do
     let lhs ← getLhs
-    let mvarCounterSaved := (← getMCtx).mvarCounter
-    let r ← elabTermEnsuringType e (← inferType lhs)
-    logUnassignedAndAbort (← filterOldMVars (← getMVars r) mvarCounterSaved)
-    unless (← isDefEqGuarded r lhs) do
-      throwError "invalid 'change' conv tactic, term{indentExpr r}\nis not definitionally equal to current left-hand-side{indentExpr lhs}"
-    changeLhs r
+    let lhs' ← elabChange lhs e
+    changeLhs lhs'
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic.Conv

tests/lean/run/change.lean

@@ -2,7 +2,19 @@
 private axiom test_sorry : ∀ {α}, α
 
 set_option linter.missingDocs false
-set_option autoImplicit true
+set_option pp.mvars false
+
+/-!
+`conv` failure
+-/
+/--
+error: 'change' tactic failed, pattern
+  m = ?_
+is not definitionally equal to target
+  n = m
+-/
+#guard_msgs in example : n = m := by
+  change m = _
 
 example : n + 2 = m := by
   change n + 1 + 1 = _
@@ -41,7 +53,6 @@ noncomputable example : Nat := by
 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)
@@ -53,7 +64,7 @@ example (h : foo 1 2 3 = 4) : True := by
   trivial
 
 example (h : foo 1 2 3 = 4) : True := by
-  change (if _ then _ else _) = _ at h
+  change ite _ _ _ = _ at h
   guard_hyp h : (if 1 < 2 then 3 else 0) = 4
   trivial
 
@@ -65,16 +76,116 @@ example (α : Type) [LT α] (x : α) (h : x < x) : x < id x := by
   guard_target =ₛ x < x
   exact h
 
--- This example shows using named and anonymous placeholders to create a new goal.
+/-!
+`change` can create new metavariables and assign them
+-/
+/--
+info: x y z : Nat
+w : Nat := x + y
+⊢ x + y = z
+-/
+#guard_msgs in
+example (x y z : Nat) : x + y = z := by
+  change ?a = _
+  let w := ?a
+  trace_state
+  exact test_sorry
+
+/-!
+`change` is not allowed to create new goals
+-/
+/--
+error: don't know how to synthesize placeholder for argument 'e'
+context:
+case z
+x y : Nat
+h : x = y
+⊢ Nat
+---
+error: unsolved goals
+x y : Nat
+h : x = y
+⊢ True
+-/
+#guard_msgs in
 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
+  change (if 1 < 2 then x else ?z) = y at h
 
 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
+
+/-!
+`change` reorders hypotheses if necessary
+-/
+/--
+info: x y z w : Nat
+a : Nat := x + y
+h : a = z + w
+⊢ True
+-/
+#guard_msgs in
+example (x y z w : Nat) (h : x + y = z + w) : True := by
+  let a := x + y
+  change a = _ at h
+  trace_state
+  trivial
+
+/-!
+## Conv `change`
+-/
+
+/-!
+conv `change` test
+-/
+example (m n : Nat) : m + 2 = n := by
+  conv => enter [1]; change m + (1 + 1)
+  guard_target =ₛ m + (1 + 1) = n
+  exact test_sorry
+
+/-!
+conv `change` test failure
+-/
+/--
+error: 'change' tactic failed, pattern
+  m + n
+is not definitionally equal to target
+  m + 2
+-/
+#guard_msgs in
+example (m n : Nat) : m + 2 = n := by
+  conv => enter [1]; change m + n
+
+/-!
+conv `change` unsolved metavariables
+-/
+/--
+error: don't know how to synthesize placeholder for argument 'e'
+context:
+case a
+m n : Nat
+⊢ Nat
+---
+error: unsolved goals
+m n : Nat
+⊢ m + 2 = n
+-/
+#guard_msgs in
+example (m n : Nat) : m + 2 = n := by
+  conv => enter [1]; change if True then m + 2 else ?a
+
+/-!
+conv `change` to create a metavariable
+-/
+/--
+info: a b c d : Nat
+e : Nat := a + b
+⊢ a + b + c = d
+-/
+#guard_msgs in
+example (a b c d : Nat) : a + b + c = d := by
+  conv => enter [1,1]; change ?mvar
+  let e := ?mvar
+  trace_state
+  exact test_sorry