feat: make sure clear_value preserves local context order (#8792)

This PR makes the `clear_value` tactic preserve the order of variables
in the local context. This is done by adding
`Lean.MVarId.withRevertedFrom`, which reverts all local variables
starting from a given variable, rather than only the ones that depend on
it.

Note: an alternative implementation might convert the ldecl to a cdecl
and then reset the meta cache. This assumes that there are no other
caches that might still remember the value of the ldecl.

src/Lean/Meta/Tactic/Replace.lean

@@ -170,6 +170,20 @@ def _root_.Lean.MVarId.withReverted (mvarId : MVarId) (fvarIds : Array FVarId)
         Elab.pushInfoLeaf (.ofFVarAliasInfo { id := y, baseId := x, userName := ← y.getUserName })
   return (r, mvarId)
 
+/--
+Like `Lean.MVarId.withReverted`, but reverts all local variables starting from `fvarId`.
+-/
+def _root_.Lean.MVarId.withRevertedFrom (mvarId : MVarId) (fvarId : FVarId)
+    (k : MVarId → Array FVarId → MetaM (α × Array (Option FVarId) × MVarId)) : MetaM (α × MVarId) := do
+  let (xs, mvarId) ← mvarId.revertFrom fvarId
+  let (r, xs', mvarId) ← k mvarId xs
+  let (ys, mvarId) ← mvarId.introNP xs'.size
+  mvarId.withContext do
+    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`.
 
@@ -216,15 +230,16 @@ def _root_.Lean.MVarId.modifyTargetEqLHS (mvarId : MVarId) (f : Expr → MetaM E
      else
        throwTacticEx `modifyTargetEqLHS mvarId m!"equality expected{indentExpr target}"
 
-
 /--
 Clears the value of the local definition `fvarId`. Ensures that the resulting goal state
 is still type correct. Throws an error if it is a local hypothesis without a value.
+
+Preserves the order of the local context.
 -/
 def _root_.Lean.MVarId.clearValue (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId := do
   mvarId.checkNotAssigned `clear_value
   let tag ← mvarId.getTag
-  let (_, mvarId) ← mvarId.withReverted #[fvarId] fun mvarId' fvars => mvarId'.withContext do
+  let (_, mvarId) ← mvarId.withRevertedFrom fvarId fun mvarId' fvars => mvarId'.withContext do
     let tgt ← mvarId'.getType
     unless tgt.isLet do
       mvarId.withContext <|

src/Lean/Meta/Tactic/Revert.lean

@@ -54,4 +54,11 @@ def _root_.Lean.MVarId.revertAfter (mvarId : MVarId) (fvarId : FVarId) : MetaM (
     let fvarIds := (← getLCtx).foldl (init := #[]) (start := localDecl.index+1) fun fvarIds decl => fvarIds.push decl.fvarId
     mvarId.revert fvarIds (preserveOrder := true) (clearAuxDeclsInsteadOfRevert := true)
 
+/-- Reverts all local declarations starting from `fvarId`. -/
+def _root_.Lean.MVarId.revertFrom (mvarId : MVarId) (fvarId : FVarId) : MetaM (Array FVarId × MVarId) :=
+  mvarId.withContext do
+    let localDecl ← fvarId.getDecl
+    let fvarIds := (← getLCtx).foldl (init := #[]) (start := localDecl.index) fun fvarIds decl => fvarIds.push decl.fvarId
+    mvarId.revert fvarIds (preserveOrder := true) (clearAuxDeclsInsteadOfRevert := true)
+
 end Lean.Meta

tests/lean/run/clear_value.lean

@@ -347,3 +347,19 @@ example : True := by
     clear_value val -- used to fail
     rfl
   trivial
+
+/-!
+Local context order preservation.
+-/
+/--
+trace: x : Nat
+y : Nat := 2
+z : Nat := 3
+⊢ x + y = x + z - 1
+-/
+#guard_msgs in
+example : let x := 1; let y := 2; let z := 3; x + y = x + z - 1 := by
+  intro x y z
+  clear_value x
+  trace_state
+  rfl