In a small-step semantics with a deterministic reduction strategy, refocusing is a transformation that connects a reduction-based normalization function (i.e., a normalization function that enumerates the successive terms in a reduction sequence -- the successive reducts) and a reduction-free normalization function (i.e., a normalization function that does not construct any reduct because all the reducts are deforested). This transformation was introduced by Nielsen and the author in the early 2000's with an informal correctness proof. Since then, it has been used in a variety of settings, starting with Biernacka and the author's syntactic correspondence between calculi and abstract machines, and several formal proofs of it have been put forward. This article presents a simple, if overdue, formal proof of refocusing that uses the Coq Proof Assistant and is aligned with the simplicity of the original idea.

翻译：在具有确定性归约策略的小步语义中，重聚焦是一种将基于归约的规范化函数（即枚举归约序列中连续项——连续归约子的规范化函数）与无归约的规范化函数（即不构造任何归约子，因为所有归约子已被去森林化的规范化函数）联系起来的变换。该变换由Nielsen与作者于21世纪初提出，并附有非形式化的正确性证明。此后，它被应用于多种场景，始于Biernacka与作者关于演算与抽象机器之间句法对应性的研究，并涌现了多个形式化证明版本。本文提出了一个简洁但迟来的重聚焦形式化证明，该证明使用Coq证明助手实现，且与原始思路的简洁性保持一致。