whnf and equation compiler

Stream: metaprogramming / tactics

[Chase Norman]

When I whnf reduce x + (y.succ), Lean is miraculously able to provide me (x.add y).succ, managing at once to evaluate the definitional equality of Nat.add without unfolding it. As I understand it, this is thanks to the equation compiler, which generates Nat.add.eq_1 and Nat.add.eq_2.

I am looking to write my own code performing reductions in the same way as whnf, using these equalities. It is not clear to me if the equations generated by the equation compiler (1) always have a standard form (the function applied by either universally quantified variables or a constructor application?), (2) have an algorithm to determine whether one of these equalities applies in a given context, (3) are exclusively definitional equalities, etc.

Essentially, I am looking for a better understanding of how Lean internally represents the reduction behavior of these functions without resorting to definition unfolding and the ReductionRules of the recursor. Thanks!

[Mario Carneiro]

Chase Norman said:

When I whnf reduce x + (y.succ), Lean is miraculously able to provide me (x.add y).succ, managing at once to evaluate the definitional equality of Nat.add without unfolding it. As I understand it, this is thanks to the equation compiler, which generates Nat.add.eq_1 and Nat.add.eq_2.

Actually it is not those equations, but rather "smart unfolding" which does this party trick, that is, Nat.add._sunfold

[Chase Norman]

Ah... I was beginning to suspect that it was something to do with Nat.add. I couldn't reproduce it with my own add definition. Do you think it is possible at all to have a definitional reduction scheme that relies directly on the output from the equation compiler?

[Mario Carneiro]

the way it works is that Nat.add._sunfold is a definition with the same type as Nat.add but defined using a series of matches terminated by other things. If reducing Nat.add._sunfold applied to the given arguments reduces away the matches, then it is asserting that the result is defeq to Nat.add applied to those same arguments and the result is the desired re-folded expression

[Mario Carneiro]

in this case, Nat.add._sunfold x y.succ reduces to (Nat.add x y).succ so that's what we should make Nat.add x y.succ unfold to

[Mario Carneiro]

So the smart unfolding definition is kind of like all of the equations all packed together in one definition, but expressed as a case tree instead of just a list

[Edward van de Meent]

curiously, Nat.add._sunfold is what i kind of expected Nat.add to be by definition...

[Edward van de Meent]

but it's different

[Mario Carneiro]

well, it couldn't be because Nat.add._sunfold is using non-recursive case splitting

[Mario Carneiro]

note that it calls Nat.add and not Nat.add._sunfold again

[Edward van de Meent]

oh ahhhhh
right, they're not the same

[Edward van de Meent]

so in a sense, Nat.add._sunfold models unfolding Nat.add for a single step.