betaReduce with loose bvars

Stream: lean4

[Dan Velleman]

I have an expression that looks something like ∀ x, (fun y => P y) x ∧ .... I want to change it to ∀ x, P x ∧ .... That's easy enough to do by, basically, taking the expression apart, calling Core.betaReduce on the part that needs to be reduced, and then putting it back together. I've done that, and it seems to work. But the expression I'm passing to Core.betaReduce has the form app (lam y ...) (bvar 0), so it has a loose bvar, and I've read that some functions that operate on expressions can run into problems if you pass an expression with loose bvars. I could avoid the issue by using Meta.withLocalDecl, but it seems like a lot of trouble if it isn't necessary. So my question is: Is there any reason to avoid passing an expression with loose bvars to Core.betaReduce?

[Jannis Limperg]

I don't know about betaReduce in particular, but indeed the Lean API in general is really not a fan of loose bvars. So you might as well learn the 'proper' way to do things like this, which I've described here.

[Dan Velleman]

Oh, I was thinking I would need withLocalDecl, but I see now that telescopes do what I want. Thanks.

But I also realized that, in my particular case, there's a much easier solution. The beta reduction of app (lam y t b bi) (bvar 0) is just b! That's how de Bruijn indices work. So there's no need to call Core.betaReduce at all; just pull out b.