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. Even though the unfold tactic mostly works in the base case(s), 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

Created [21 Feb 2025]