fix: impossible to not cleanup the goal (#14205)

This PR stops the `impossible` tactic combinator to run `cleanup` on the
goal before negation, as that would defeat the point.

It also moves the `revertAll` function to `Revert.lean`, removes the
change of MVarId kind (`.revert` takes care of that internally,
difference should only matter if the goal has empty local context) and
renames the residual lean file to `MarkAccessible.lean`.

Fixes: #14201

Author: nomeata

src/Lean/Elab/Tactic/Grind/Have.lean

@@ -7,7 +7,7 @@ module
 prelude
 public import Lean.Elab.Tactic.Grind.Basic
 import Lean.Meta.Tactic.Grind.Intro
-import Lean.Meta.Tactic.Grind.RevertAll
+import Lean.Meta.Tactic.Grind.MarkAccessible
 import Lean.Elab.SyntheticMVars
 import Lean.Meta.Tactic.Grind.Solve
 namespace Lean.Elab.Tactic.Grind

src/Lean/Elab/Tactic/Impossible.lean

@@ -32,10 +32,7 @@ private def mkImpossibleNegType (mainGoal : MVarId) (goalType : Expr)
     (cfg : Parser.Tactic.ImpossibleConfig) :
     MetaM (Expr × Array Name) := mainGoal.withContext do
   let dummy ← mkFreshExprSyntheticOpaqueMVar goalType
-  let cleaned ← dummy.mvarId!.cleanup
-  let (_, reverted) ← cleaned.revert
-    (clearAuxDeclsInsteadOfRevert := true)
-    (← cleaned.getDecl).lctx.getFVarIds
+  let reverted ← dummy.mvarId!.revertAll
   let revertedType ← reverted.getType
   let r ← Closure.mkValueTypeClosure revertedType (mkConst ``True)
     (zetaDelta := false)

src/Lean/Meta/Tactic/Grind.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Attr
-public import Lean.Meta.Tactic.Grind.RevertAll
+public import Lean.Meta.Tactic.Grind.MarkAccessible
 public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.Util
 public import Lean.Meta.Tactic.Grind.Cases

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

@@ -12,7 +12,7 @@ import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.CasesMatch
 import Lean.Meta.Tactic.Grind.Injection
 import Lean.Meta.Tactic.Grind.Core
-import Lean.Meta.Tactic.Grind.RevertAll
+import Lean.Meta.Tactic.Grind.MarkAccessible
 import Init.Grind.Util
 public section
 namespace Lean.Meta.Grind

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

@@ -12,7 +12,7 @@ import Lean.PrettyPrinter
 import Lean.Meta.Tactic.ExposeNames
 import Lean.Meta.Tactic.Simp.Diagnostics
 import Lean.Meta.Tactic.Simp.Rewrite
-import Lean.Meta.Tactic.Grind.RevertAll
+import Lean.Meta.Tactic.Grind.MarkAccessible
 import Lean.Meta.Tactic.Grind.Proj
 import Lean.Meta.Tactic.Grind.ForallProp
 import Lean.Meta.Tactic.Grind.CtorIdx

src/Lean/Meta/Tactic/Grind/RevertAll.lean …an/Meta/Tactic/Grind/MarkAccessible.leansrc/Lean/Meta/Tactic/Grind/RevertAll.lean renamed to src/Lean/Meta/Tactic/Grind/MarkAccessible.lean src/Lean/Meta/Tactic/Grind/RevertAll.lean renamed to src/Lean/Meta/Tactic/Grind/MarkAccessible.lean

@@ -51,21 +51,4 @@ def _root_.Lean.MVarId.markAccessible (mvarId : MVarId) : MetaM MVarId := mvarId
   mvarId.assign mvarNew
   return mvarNew.mvarId!
 
-/--
-Reverts all free variables in the goal `mvarId`.
-**Remark**: Auxiliary local declarations are cleared.
-The `grind` tactic also clears them, but this tactic can be used independently by users.
--/
-def _root_.Lean.MVarId.revertAll (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
-  mvarId.checkNotAssigned `revertAll
-  let mut toRevert := #[]
-  for fvarId in (← getLCtx).getFVarIds do
-    unless (← fvarId.getDecl).isAuxDecl do
-      toRevert := toRevert.push fvarId
-  mvarId.setKind .natural
-  let (_, mvarId) ← mvarId.revert toRevert
-    (preserveOrder := true)
-    (clearAuxDeclsInsteadOfRevert := true)
-  return mvarId
-
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Revert.lean

@@ -66,4 +66,19 @@ def _root_.Lean.MVarId.revertFrom (mvarId : MVarId) (fvarId : FVarId) : MetaM (A
     let fvarIds := (← getLCtx).foldl (init := #[]) (start := localDecl.index) fun fvarIds decl => fvarIds.push decl.fvarId
     mvarId.revert fvarIds (preserveOrder := true) (clearAuxDeclsInsteadOfRevert := true)
 
+/--
+Reverts all free variables in the goal `mvarId`.
+**Remark**: Auxiliary local declarations are cleared.
+-/
+def _root_.Lean.MVarId.revertAll (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
+  mvarId.checkNotAssigned `revertAll
+  let mut toRevert := #[]
+  for fvarId in (← getLCtx).getFVarIds do
+    unless (← fvarId.getDecl).isAuxDecl do
+      toRevert := toRevert.push fvarId
+  let (_, mvarId) ← mvarId.revert toRevert
+    (preserveOrder := true)
+    (clearAuxDeclsInsteadOfRevert := true)
+  return mvarId
+
 end Lean.Meta

tests/elab/impossibleTactic.lean

@@ -1,4 +1,7 @@
 import Lean
+
+set_option linter.unusedVariables false
+
 /-! # Tests for the `impossible` tactic combinator -/
 
 -- Closed goal: the negation has no binders, so the user proves it directly.
@@ -250,3 +253,16 @@ example : 0 = 1 ∧ True := by
   constructor
   impossible by decide
   trivial
+
+-- Test that we don’t run `cleanup` in `impossible`.
+
+/--
+error: unsolved goals
+⊢ False
+---
+trace: ⊢ ¬∀ {α : Type u_1} (xs : List α), xs.length > 0 → xs = [] → False
+-/
+#guard_msgs in
+example (xs : List α) (h : xs.length > 0) : xs ≠ [] := by
+  intro h_empty
+  impossible by trace_state; simp