Identifiers in auto-tactics don't respect lexical scope

[david-christiansen]

Prerequisites

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

• [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [X] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [X] 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

PR #3328 began allowing identifiers in auto-tactics, a much-desired feature. But these identifiers don't respect lexical scope/hygiene.

Steps to Reproduce

1. Create a file with the definition from the test case in #3328:

   def f3 (x y : Nat) (h : x = y := by exact Eq.refl x) : Nat :=
   x + x
   

2. Run the test with a local name other than x:

   #check fun someNameOtherThanX => f3 someNameOtherThanX someNameOtherThanX
   

Expected behavior: I would expect the test to pass, because x is bound by the function's parameter named x. Lean's tactic language usually respects lexical scope.

Actual behavior: Elaboration fails with the message unknown identifier 'x'

Versions

This is present in the 4.9 release, as well as 4.11.0-nightly-2024-07-01 on live.lean-lang.org.

Impact

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

[digama0]

This seems unlikely to work, especially if you consider that you can also call f3 (1 + 1) 2, at which point it's not clear what name x is supposed to be. The "correct" behavior in this particular case would be to treat x in the auto tactic not as a name but rather a reference to the previous expression and subject to substitution like regular expressions, but I don't think tactics allow that. Perhaps you can hack it in by adding let x := 1 + 1 into the local context in which to run the tactic, but that can have other side effects and it's not obviously the right behavior.

[david-christiansen]

It's definitely tricky, and I agree that there isn't an obviously right semantics. But we do need to explain to people how to use this at some point.

What is the specification for the current behavior? Is it that names in the script are resolved in the global context immediately prior to the definition, or is it that they're resolved unhygienically at the use site? The former seems like something we can document our way out of, but the test here seems to indicate the latter, which strikes me as unpredictable.

[nomeata]

Putting the assignment x := 1+1 into the local context before elaborating the tactic seems to be most correct behavior to me, if it can be made to work. The other semantics discussed here seem rather weird.

[mhuisi]

Another issue related to this feature is that these identifiers now show up in the .ilean files at the call-sites of those functions. E.g. IO.waitAny has a parameter (h : tasks.length > 0 := by exact Nat.zero_lt_succ _) and Nat.zero_lt_succ now shows up in the .ilean files of all call-sites of IO.waitAny, effectively breaking language server support for that function (e.g.: when hovering over the identifier, it displays an incorrect span, go to definition doesn't immediately take you to IO.waitAny but requires you to choose between Nat.zero_lt_succ and IO.waitAny, "find references" shows the references of both identifiers, etc.).