Identifiers in auto-tactics don't respect lexical scope

david-christiansen commented 5 days ago

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

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

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 commented 5 days ago

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 commented 4 days ago

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 commented 4 days ago

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.

leanprover / lean4