fix: improvements to change tactic (#6022)

This PR makes the `change` tactic and conv tactic use the same
elaboration strategy. It works uniformly for both the target and local
hypotheses. Now `change` can assign metavariables, for example:
```lean
example (x y z : Nat) : x + y = z := by
  change ?a = _
  let w := ?a
  -- now `w : Nat := x + y`
```

src/Lean/Elab/Tactic/Change.lean

@@ -13,6 +13,31 @@ open Meta
 # Implementation of the `change` tactic
 -/
 
+/--
+Elaborates the pattern `p` and ensures that it is defeq to `e`.
+Emulates `(show p from ?m : e)`, returning the type of `?m`, but `e` and `p` do not need to be types.
+Unlike `(show p from ?m : e)`, this can assign synthetic opaque metavariables appearing in `p`.
+-/
+def elabChange (e : Expr) (p : Term) : TacticM Expr := do
+  let p ← runTermElab do
+    let p ← Term.elabTermEnsuringType p (← inferType e)
+    unless ← isDefEq p e do
+      /-
+      Sometimes isDefEq can fail due to postponed elaboration problems.
+      We synthesize pending synthetic mvars while allowing typeclass instances to be postponed,
+      which might enable solving for them with an additional `isDefEq`.
+      -/
+      Term.synthesizeSyntheticMVars (postpone := .partial)
+      discard <| isDefEq p e
+    pure p
+  withAssignableSyntheticOpaque do
+    unless ← 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}"
+    instantiateMVars p
+
 /-- `change` can be used to replace the main goal or its hypotheses with
 different, yet definitionally equal, goal or hypotheses.
 
@@ -38,15 +63,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
+        let (hTy', mvars) ← withCollectingNewGoalsFrom (elabChange (← h.getType) newType) (← getMainTag) `change
+        liftMetaTactic fun mvarId => do
+          return (← mvarId.changeLocalDecl h hTy') :: mvars)
+      (atTarget := do
+        let (tgt', mvars) ← withCollectingNewGoalsFrom (elabChange (← getMainTarget) newType) (← getMainTag) `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")
+          return (← mvarId.replaceTargetDefEq tgt') :: mvars)
+      (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
@@ -15,11 +16,9 @@ open Meta
   | `(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
+    logUnassignedAndAbort (← filterOldMVars (← getMVars lhs') mvarCounterSaved)
+    changeLhs lhs'
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic.Conv

tests/lean/run/change.lean

@@ -2,7 +2,7 @@
 private axiom test_sorry : ∀ {α}, α
 
 set_option linter.missingDocs false
-set_option autoImplicit true
+set_option pp.mvars false
 
 example : n + 2 = m := by
   change n + 1 + 1 = _
@@ -40,6 +40,10 @@ noncomputable example : Nat := by
 
 def foo (a b c : Nat) := if a < b then c else 0
 
+/-!
+The first `change` would fail with `typeclass instance problem is stuck` if we did not have
+the `Term.synthesizeSyntheticMVars (postpone := .partial); discard <| isDefEq p e` hint
+-/
 example : foo 1 2 3 = 3 := by
   change (if _ then _ else _) = _
   change ite _ _ _ = _
@@ -65,16 +69,143 @@ 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.
+/-!
+basic failure
+-/
+/--
+error: 'change' tactic failed, pattern
+  m = ?_
+is not definitionally equal to target
+  n = m
+-/
+#guard_msgs in example : n = m := by
+  change m = _
+
+/-!
+`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 allowed to create new goals.
+Motivation: sometimes there are proof arguments that need to be filled in, and it is easier to do so as 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
+  change (if 1 < 2 then x else ?z) = y at h
   · trivial
+  · exact 22
 
 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
+
+/-!
+`change` inserts a coercion when types are incompatible.
+-/
+example (ty : {α : Prop // Nonempty α}) : ty.val := by
+  change ty
+  guard_target =ₛ ty.val
+  exact test_sorry
+
+/-!
+Fails, type hint can't hint enough since `.some _` is postponed.
+-/
+/--
+error: invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
+  ?_
+-/
+#guard_msgs in example : some true = (some true).map id := by
+  change _ = .some _
+
+/-!
+That works with a mild type hint.
+-/
+example : some true = (some true).map id := by
+  change _ = (.some _ : Option _)
+  rfl
+
+
+/-!
+## 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