Execute `headBeta` on all local decl

Stream: metaprogramming / tactics

[Leni Aniva]

Is there a way to execute Expr.headBeta on all local declarations?

Sometimes I see a local declaration of this type:

b : (fun x => ...) y

and I want to eliminate them. e.g. b would be typed b : ...[x/y] instead.

The reason is the apply tactic seems to really struggle with applying b when its type of the form

(fun x => (forall z, ...)) y

and it loses track of goals that it produces.

[Patrick Massot]

Does the tactic beta_reduce at * work for you?

[Leni Aniva]

Patrick Massot said:

Does the tactic beta_reduce at * work for you?

I need a vanilla metaprogramming solution ):

[Jireh Loreaux]

docs#Lean.Core.betaReduce (which is the ultimate implementation of beta_reduce) is pretty vanilla.

[Leni Aniva]

Jireh Loreaux said:

docs#Lean.Core.betaReduce (which is the ultimate implementation of beta_reduce) is pretty vanilla.

and I would have to execute this on every fvar of local declarations? Is there a way to run a function to modify local decls?

[Patrick Massot]

Did you try to find a tactic doing something similar that you could use as inspiration?

[Leni Aniva]

Patrick Massot said:

Did you try to find a tactic doing something similar that you could use as inspiration?

Therei is beta_reduce. If there's no simpler infrastructure I'll just copy its implementation

[Patrick Massot]

I was referring to your question about modifying every local declaration.

[Leni Aniva]

[Quoting…]

beta_reduce does it, but it doesn't rely on vanilla Lean functions

[Jireh Loreaux]

You can have a look in the metaprogramming book. This section describes how to loop through the local context, among other things.