Controlling unfolding in type theory

10/11/2022
by   Daniel Gratzer, et al.
0

We present a novel mechanism for controlling the unfolding of definitions in dependent type theory. Traditionally, proof assistants let users specify whether each definition can or cannot 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 type theory with extension types, a connective first introduced in the context of homotopy type theory. We prove a normalization theorem for our core calculus and have implemented our system in the cooltt proof assistant, providing both theoretical and practical evidence for it.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset