simp destroys let bindings in projection

Stream: lean4

[Tomas Skrivan]

When you turn off zeta simp still destroys let bindings inside of projection application.

mwe

example :
    (let a := id 7
     let b := a + 42
     (a,b)).2
    =
    let a := id 7
    let b := a + 42
    b
    := by
  conv =>
    lhs
    simp (config := {zeta := false}) only []
    trace_state

prints id 7 + 42 but I'm expecting

    let a := id 7
    let b := a + 42
    b

Is this intended behavior or is that considered as a bug?

[Tomas Skrivan]

Ohh I just found out that setting proj:=false fixes this. I clearly misunderstood this option and never tried it until now.

[Kyle Miller]

I think what's happening is that when proj := true then the projection function is being unfolded, but to unfold it it has to put the argument into whnf. This is independent of zeta, which is just about whether simp itself will eliminate a let.

Here's the simp reduction code: https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Tactic/Simp/Main.lean#L149

[Kyle Miller]

Maybe if there were a way to have simp configure docs#Lean.Meta.WhnfCoreConfig you could turn this kind of zeta reduction off too, while still keeping projection reduction.

[Tomas Skrivan]

Another approach is to pull let bindings out of applications.

In my own fork of simp I implemented different version of reduceProjFn? but updating to lean4:v4.6.0-rc1 broke everything. So now I'm trying to figure out an approach without forking simp :)

[Kyle Miller]

I suppose you could use the mathlib lift_lets for that

[Kyle Miller]

That could also probably be a pre-simproc. You'd have to decide how deep into an expression you want to look for lets though, if you care about quadratic performance.

[Tomas Skrivan]

Yeah I experimented with it. I'm afraid that as I'm already running simp, calling lift lets might add extra power to the O(n^*)

[Tomas Skrivan]

Hmm limiting the depth of lift_lets is a good idea!

[Tomas Skrivan]

However, I'm also doing few extra stuff though. For example, I'm splitting let binding of structure constructors into multiple let bindings. And I'm doing it as pre-simproc now as you suggest.