`ClearExcept` (`clear * -`) clears invisible auxiliary declarations (`isAuxDecl`) including recursive hypotheses

[oliver-butterley]

Following the Zulip discussion: (#general > ClearExcept clears even if isAuxDecl, is this intended?).

Motivation

When writing a recursive proof in tactic mode, Lean places the recursive hypothesis in the local context as an auxiliary declaration (LocalDecl.isAuxDecl). This declaration is:

• Completely invisible in the Infoview (even with all display options enabled)
• Required for the recursive call to elaborate

The clear * - tactic (Mathlib.Tactic.ClearExcept) iterates over all declarations in the local context and clears everything not in the explicit keep set or a type-class instance. It does not check isAuxDecl, so it silently clears the recursive hypothesis. While the hypothesis can technically be added to the keep set by name, it is not shown in the Infoview, making it easy to overlook.

In simple examples this is never an issue, we found the inconvenience when working with software verification where the context gets huge and needs clearing for performance and where the recursive goals are closed by automation and so it is easy to overlook the need to explicitly add the name of the theorem to the exclude list.

Minimal reproduction

import Mathlib.Tactic.ClearExcept

def myLen : List α → Nat
  | [] => 0
  | _ :: xs => myLen xs + 1

-- This fails: `clear * - xs` removes the invisible recursive hypothesis.
theorem myLen_eq_length : ∀ (l : List α), myLen l = l.length
  | [] => by simp [myLen]
  | _ :: xs => by
    simp [myLen]
    clear * - xs
    exact myLen_eq_length xs

Without clear * -, the proof works fine. It also works fine if myLen_eq_length is added to the clear * - list but myLen_eq_length is never shown in the info view.

Expected behaviour (in my opinion)

clear * - should skip auxiliary declarations by default, the same way it already skips type-class instances. Auxiliary declarations are internal bookkeeping and should not be touched by a user-facing "clear everything" tactic.

Proposed fix

In Mathlib.Tactic.ClearExcept.getVarsToClear, add decl.isAuxDecl to the skip condition:

 def getVarsToClear (preserve : Array FVarId) : MetaM (Array FVarId) := do
   let mut toClear : Array FVarId := #[]
   for decl in ← getLCtx do
-    unless preserve.contains decl.fvarId do
+    unless preserve.contains decl.fvarId || decl.isAuxDecl do
       if let none ← isClass? decl.type then
         toClear := toClear.push decl.fvarId
   return toClear

PR with proposed fix: #36723