From d0e34aaed50c1bfbb15717d60b310d094341bb3e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 15 May 2024 01:22:54 +0200
Subject: [PATCH] feat: add `revertAll` tactic for `grind` (#4167)

---
 src/Init/Grind.lean                       |  1 +
 src/Init/Grind/Norm.lean                  |  4 +--
 src/Init/Grind/Tactics.lean               | 14 ++++++++++
 src/Lean/Meta/Tactic/Grind.lean           |  1 +
 src/Lean/Meta/Tactic/Grind/RevertAll.lean | 33 +++++++++++++++++++++++
 tests/lean/run/grind_revertAll.lean       | 19 +++++++++++++
 6 files changed, 70 insertions(+), 2 deletions(-)
 create mode 100644 src/Init/Grind/Tactics.lean
 create mode 100644 src/Lean/Meta/Tactic/Grind/RevertAll.lean
 create mode 100644 tests/lean/run/grind_revertAll.lean

diff --git a/src/Init/Grind.lean b/src/Init/Grind.lean
index 0c58821b37..b495ac9f1a 100644
--- a/src/Init/Grind.lean
+++ b/src/Init/Grind.lean
@@ -5,3 +5,4 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Grind.Norm
+import Init.Grind.Tactics
diff --git a/src/Init/Grind/Norm.lean b/src/Init/Grind/Norm.lean
index 1b1ec57443..192fd3eb0c 100644
--- a/src/Init/Grind/Norm.lean
+++ b/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
diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean
new file mode 100644
index 0000000000..89e30d2b8b
--- /dev/null
+++ b/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
diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean
index f3b0511d0b..05b9295897 100644
--- a/src/Lean/Meta/Tactic/Grind.lean
+++ b/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
diff --git a/src/Lean/Meta/Tactic/Grind/RevertAll.lean b/src/Lean/Meta/Tactic/Grind/RevertAll.lean
new file mode 100644
index 0000000000..e591d43b5e
--- /dev/null
+++ b/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
diff --git a/tests/lean/run/grind_revertAll.lean b/tests/lean/run/grind_revertAll.lean
new file mode 100644
index 0000000000..f17a5f27c4
--- /dev/null
+++ b/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₂