revert and variable

Stream: lean4

[Sven Manthe]

@Floris van Doorn and me found a situation, where the tactic revert fails expectedly, but creates a not so nice error message. This also affects the extract_goal tactic of Mathlib, which just passes this message on.

--import Mathlib.Tactic.ExtractGoal

variable {P : Prop}
example
  --{P : Prop} --uncommenting this line fixes the issue
  (S : P → Prop) :
  ∃ (hx : P), S hx := by
  apply Exists.intro
  · --revert P
    --extract_goal
    sorry
  · sorry

[Sven Manthe]

PS: I just realized that uncommenting the parameter line actually makes revert P succeed.

[Joachim Breitner]

For the benefit from away from the computer, whats the error message?

[Floris van Doorn]

tactic 'clear' failed, target depends on '_example'

[Floris van Doorn]

The issue has to do with the fact that the goal contains a metavariable, and this metavariable depends on an auxiliary local constant(?). It is interesting that the behavior changes depending on whether P is an argument or a variable.

[Joachim Breitner]

I wonder if this _example is the name for the current function in case you want to make it recursive. Can you produce this issue with def as well?

[Floris van Doorn]

Yes, with theorem it will give the same error message with the theorem name. It gives the same error message The same error message occurs when writing clear <thmname>

variable {P : Type}
theorem foo
  -- {P : Type} --uncommenting this line fixes the issue
  (S : P → Prop) :
  ∃ (hx : P), S hx := by
  apply Exists.intro
  revert P -- tactic 'clear' failed, target depends on 'foo'
  -- clear foo -- gives same error message, but also fails with P as argument

[Sven Manthe]

Yes, it is the name of the current function (we used a def originally)

[Joachim Breitner]

I see. probably worth recording in an issue.

[Damiano Testa]

Just out of curiosity, what happens if you add nonrec to the declaration? (I have a vague memory that _example is what nonrec uses.)

[Floris van Doorn]

Then the revert succeeds and extract_goal fails with the expected "extracted goal has metavariables" error.
Good point, I forgot about that modifier. That can at least be a workaround.

[Damiano Testa]

Actually, it seems more successful than what I hoped for!

[Kyle Miller]

Weird, I was tried to minimize, and for some unknown reason revert is removing the second goal:

theorem foo (p : Prop) (h : p) : ∃ (n : Nat), p := by
  apply Exists.intro
  revert p
  sorry
-- (kernel) declaration has metavariables 'foo'

(4.10.0, commit 0a1a855ba80e51515570439f3d73d3d9414ac053)

[Sven Manthe]

https://github.com/leanprover/lean4/issues/4886

[Joachim Breitner]

I added a bit more analysis to the issue