What's a non-easy whnf?

Stream: lean4

[Kevin Buzzard]

I'm looking at before/after traces after a change in mathlib's typeclass system and I see that I have made some Non-easy whnfs disappear. FWIW the diff looks like this:

5426,5432c5426,5427
<                 [Meta.whnf] [21.000000] Non-easy whnf: SMulZeroClass M A
<                 [Meta.whnf] [21.000000] Non-easy whnf: AddZeroClass A
<                 [Meta.whnf] [21.000000] Non-easy whnf: DistribSMul M A
<                 [Meta.whnf] [21.000000] Non-easy whnf: SMul M A
<                 [Meta.whnf] [21.000000] Non-easy whnf: Zero A
<                 [Meta.whnf] [21.000000] Non-easy whnf: SMulZeroClass M A
<                 [Meta.isDefEq] [11491.000000] ✅️ (Algebra.id (MvPolynomial σ R)).toSMul =?= instDistribSMul.toSMul
---
>                 [Meta.isDefEq] [10411.000000] ✅️ (Algebra.id
>                         (MvPolynomial σ R)).toSMul =?= Mul.toSMul' (MvPolynomial σ R)

(the change is that the RHS of the =?= is now different). I doubt this is much to fuss about, 21.000000 mheartbeats is nothing, but I was wondering what I'd done. I know I'm just supposed to read the source code but it's meaningless to me. I found lean4#3774 which will presumably tell some people what the answer is, but the PR has no description.

[Edward van de Meent]

i think (from reading the PR) that a non-easy whnf is one which hasn't been cached before?

[Kyle Miller]

The easy whnfs are:

• those that are already in the whnf cache, so don't need to be recomputed
• expressions that are obviously already in WHNF (foralls, unapplied lambdas, universes, and literals)
• expressions that are let-defined free variables or assigned metavariables and after unfolding them they're easy whnfs

[Kyle Miller]

For example, SMulZeroClass M A is not an easy whnf since it's a constant application. Deciding if it's in WHNF requires details about the definition SMulZeroClass.

[Kyle Miller]

Easy/non-easy doesn't seem particularly relevant here; my understanding is that the new isDefEq problem after the typeclass changes is easier(*) for isDefEq to resolve: it's asking for fewer things to be put in WHNF.

(*) At least in terms of number of WHNF calculations.

[Edward van de Meent]

Kyle Miller said:

For example, SMulZeroClass M A is not an easy whnf since it's a constant application. Deciding if it's in WHNF requires details about the definition SMulZeroClass.

reading your explanation, maybe it'd be more relevant to say "deciding what the WHNF is requires details"? because although it is true, it could still be an easy whnf if it's been cached?

[Kyle Miller]

I was imprecise saying that cached results are "easy". It's an explanation for what skips the "Non-easy whnf" trace message.

For my comment about requiring details, that's more an explanation of my understanding of the design of this part of the WHNF reducer. In the end, an "easy case" is what whnfEasyCases is implemented to handle. I don't think there's any technical definition beyond the practical implementation.