feat: revert tactic

src/Init/Lean/Meta/Basic.lean

@@ -414,6 +414,9 @@ if xs.isEmpty then pure e else liftMkBindingM $ MetavarContext.mkLambda xs e
 def mkForallUsedOnly (xs : Array Expr) (e : Expr) : MetaM (Expr × Nat) :=
 if xs.isEmpty then pure (e, 0) else liftMkBindingM $ MetavarContext.mkForallUsedOnly xs e
 
+def elimMVarDeps (xs : Array Expr) (e : Expr) : MetaM Expr :=
+if xs.isEmpty then pure e else liftMkBindingM $ MetavarContext.elimMVarDeps xs e
+
 /-- Save cache, execute `x`, restore cache -/
 @[inline] def savingCache {α} (x : MetaM α) : MetaM α := do
 s ← get;

src/Init/Lean/Meta/Tactic.lean

@@ -7,3 +7,4 @@ prelude
 import Init.Lean.Meta.Tactic.Intro
 import Init.Lean.Meta.Tactic.Assumption
 import Init.Lean.Meta.Tactic.Apply
+import Init.Lean.Meta.Tactic.Revert

src/Init/Lean/Meta/Tactic/Revert.lean

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Meta.Tactic.Util
+
+namespace Lean
+namespace Meta
+
+def revert (mvarId : MVarId) (fvars : Array FVarId) : MetaM (Array FVarId × MVarId) :=
+if fvars.isEmpty then pure (fvars, mvarId)
+else withMVarContext mvarId $ do
+  checkNotAssigned mvarId `revert;
+  e ← elimMVarDeps (fvars.map mkFVar) (mkMVar mvarId);
+  pure $ e.withApp $ fun mvar args => (args.map Expr.fvarId!, mvar.mvarId!)
+
+end Meta
+end Lean

src/Init/Lean/MetavarContext.lean

@@ -890,6 +890,9 @@ end MkBinding
 
 abbrev MkBindingM := ReaderT LocalContext MkBinding.M
 
+def elimMVarDeps (xs : Array Expr) (e : Expr) : MkBindingM Expr :=
+fun _ => MkBinding.elimMVarDeps xs e
+
 def mkBinding (isLambda : Bool) (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) : MkBindingM (Expr × Nat) :=
 fun lctx => MkBinding.mkBinding isLambda lctx xs e usedOnly
 

src/Init/Lean/Parser/Tactic.lean

@@ -42,6 +42,7 @@ def nonEmptySeq : Parser := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "
 
 @[builtinTacticParser] def «intro»      := parser! nonReservedSymbol "intro " >> optional ident'
 @[builtinTacticParser] def «intros»     := parser! nonReservedSymbol "intros " >> many ident'
+@[builtinTacticParser] def «revert»     := parser! nonReservedSymbol "revert " >> many1 ident
 @[builtinTacticParser] def «assumption» := parser! nonReservedSymbol "assumption"
 @[builtinTacticParser] def «apply»      := parser! nonReservedSymbol "apply " >> termParser
 @[builtinTacticParser] def «exact»      := parser! nonReservedSymbol "exact " >> termParser