Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Controlling unfolding in type theory

Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal

TL;DR

The paper addresses brittleness and fragility in proofs caused by definitional unfolding in dependent type theory. It introduces a surface language for fine-grained, local, and default-opaque unfolding that elaborates into a core calculus TT_P augmented with extension types and proposition symbols, and proves a normalization result to guarantee decidability of type checking. The approach is implemented in theCoolTT proof assistant, with a pathway to Agda, and is argued to be more modular and predictable than existing opacity mechanisms. The work blends practical tooling with deep metatheory—via category-theoretic models, gluing, and synthetic Tait computability—to ensure robust definitional equality reasoning while enabling scalable library organization and reasoning about definitions. Overall, controlled unfolding promises improved modularity, performance, and predictability for large mechanized mathematics.

Abstract

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.

Controlling unfolding in type theory

TL;DR

The paper addresses brittleness and fragility in proofs caused by definitional unfolding in dependent type theory. It introduces a surface language for fine-grained, local, and default-opaque unfolding that elaborates into a core calculus TT_P augmented with extension types and proposition symbols, and proves a normalization result to guarantee decidability of type checking. The approach is implemented in theCoolTT proof assistant, with a pathway to Agda, and is argued to be more modular and predictable than existing opacity mechanisms. The work blends practical tooling with deep metatheory—via category-theoretic models, gluing, and synthetic Tait computability—to ensure robust definitional equality reasoning while enabling scalable library organization and reasoning about definitions. Overall, controlled unfolding promises improved modularity, performance, and predictability for large mechanized mathematics.

Abstract

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.
Paper Structure (44 sections, 11 theorems, 19 equations, 3 figures)

This paper contains 44 sections, 11 theorems, 19 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Contributions
  3. Outline
  4. A surface language with controlled unfolding
  5. A simple dependency: length-indexed vectors
  6. Transitive unfolding
  7. Recovering unconditionally transparent/opaque definitions
  8. Unfolding within the type
  9. Unfolding within subexpressions
  10. Controlling unfolding with extension types
  11. A core calculus with proposition symbols
  12. Elaborating controlled unfolding to our core calculus
  13. The elaboration algorithm
  14. The core calculus TT_P
  15. Signatures over TT_P
  16. ...and 29 more sections

Key Result

Proposition 10

Let $\mathbb{T}$ be the free category with representable maps generated by a given logical framework signature; then the groupoid of CwR functors $\hom _{\DelimProtect{\CWR}} \DelimPrn{\mathbb{T},\mathcal{E}}$ is equivalent to the groupoid of interpretations of the signature within $\mathcal{E}$.

Figures (3)

  • Figure 1: The non-standard aspects of the LF signature for .
  • Figure 2: Selected rules from the definition of $\Nf$, $\Ne$, and $\NfTy$.
  • Figure 3: The normalization structure on the universe.

Theorems & Definitions (46)

  • Remark 1
  • Remark 2
  • Remark 3
  • Remark 4
  • Remark 5
  • Remark 6
  • Definition 7
  • Definition 8
  • Definition 9
  • Proposition 10
  • ...and 36 more