feat: add assertAfter tactic

src/Lean/LocalContext.lean

@@ -282,11 +282,11 @@ lctx.decls.findSomeRevM? $ fun decl => match decl with
   | none      => pure none
   | some decl => f decl
 
-@[specialize] def foldlFromM (lctx : LocalContext) (f : β → LocalDecl → m β) (b : β) (decl : LocalDecl) : m β :=
+@[specialize] def foldlFromM (lctx : LocalContext) (f : β → LocalDecl → m β) (b : β) (index : Nat) : m β :=
 lctx.decls.foldlFromM (fun b decl => match decl with
   | none      => pure b
   | some decl => f b decl)
-  b decl.index
+  b index
 
 end
 
@@ -299,8 +299,8 @@ Id.run $ lctx.findDeclM? f
 @[inline] def findDeclRev? {β} (lctx : LocalContext) (f : LocalDecl → Option β) : Option β :=
 Id.run $ lctx.findDeclRevM? f
 
-@[inline] def foldlFrom {β} (lctx : LocalContext) (f : β → LocalDecl → β) (b : β) (decl : LocalDecl) : β :=
-Id.run $ lctx.foldlFromM f b decl
+@[inline] def foldlFrom {β} (lctx : LocalContext) (f : β → LocalDecl → β) (b : β) (index : Nat) : β :=
+Id.run $ lctx.foldlFromM f b index
 
 partial def isSubPrefixOfAux (a₁ a₂ : PArray (Option LocalDecl)) (exceptFVars : Array Expr) : Nat → Nat → Bool
 | i, j =>

src/Lean/Meta/Tactic/Assert.lean

@@ -4,6 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.FVarSubst
+import Lean.Meta.Tactic.Intro
+import Lean.Meta.Tactic.Revert
 
 namespace Lean
 namespace Meta
@@ -50,5 +53,39 @@ withMVarContext mvarId $ do
   assignExprMVar mvarId (mkApp2 newMVar val rflPrf);
   pure newMVar.mvarId!
 
+structure AssertAfterResult :=
+(fvarId : FVarId)
+(mvarId : MVarId)
+(subst  : FVarSubst)
+
+/--
+  Convert the given goal `Ctx |- target` into a goal containing `(userName : type)` after the local declaration with if `fvarId`.
+  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 assertAfter (mvarId : MVarId) (fvarId : FVarId) (userName : Name) (type : Expr) (val : Expr) : MetaM AssertAfterResult := do
+withMVarContext mvarId $ do
+  checkNotAssigned mvarId `assertAfter;
+  tag        ← getMVarTag mvarId;
+  target     ← getMVarType mvarId;
+  localDecl  ← getLocalDecl fvarId;
+  lctx       ← getLCtx;
+  localInsts ← getLocalInstances;
+  let fvarIds := lctx.foldlFrom (fun (fvarIds : Array FVarId) decl => fvarIds.push decl.fvarId) #[] (localDecl.index+1);
+  let xs   := fvarIds.map mkFVar;
+  targetNew ← mkForallFVars xs target;
+  let targetNew := Lean.mkForall userName BinderInfo.default type targetNew;
+  let lctxNew := fvarIds.foldl (fun (lctxNew : LocalContext) fvarId => lctxNew.erase fvarId) lctx;
+  let localInstsNew := localInsts.filter fun inst => fvarIds.contains inst.fvar.fvarId!;
+  mvarNew ← mkFreshExprMVarAt lctxNew localInstsNew targetNew MetavarKind.syntheticOpaque tag;
+  let args := (fvarIds.filter fun fvarId => !(lctx.get! fvarId).isLet).map mkFVar;
+  let args := #[val] ++ args;
+  assignExprMVar mvarId (mkAppN mvarNew args);
+  (fvarIdNew, mvarIdNew) ← intro1 mvarNew.mvarId! false;
+  (fvarIdsNew, mvarIdNew) ← introN mvarIdNew fvarIds.size [] false;
+  let subst := fvarIds.size.fold
+    (fun i (subst : FVarSubst) => subst.insert (fvarIds.get! i) (mkFVar (fvarIdsNew.get! i)))
+    {};
+  pure { fvarId := fvarIdNew, mvarId := mvarIdNew, subst := subst }
+
 end Meta
 end Lean

src/Lean/MetavarContext.lean

@@ -775,7 +775,7 @@ else do
       else
         pure newToRevert)
     newToRevert
-    firstDeclToVisit
+    firstDeclToVisit.index
 
 /-- Create a new `LocalContext` by removing the free variables in `toRevert` from `lctx`.
     We use this function when we create auxiliary metavariables at `elimMVarDepsAux`. -/

tests/lean/run/meta7.lean

@@ -73,3 +73,25 @@ forallBoundedTelescope t (some 0) fun xs b => do
   pure ()
 
 #eval tst3
+
+def tst4 : MetaM Unit := do
+print "----- tst4 -----";
+let nat := mkConst `Nat;
+withLocalDeclD `x nat fun x => withLocalDeclD `y nat fun y => do
+m ← mkFreshExprMVar nat;
+print (← ppGoal m.mvarId!);
+val ← mkAppM `HasAdd.add #[mkNatLit 10, y];
+⟨zId, nId, subst⟩ ← assertAfter m.mvarId! x.fvarId! `z nat val;
+print m;
+print (← ppGoal nId);
+withMVarContext nId do {
+  print (subst.apply x ++ " " ++ subst.apply y ++ " " ++ mkFVar zId);
+  assignExprMVar nId (← mkAppM `HasAdd.add #[subst.apply x, mkFVar zId]);
+  print (mkMVar nId)
+};
+print m;
+expected ← mkAppM `HasAdd.add #[x, val];
+check (isDefEq m expected);
+pure ()
+
+#eval tst4