  The compactness lemma in programming language theory states that any
recursive function can be simulated by a finite unrolling of the function. One
important use case it has is in the logical relations proof technique for
proving properties of typed programs, such as strong normalization. The
relation between recursive functions and their finite counterparts is a special
variant of the class of bisimulation relations. However, standard bisimulation
proof approaches do not apply to the compactness lemma as properties of the
relation vary over execution. As a result, the proof of compactness is often
messy because the multiple copies made of the recursive function during
execution can be unrolled an inconsistent number of times. We present a new
proof technique by indexing the bisimulation relation over the step transitions
and utilizing an intermediate "pattern" language to mechanize bookkeeping. This
generalization of "pattern stepping bisimulation" obviates the need for
contextual approximation within the compactness lemma, and thus extends the
compactness lemma to a wider range of programming languages, including those
that incorporate control flow effects. We demonstrate this approach by formally
verifying the compactness lemma within the Coq theorem prover in the setting of
explicit control flow and polymorphism.
