whnf with bvars

Stream: lean4

[Adam Topaz]

I'm trying to understand when I should expect docs#Lean.Meta.whnf to work in the presence of bvars. For example:

import Lean

open Lean

#eval show MetaM Unit from do -- fine
  let e ← Meta.whnf (.forallE `a (.bvar 0) (.bvar 1) .default)
  logInfo (← Meta.ppExpr e)

#eval show MetaM Unit from do -- panic
  let e ← Meta.whnf (.bvar 0)
  logInfo (← Meta.ppExpr e)

The second code block fails with a panic but the first one works fine.

[Kyle Miller]

You should never expect it to work with loose bvars. It might accidentally be ok with them in some cases, but you shouldn't rely on it.

[Adam Topaz]

Ok good to know.

[Adam Topaz]

Is there a standard way to convert bvars to fvars and back?

[Kyle Miller]

Are you in a situation where bvars can't be instantiated with fvars?

[Adam Topaz]

I'm essentially trying to get the whnf of Exprs which are types of parameters of some lambda or a forall.

[Kyle Miller]

If you look through the source for examples of withLocalDecl, instantiate1, and mkForallFvars/mkLambdaFvars, you'll see a design pattern. (On my phone or I might give you a specific example)

[Adam Topaz]

Thanks! I'll take a look at those.

[Kyle Miller]

docs#Lean.Meta.transform might be an example (I'll check after sending this message)

[Kyle Miller]

Yeah, take a look at its visit functions. Maybe you can use this transform function for what you're doing?

[Jannis Limperg]

I think docs#Lean.Meta.forallTelescope and docs#Lean.Meta.lambdaTelescope might be what you're looking for. These 'open up' terms of the form forall (a1 : T1) ... (an : Tn), U, making a1 : T1, ..., an : Tn available as temporary local hypotheses. You can then get Ti via fvarId.getDecl and whnf it.

[Adam Topaz]

Thanks Jannis, I'll try that as well.

[Kyle Miller]

If you're happy with it going through a whole telescope, then those are definitely a good choice rather than using withLocalDecl manually. There are also Bounded variants.

[Adam Topaz]

forallTelescope is working perfectly for my application, but it's a bit cumbersome to extract the name and binder info for each parameter. I can do it by getting the local context and using LocalContext.fvarIdToDecl with various matches, but is there a more direct way?

[Kyle Miller]

You get the name and binder info immediately if you do withLocalDecl yourself (since this is data you have to pass it).

There are some functions in the FVarId namespace you can use rather than obtaining the decl first. For example docs#Lean.FVarId.getBinderInfo and docs#Lean.FVarId.getUserName

[Adam Topaz]

Oh great those two functions will make my life easy :)