From 572ffe77e3877199f0e2646154f77773f6a8a499 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Sun, 18 Dec 2022 14:43:18 -0800
Subject: [PATCH] fix: implement assertAfter using revert

---
 src/Lean/Meta/Tactic/Assert.lean | 31 ++++++++++---------------------
 src/Lean/Meta/Tactic/Revert.lean | 17 +++++++++++++----
 tests/lean/run/1963.lean         |  9 +++++++++
 3 files changed, 32 insertions(+), 25 deletions(-)
 create mode 100644 tests/lean/run/1963.lean

diff --git a/src/Lean/Meta/Tactic/Assert.lean b/src/Lean/Meta/Tactic/Assert.lean
index 953fb1cc50..6d565fe008 100644
--- a/src/Lean/Meta/Tactic/Assert.lean
+++ b/src/Lean/Meta/Tactic/Assert.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Meta.Tactic.FVarSubst
 import Lean.Meta.Tactic.Intro
+import Lean.Meta.Tactic.Revert
 
 namespace Lean.Meta
 
@@ -72,27 +73,15 @@ structure AssertAfterResult where
   It assumes `val` has type `type`, and that `type` is well-formed after `fvarId`.
   Note that `val` does not need to be well-formed after `fvarId`. That is, it may contain variables that are defined after `fvarId`. -/
 def _root_.Lean.MVarId.assertAfter (mvarId : MVarId) (fvarId : FVarId) (userName : Name) (type : Expr) (val : Expr) : MetaM AssertAfterResult := do
-  mvarId.withContext do
-    mvarId.checkNotAssigned `assertAfter
-    let tag        ← mvarId.getTag
-    let target     ← mvarId.getType
-    let localDecl  ← fvarId.getDecl
-    let lctx       ← getLCtx
-    let localInsts ← getLocalInstances
-    let fvarIds := lctx.foldl (init := #[]) (start := localDecl.index+1) fun fvarIds decl => fvarIds.push decl.fvarId
-    let xs   := fvarIds.map mkFVar
-    let targetNew ← mkForallFVars xs target (usedLetOnly := false)
-    let targetNew := Lean.mkForall userName BinderInfo.default type targetNew
-    let lctxNew := fvarIds.foldl (init := lctx) fun lctxNew fvarId => lctxNew.erase fvarId
-    let localInstsNew := localInsts.filter fun inst => !fvarIds.contains inst.fvar.fvarId!
-    let mvarNew ← mkFreshExprMVarAt lctxNew localInstsNew targetNew MetavarKind.syntheticOpaque tag
-    let args := (fvarIds.filter fun fvarId => !(lctx.get! fvarId).isLet).map mkFVar
-    let args := #[val] ++ args
-    mvarId.assign (mkAppN mvarNew args)
-    let (fvarIdNew, mvarIdNew) ← mvarNew.mvarId!.intro1P
-    let (fvarIdsNew, mvarIdNew) ← mvarIdNew.introNP fvarIds.size
-    let subst := fvarIds.size.fold (init := {}) fun i subst => subst.insert fvarIds[i]! (mkFVar fvarIdsNew[i]!)
-    return { fvarId := fvarIdNew, mvarId := mvarIdNew, subst := subst }
+  mvarId.checkNotAssigned `assertAfter
+  let (fvarIds, mvarId) ← mvarId.revertAfter fvarId
+  let mvarId ← mvarId.assert userName type val
+  let (fvarIdNew, mvarId) ← mvarId.intro1P
+  let (fvarIdsNew, mvarId) ← mvarId.introNP fvarIds.size
+  let mut subst := {}
+  for f in fvarIds, fNew in fvarIdsNew do
+    subst := subst.insert f (mkFVar fNew)
+  return { fvarId := fvarIdNew, mvarId, subst }
 
 @[deprecated MVarId.assertAfter]
 def assertAfter (mvarId : MVarId) (fvarId : FVarId) (userName : Name) (type : Expr) (val : Expr) : MetaM AssertAfterResult := do
diff --git a/src/Lean/Meta/Tactic/Revert.lean b/src/Lean/Meta/Tactic/Revert.lean
index 5c0de7e1a7..1c4da42e33 100644
--- a/src/Lean/Meta/Tactic/Revert.lean
+++ b/src/Lean/Meta/Tactic/Revert.lean
@@ -10,14 +10,16 @@ namespace Lean.Meta
 /--
 Revert free variables `fvarIds` at goal `mvarId`.
 -/
-def _root_.Lean.MVarId.revert (mvarId : MVarId) (fvarIds : Array FVarId) (preserveOrder : Bool := false) : MetaM (Array FVarId × MVarId) := do
+def _root_.Lean.MVarId.revert (mvarId : MVarId) (fvarIds : Array FVarId) (preserveOrder : Bool := false)
+    (clearAuxDeclsInsteadOfRevert := false) : MetaM (Array FVarId × MVarId) := do
   if fvarIds.isEmpty then
     pure (#[], mvarId)
   else mvarId.withContext do
     mvarId.checkNotAssigned `revert
-    for fvarId in fvarIds do
-      if (← fvarId.getDecl) |>.isAuxDecl then
-        throwError "failed to revert {mkFVar fvarId}, it is an auxiliary declaration created to represent recursive definitions"
+    unless clearAuxDeclsInsteadOfRevert do
+      for fvarId in fvarIds do
+        if (← fvarId.getDecl) |>.isAuxDecl then
+          throwError "failed to revert {mkFVar fvarId}, it is an auxiliary declaration created to represent recursive definitions"
     let fvars := fvarIds.map mkFVar
     let toRevert ← collectForwardDeps fvars preserveOrder
     /- We should clear any `auxDecl` in `toRevert` -/
@@ -43,6 +45,13 @@ def _root_.Lean.MVarId.revert (mvarId : MVarId) (fvarIds : Array FVarId) (preser
     mvar.mvarId!.setTag tag
     return (toRevert.map Expr.fvarId!, mvar.mvarId!)
 
+/-- Reverts all local declarations after `fvarId`. -/
+def _root_.Lean.MVarId.revertAfter (mvarId : MVarId) (fvarId : FVarId) : MetaM (Array FVarId × MVarId) :=
+  mvarId.withContext do
+    let localDecl ← fvarId.getDecl
+    let fvarIds := (← getLCtx).foldl (init := #[]) (start := localDecl.index+1) fun fvarIds decl => fvarIds.push decl.fvarId
+    mvarId.revert fvarIds (preserveOrder := true) (clearAuxDeclsInsteadOfRevert := true)
+
 @[deprecated MVarId.revert]
 def revert (mvarId : MVarId) (fvarIds : Array FVarId) (preserveOrder : Bool := false) : MetaM (Array FVarId × MVarId) := do
   mvarId.revert fvarIds preserveOrder
diff --git a/tests/lean/run/1963.lean b/tests/lean/run/1963.lean
new file mode 100644
index 0000000000..f1bc0a3de3
--- /dev/null
+++ b/tests/lean/run/1963.lean
@@ -0,0 +1,9 @@
+variable (x : Id Nat) (h : x = x)
+
+theorem Id_def : Id α = α := rfl
+
+theorem bar : x = x.succ := by
+  rw [Id_def] at x
+  -- rw should not expose the auxdecl `bar`:
+  fail_if_success assumption
+  sorry