whnf variant which preserves let-bindings

Stream: metaprogramming / tactics

[Heather Macbeth]

Is there a variant of whnf(R) which does not unfold a variable a which has been defined previously using let a := ...? (I believe this is the "zetaDelta" kind of let, but I may be wrong about the naming.)

I would still like it to see through mdata, perform beta-reduction and look inside abbrevs. I tried e.consumeMData.headBeta, but (in retrospect, predictably) this managed the first two but not the third.

[Heather Macbeth]

Related: is there a version of isDefEq which doesn't see through this kind of "let"?

[Jovan Gerbscheid]

There is docs#Lean.Meta.whnfCore, which takes a configuration argument. In this configuration you can set zetaDelta := false. whnfCore is a somewhat weaker version of whnf, which doesn't unfold constants. (you can see this in how it is used in the definition of whnf at docs#Lean.Meta.whnfImp). Since you want to still look through abbrevs, you would have to do this manually. For example, this is a function in the DiscrTree, which also unfolds abbrevs and does eta reduction:

partial def reduce (e : Expr) (config : WhnfCoreConfig) : MetaM Expr := do
  let e ← whnfCore e config
  match (← unfoldDefinition? e) with
  | some e => reduce e config
  | none => match e.etaExpandedStrict? with
    | some e => reduce e config
    | none   => return e

To make sure you only unfold abbrevs, remember to use docs#Lean.Meta.withReducible.

[Jovan Gerbscheid]

Unfortunately you can't set this configuration for isDefEq.

[Heather Macbeth]

Thanks, Jovan! That's helpful.

I realised that to do an isDefEq which treats lets as black boxes I could do something like

• save state
• clear the values of all the local definitions (docs#Lean.MVarId.clearValue)
• get the result of isDefEq
• restore the state

This seems a bit hacky but maybe it would work -- is there anything that could go wrong with this approach?

[Notification Bot]

54 messages were moved from this topic to #metaprogramming / tactics > isDefEq variant which preserves let-bindings by Heather Macbeth.

[Heather Macbeth]

Returning to Jovan's idea of using whnfCore e (config := { zetaDelta := false }) (perhaps with tricks to handle abbrevs, etc.) to get "whnf which preserves let-bindings" ....

I noticed that whnf is an extern, which I think means the real implementation is in the C code, whereas whnfCore is implemented in Lean. Does this mean I should expect worse performance if I switch from whnf to whnfCore?

[Jovan Gerbscheid]

There are a couple functions such as whnf which look like they are implemented in C, but they are actually implemented in Lean. So if you see for example @[extern 6 "lean_whnf"], then you should search in the lean source code for the string lean_whnf, which will lead you to find its definition:

@[export lean_whnf]
partial def whnfImp (e : Expr) : MetaM Expr :=
  withIncRecDepth <| whnfEasyCases e fun e => do
    let useCache ← useWHNFCache e
    match (← cached? useCache e) with
    | some e' => pure e'
    | none    =>
      withTraceNode `Meta.whnf (fun _ => return m!"Non-easy whnf: {e}") do
        checkSystem "whnf"
        let e' ← whnfCore e
        match (← reduceNat? e') with
        | some v => cache useCache e v
        | none   =>
          match (← reduceNative? e') with
          | some v => cache useCache e v
          | none   =>
            match (← unfoldDefinition? e') with
            | some e'' => cache useCache e (← whnfImp e'')
            | none => cache useCache e e'

[Kyle Miller]

We use whnfCore when we want to do whnf with just the rules of lambda calculus

[Kyle Miller]

It's like whnf if there were a transparency setting below reducible

[Jovan Gerbscheid]

So from the definition of whnfImp, we can see whnf is just whnfCore + unfoldDefinition + reduceNative? + reduceNat? and with some caching

[Heather Macbeth]

Jovan Gerbscheid said:

There are a couple functions such as whnf which look like they are implemented in C, but they are actually implemented in Lean. So if you see for example @[extern 6 "lean_whnf"], then you should search in the lean source code for the string lean_whnf, which will lead you to find its definition:

Thanks! How would I tell the difference between this and a function that is actually implemented in C? Do I just have to search the codebase for @[export lean_whnf], and if nothing turns up then it means that it's implemented in C?

[Jovan Gerbscheid]

Yeah, that's what I do. Actually I think the only ones I know of where the definition is in a different file are defined right after opaque whnf in the same file (inferType, isExprDefEqAux, isLevelDefEqAux, synthPending)

[Jovan Gerbscheid]

And MVarId.checkedAssign in the same file.

[Heather Macbeth]

I know the FRO is generally hesitant to make changes to really foundational pieces of Lean, but it really seems to be very easy to provide a whnfImp variant which takes an optional docs#Lean.Meta.WhnfCoreConfig argument: only the calls to whnfEasyCases and whnfCore need to be changed, and these both already admit an optional WhnfCoreConfig argument. (And then whnfImp itself could be a one-line specialization of the variant.)

@Kyle Miller (or another FRO employee), do you think core would consider making this change? There is a lot of algebraic automation in Lean in which (I believe) it is preferable for lets to be preserved, for much the same reasons that were advanced in lean4#2682 in favour of simp preserving lets. For example, I think ring_nf and abel_nf would ideally preserve lets. See #19120.

I can open an issue on the Lean 4 repo, but first wanted to check whether this change would be considered at all.

[Joachim Breitner]

Didn't look closely, but isn't it maybe the case that Leo happens to be working on exactly that, independent of this discussion? https://github.com/leanprover/lean4/pull/6053

[Jovan Gerbscheid]

Yes, very nice. I see that this PR adds the whnfCoreConfig options into the configuration of the MetaM monad instead of passing them as an explicit argument to whnfCore

[Heather Macbeth]

Thanks for pointing this out! That's a big PR of Leo's and it seems that this change I had hoped for is just a side effect -- do you know what the main point of the PR is?

[Heather Macbeth]

Do I understand correctly that (among other things) that PR would enable both the two things I asked about: turning off zetaDelta in whnf and also in isDefEq?

[Jovan Gerbscheid]

It looks to me like that is exactly the point: global configurability of reductions like zetaDelta, so that these can be set in functions like isDefEq.

[Heather Macbeth]

That's great!

[Heather Macbeth]

Have there been previous discussions of this point, or other places where people requested this feature? I hadn't noticed any.

[Kyle Miller]

This is an independent development, as part of some performance and correctness improvements

[Heather Macbeth]

Interesting ... looking through recent PRs I see lean4#6051, lean4#6054, lean4#6072 -- are they related? So this is something to do with simp performance?

[Kyle Miller]

Yes, they're related. My understanding is that we need zetaDelta to be set in a consistent way to make sure the discrimination tree can index local hypotheses correctly.

[Heather Macbeth]

Is this (indirectly) a consequence of lean4#2682, then? Giving simp a zetaDelta flag ended up requiring that all the core metaprogramming machinery have a zetaDelta flag too?

[Jovan Gerbscheid]

@Heather Macbeth, do you want to continue with #19120? I think you can remove the function whnfWithConfig, and instead just add a withConfig ({. with zetaDelta := false }) to the whnf.