MVarId.revertAll snags auxiliary declarations, leading to termination issues

[eric-wieser]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Lean.MVarId.revertAll fails to ignore auxiliary declarations if variable is used.

Context

[Broader context that the issue occurred in. If there was any prior discussion on the Lean Zulip, link it here as well.]

Steps to Reproduce

import Lean

open Lean.Elab.Tactic

variable (p q : Prop)
theorem foo (h : p ∧ q) : q ∧ p := by
  run_tac liftMetaTactic1 (·.revertAll)
  sorry

Expected behavior: Goal is ⊢ ∀ (p q : Prop), p ∧ q → q ∧ p, no errors

Actual behavior: Goal is ⊢ ∀ (p q : Prop), p ∧ q → (p ∧ q → q ∧ p) → q ∧ p, and the error is

fail to show termination for
  foo
with errors
failed to infer structural recursion:
Not considering parameter p of foo:
  it is unchanged in the recursive calls
Not considering parameter q of foo:
  it is unchanged in the recursive calls
Cannot use parameter h:
  the type p ∧ q does not have a `.brecOn` recursor

Versions

4.14.0-rc3

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[eric-wieser]

Using clearAuxDecls seems to work, but the implementatoin of revertAll suggests it is supposed to handle this for me.

[nomeata]

So there is a workaround, you are unblocked and this is just™ a matter of misleading API design/documentation?

[eric-wieser]

Yes, I am unblocked, but these lines make me thing this function was intended to operate as I was hoping it would:

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

Lines 17 to 21 in 3752241

	let fvars ← fvarIds.filterMapM fun fvarId => do
	if (← fvarId.getDecl).isAuxDecl then
	return none
	else
	return some (mkFVar fvarId)

Empirically, the current behavior seems to be "ignore leading auxiliary declarations", so I'd lean towards this being a design issue rather than a documentation issue.