Unfold `let`

Stream: metaprogramming / tactics

[Leni Aniva]

Is there a function which turns an .letE expression into one which doesn't begin with a .letE (but can contain them) via repeated substitution?

[Eric Paul]

If I understand you correctly, then docs#Lean.Meta.whnf should do what you are asking for. For example:

import Lean
import Qq
open Lean Meta Qq

/--
info:
let x := 5;
let y := 6;
fun z => z * x * y
---
info:
fun z => z * 5 * 6
-/
#guard_msgs in
run_meta
  let letE := q(let x := 5; let y := 6; fun z => z * x * y)
  Lean.logInfo m!"{letE}"
  Lean.logInfo m!"{←whnf letE}"

[Eric Paul]

Although using whnf may do more computation than you want. The following uses docs#Lean.Meta.expandLet to only substitute the letEs and nothing else.

import Lean
import Qq
open Lean Meta Qq

def expandLetExpr : Expr → Expr
| .letE _ _ v b _ => Meta.expandLet b #[v] (zetaHave := true)
| e => e

/--
info:
let x := 5;
let y := 6;
x * y
---
info:
30
---
info:
5 * 6
-/
#guard_msgs in
run_meta
  let letE := q(let x := 5; let y := 6; x * y)
  Lean.logInfo m!"{letE}"
  Lean.logInfo m!"{←whnf letE}"
  Lean.logInfo m!"{expandLetExpr letE}"

[Jovan Gerbscheid]

If you only want the zeta reduction, a typical way to do this would be something like

match e with
| .letE _ _ v b _ => b.instantiate1 v
| _ => e

And you can do this recursively.

[Kyle Miller]

It's worth taking a look at the code of docs#Lean.Meta.expandLet (what @Eric Paul pointed out). The basic idea is what @Jovan Gerbscheid points out, but it's more efficient — it does instantiation in a single pass once it collects all the let values. The zetaHave parts can be ignored, since it's just for honoring some whnf options.

The efficiency improvement is important for deep let chains; it goes from O(ne) to O(e), where n is the depth of the let chain and e is the size of the expression.