We present a new way to control the unfolding of definitions in dependent type theory. Traditionally, proof assistants require users to fix whether each definition will or will not be unfolded in the remainder of a development; unfolding definitions is often necessary in order to reason about them, but an excess of unfolding can result in brittle proofs and intractably large proof goals. In our system, definitions are by default not unfolded, but users can selectively unfold them in a local manner. We justify our mechanism by means of elaboration to a core theory with extension types -- a connective first introduced in the context of homotopy type theory -- and by establishing a normalization theorem for our core calculus. We have implemented controlled unfolding in the cooltt proof assistant, inspiring an independent implementation in Agda.

翻译：我们提出了一种在依赖类型理论中控制定义展开的新方法。传统上，证明辅助工具要求用户预先确定每个定义在后续开发中是否会被展开；展开定义通常是进行推理的必要条件，但过度展开会导致证明脆弱且证明目标变得难以处理。在我们的系统中，定义默认不展开，但用户可以局部地选择性地展开它们。我们通过将系统精化到具有扩展类型（一种最初在同伦类型理论中引入的连接词）的核心理论，并为核心演算建立标准化定理，从而验证了我们机制的合理性。我们已在cooltt证明助手中实现了受控展开功能，并启发了Agda中的独立实现。