feat: add revertAll tactic for grind (#4167)

src/Init/Grind.lean

@@ -5,3 +5,4 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Grind.Norm
+import Init.Grind.Tactics

src/Init/Grind/Norm.lean

@@ -8,7 +8,7 @@ import Init.SimpLemmas
 import Init.Classical
 import Init.ByCases
 
-namespace Lean.Meta.Grind
+namespace Lean.Grind
 /-!
 Normalization theorems for the `grind` tactic.
 
@@ -107,4 +107,4 @@ attribute [grind_norm] Nat.le_zero_eq
 -- GT GE
 attribute [grind_norm] GT.gt GE.ge
 
-end Lean.Meta.Grind
+end Lean.Grind

src/Init/Grind/Tactics.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Tactics
+
+namespace Lean.Grind
+/-!
+`grind` tactic and related tactics.
+-/
+
+end Lean.Grind

src/Lean/Meta/Tactic/Grind.lean

@@ -5,3 +5,4 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Grind.Attr
+import Lean.Meta.Tactic.Grind.RevertAll

src/Lean/Meta/Tactic/Grind/RevertAll.lean

@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Util
+
+namespace Lean.Meta.Grind
+
+/--
+Revert all free variables at goal `mvarId`.
+-/
+def _root_.Lean.MVarId.revertAll (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
+  mvarId.checkNotAssigned `revertAll
+  let fvarIds := (← getLCtx).getFVarIds
+  let fvars ← fvarIds.filterMapM fun fvarId => do
+    if (← fvarId.getDecl).isAuxDecl then
+      return none
+    else
+      return some (mkFVar fvarId)
+  let tag ← mvarId.getTag
+  mvarId.setKind .natural
+  let (e, _) ←
+    try
+      liftMkBindingM <| MetavarContext.revert fvars mvarId (preserveOrder := true)
+    finally
+      mvarId.setKind .syntheticOpaque
+  let mvar := e.getAppFn
+  mvar.mvarId!.setTag tag
+  return mvar.mvarId!
+
+end Lean.Meta.Grind

tests/lean/run/grind_revertAll.lean

@@ -0,0 +1,19 @@
+import Lean
+
+open Lean Elab Tactic in
+elab "revert_all" : tactic => do
+  liftMetaTactic1 (·.revertAll)
+
+example {α : Type u} [Inhabited α] (a : α) (f : α → α) (h : f a = default) : default = f a := by
+  revert_all
+  guard_target =ₛ∀ {α : Type u} [inst : Inhabited α] (a : α) (f : α → α), f a = default → default = f a
+  intro α inst a f h
+  exact h.symm
+
+example (a b : α) (h₁ : a = b) (f g : α → α) (h₂ : ∀ x, f x = x) (h₃ : ∀ x, g x = f x) : ∃ x : α, f x = a ∧ g x = b := by
+  apply Exists.intro
+  revert_all
+  intro β a₁ a₂ h f₁ f₂ h' h''
+  constructor
+  · exact h' a₁
+  · rw [h'', h]; exact h' a₂