Lack of smart unfolding was a feature

[Kha]

I had even mentioned it on our course slides! :)

For the sake of consistency with the base tactics, I would suggest:

• norm simp f should do smart unfolding, like simp [f]
• norm unfold f should do unconditional unfolding, like unfold f

[JLimperg]

I'm finally getting to this, sorry for the very long wait. Looking at how to best implement this, I'm quite confused by all these different unfolding methods. My understanding so far:

• unfold uses the equation from getUnfoldEqnFor?. It performs a special simp call which applies the equation and reduces any resulting match statement(?) in a pre method (why in a pre method?). If the equation is not available, it performs a plain delta reduction without any postprocessing.
• simp uses the equations from getEqnsFor? (what's the difference between this and getUnfoldEqnFor??) without any postprocessing for resulting match statements(?). If these equations are available and the def can be smart-unfolded, or if the equations are not available, the def is added to the toUnfold list of SimpTheorems and is subsequently unfolded using unfoldDefinition?, which performs smart unfolding or, if that's not available, plain delta reduction(?).

For simp rules, I can copy the simp logic, which will at least guarantee that we get the same semantics. For unfold rules, I could copy the implementation of unfold, but it would be really inefficient to run this once for each rule. Alternative method: make a simp call which has smart unfolding disabled and which, for each definition f, uses either the equations from getUnfoldEqnFor? f or adds f to the toUnfold list. Add a post method which reduces resulting match statements. Does this give at least somewhat similar semantics?

[Kha]

Sorry for the delay from my side as well :smile: .

why in a pre method?

I don't think it makes a difference.

what's the difference between this and getUnfoldEqnFor??

I'm not really sure to be honest. It looks like an unfold theorem can be "stronger" than any individual equation theorem by combining multiple ones: https://github.com/leanprover/lean4/blob/3a12c99666fad1cf3b060a4a2e71fa8d481c4969/src/Lean/Elab/PreDefinition/Eqns.lean#L320-L322 (@leodemoura?)

without any postprocessing for resulting match statements(?)

The equation theorems should already express the cases of the internal match terms.

unfoldDefinition?, which performs smart unfolding or, if that's not available, plain delta reduction(?).

Yes, I think so.

Add a post method which reduces resulting match statements.

Shouldn't this one be pre so that definitions in unfolded bodies are also unfolded in the same step?