Unqualified unfold no longer works

Stream: lean4

[Craig McLaughlin]

I updated a project to align with Mathlib @ lean-v4.13.0-rc3 and now I get an error ("failed to unfold 'formula' ...") where I didn't before with unfolding a definition:

def formula := True

theorem test (formula: formula) : True := by
  unfold formula at formula

The strange thing is I am not getting this error if I use the above snippet in another project with the same Mathlib version. I suspect there might be something with caching in the .lake directory...any pointers?

Things I've tried which did not resolve the issue:

• Deleting the .lake directory and executing lake update;
• Placing the above snippet in its own file with no imports;

[Kyle Miller]

The issue is that unfold now lets you unfold local variables, and it's trying to unfold formula the local variable in formula.

Here are two different fixes:

theorem test (formula: formula) : True := by
  unfold _root_.formula at formula

theorem test (form : formula) : True := by
  unfold formula at form

[Kyle Miller]

I would suggest not having local variables that shadow global names

[Kyle Miller]

Thanks for the report. lean4#5815 has a better error message:

image.png

[Kyle Miller]

(I don't know why you are seeing the caching issue)

[Craig McLaughlin]

Thanks for the clarification and the quick patch!

1. When would there be confusion between the two instances of formula that would prevent Lean from figuring which one is meant from the context? In your pull request the usage is unfold x which I agree could be confusing but surely:

def X := Nat

theorem test (X : X) : X + 1 = 1 := by
  unfold X at X

is not ambiguous as to which X is meant to be unfolded? I agree in principle that shadowing names is bad practice but I think my actual use case makes the proof easier to read;

2. This change to unfold doesn't explain why I only see the error in one development and not the other (Does this point to a separate issue?);
3. Is unfold_let now superfluous?

[Kyle Miller]

1. It's using the normal name resolution to figure out which X to refer to. I suppose in principle it could use the rule "only refer to names that come from before the local variable X was defined" if you do unfold ... at X
2. Are you doing it from a blank file in each case? Or is there other context?
3. Mostly, though unfold_let can interleave unfoldings. With unfold you might need to do unfold x y x for example. In any case, improvements made to dsimp only [x, y] a few versions back makes unfold_let totally superfluous.

[Craig McLaughlin]

1. I assume a binding cannot depend on itself but I don't have a good idea on how difficult that would be to implement (or if it even is of interest to others);
2. Yes. In fact, I just did lake new unfold-test and pasted the snippet for X := Nat above into the Basic.lean; I get no error and it unfolds the type X to Nat in the context of the hypothesis X (might be worth noting that the 'Expected Type' section of my Goal buffer still mentions _root_.X);
3. Ah, good to know. Thanks!

[Kyle Miller]

For 2, what's the output of #eval Lean.versionString for both projects?

[Craig McLaughlin]

For the projects which do not report an error (e.g. unfold-test) this string is "4.12.0-rc1" and for the other project which does report an error it is "4.13.0-rc3". Which would certainly explain the discrepancy but other things I tried: M-x lean4-show-version and elan show imply all projects are using Lean 4.13.

/unfold-test$ elan show
...
active toolchain
----------------

leanprover/lean4:v4.13.0-rc3 (overridden by '/unfold-test/lean-toolchain')
/unfold-test$ cat lean-toolchain
leanprover/lean4:v4.13.0-rc3

How do I switch them to the latest version?

[Kim Morrison]

I didn't exactly follow what's going on above, but 99% of the time the way to change the version being used it to directly edit lean-toolchain.

[Craig McLaughlin]

That's what the cat command was for in the above code snippet; I've edited lean-toolchain to the v4.13.0-rc3 release. Then I called lake update but nothing has changed (I still do not get the expected error, and the eval command produces the wrong compiler version). What is the other 1%? Or can you think of any other step I might have missed?

[Kim Morrison]

Are you downstream of Mathlib?

[Kim Morrison]

If so, running lake update will have the effect of overwriting your lean-toolchain with the lean-toolchain from Mathlib.

[Kim Morrison]

So in this case you need to edit your lakefile to tell it to use a commit of Mathlib which is on v4.13.0-rc3.

[Kim Morrison]

But if this is what is affecting you, you should be able to see that by checking if lean-toolchain changed after running lake update.