From 70b41fe65976b4eefa89d489245e7b0529703f41 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 8 Feb 2020 17:30:00 -0800
Subject: [PATCH] feat: `revert` tactic

---
 src/Init/Lean/Meta/Basic.lean         |  3 +++
 src/Init/Lean/Meta/Tactic.lean        |  1 +
 src/Init/Lean/Meta/Tactic/Revert.lean | 20 ++++++++++++++++++++
 src/Init/Lean/MetavarContext.lean     |  3 +++
 src/Init/Lean/Parser/Tactic.lean      |  1 +
 5 files changed, 28 insertions(+)
 create mode 100644 src/Init/Lean/Meta/Tactic/Revert.lean

diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index 7ccd9b0947..9100c24dcc 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/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;
diff --git a/src/Init/Lean/Meta/Tactic.lean b/src/Init/Lean/Meta/Tactic.lean
index 8cf5925c5e..af6c31eb8b 100644
--- a/src/Init/Lean/Meta/Tactic.lean
+++ b/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
diff --git a/src/Init/Lean/Meta/Tactic/Revert.lean b/src/Init/Lean/Meta/Tactic/Revert.lean
new file mode 100644
index 0000000000..a64fac75e4
--- /dev/null
+++ b/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
diff --git a/src/Init/Lean/MetavarContext.lean b/src/Init/Lean/MetavarContext.lean
index 1636feb3ba..e05698c0ff 100644
--- a/src/Init/Lean/MetavarContext.lean
+++ b/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
 
diff --git a/src/Init/Lean/Parser/Tactic.lean b/src/Init/Lean/Parser/Tactic.lean
index 587d75d10b..3cf8b773d3 100644
--- a/src/Init/Lean/Parser/Tactic.lean
+++ b/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