About unfolding calls

Rule of thumb:

• use the unfold tactic on functions that are not defined recursively; and
• use fold-unfold lemmas on functions that are defined recursively.

Systematically stating fold-unfold lemmas for each recursive function (1) clarifies its equational intent and (2) saves a lot of grief later on. For example, consider mystery_function_19 from Week 05: the first thing to do was to state fold-unfold lemmas. Yes, the unfold tactic mostly works in the base case(s), but it mostly does not in the induction step(s). Besides, trying to make do without fold-unfold lemmas makes one lose sight of the unity of the approach, as satisfying as it may feel to engage a fight with clearly belligerent windmills and to re-invent an ad-hoc version of the wheel in order to win that fight.

Version

Extracted this chapter from a chapter about miscellanies [21 Mar 2024]