Eta-expansion using Lean.Meta.transform

Stream: lean4

[Joachim Breitner]

Here is a little puzzle: Using docs#Lean.Meta.transform, given a function name f, eta-expand every occurrence of fn that does not already have two arguments.

This means to also eta expand a single f as in (id f). But it seems neither with pre nor with post, when looking at a .const f, I can easily tell whether it is part of an application (and my not need to be eta-expanded), or if it is really a lone occurrence (which I do have to eta-expand).

[Mario Carneiro]

You can do it at the cost of not being able to share the cache between nested invocations in some cases. in pre, check if it is an application of fn. If so, recursively call transform on the arguments of fn, eta expand if there are fewer than two arguments, and then return .done. Otherwise return .continue.

[Joachim Breitner]

Hmm, true, but not quite satisfying, due to the missed cache and loss of elegance. For now I just added a flag to transform to not call post twice on f a b, I'll see if that's acceptable during code review.

[Mario Carneiro]

another possibility is to call transform.visit directly and do the setup outside / in a transform.run function

[Kyle Miller]

@Joachim Breitner Here's the mathlib implementation of eta expansion for the eta_expand tactic: https://github.com/leanprover-community/mathlib4/blob/a2ca43e594f2f3d1ccbb2cf178fd5800abc61321//Mathlib/Tactic/DefEqTransformations.lean#L180

While I'm not sure the algorithm is completely correct, it uses transform in the way Mario suggested.