Controlling unfolding in type theory Daniel Gratzer10000000319440789 Jonathan Sterling10000000205855564 Carlo Angiuli20000000295903303 Thierry Coquand30000000254295153 and

2025-04-24 0 0 915.7KB 31 页 10玖币

侵权投诉

Controlling unfolding in type theory

Daniel Gratzer1[0000−0003−1944−0789], Jonathan Sterling1[0000−0002−0585−5564],

Carlo Angiuli

2[0000−0002−9590−3303]

, Thierry Coquand

3[0000−0002−5429−5153]

, and

Lars Birkedal1[0000−0003−1320−0098]

1Aarhus University

2Carnegie Mellon University

3Chalmers University

Abstract.

We present a novel mechanism for controlling the unfolding

of deﬁnitions in dependent type theory. Traditionally, proof assistants

let users specify whether each deﬁnition can or cannot be unfolded in

the remainder of a development; unfolding deﬁnitions 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, deﬁnitions

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 ﬁrst 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.

1 Introduction

In dependent type theory, terms are type checked modulo deﬁnitional equality,

a congruence generated by

-, and

-laws, as well unfolding of deﬁnitions.

Unfolding deﬁnitions is to some extent a convenience that allows type checkers

to silently discharge many proof obligations, e.g. a list of length 1 + 1 is without

further annotation also a list of length 2. It is by no means the case, however,

that we always want a given deﬁnition to unfold:

–

Modularity: Dependent types are famously sensitive to the smallest changes

to deﬁnitions, such as whether

(+)

recurs on its ﬁrst or its second argument.

If we plan to change a deﬁnition in the future, it may be desirable to avoid

exposing its implementation to the type checker.

–

Usability: Although unfolding has the potential to simplify proof states, it also

has the potential to dramatically complicate them, resulting in unreadable

subgoals, error messages, etc. A user may ﬁnd that certain deﬁnitions are

likely to be problematic in this way, and thus opt not to unfold them.

Many proof assistants accordingly have implementation-level support for marking

deﬁnitions opaque (unable to be unfolded), including Agda’s

abstract

key-

word [36] and Coq’s Qed command [38].

arXiv:2210.05420v1 [cs.LO] 11 Oct 2022

2 D. Gratzer et al.

But unfolding deﬁnitions is not merely a matter of convenience: to prove a

property of a function, we must unfold it. For example, if we make the deﬁnition

of the

(+)

function opaque, then

(+)

is indistinguishable from a variable of type

N→N→Nand so cannot be shown to be commutative, satisfy 1 + 1 = 2,etc.

In practice, proof assistants resolve this contradiction by adopting an inter-

mediate stance: deﬁnitions are transparent (unfolded during type checking) by

default, but users are given some control over their unfolding. Coq provides

conversion tactics (

cbv

simpl

,etc.) for applying deﬁnitional equalities, each

of which can be annotated with a list of deﬁnitions to unfold; its

Opaque

and

Transparent

commands toggle the default unfolding behavior of a transparent

deﬁnition; and the SSReflect tactic language natively supports a “

lock

ing”

idiom for controlling when deﬁnitions unfold [

]. Agda allows users to group

multiple deﬁnitions into a single

abstract

block, inside of which the deﬁnitions

are transparent and outside of which they are opaque; this allows users to deﬁne

a function, prove all lemmas that depend on how the function was deﬁned, and

then irreversibly make the function and lemmas opaque.

These mechanisms for controlling unfolding are more subtle than they may at

ﬁrst appear. In Agda, deﬁnitions within

abstract

blocks are transparent to other

deﬁnitions in the same block, but opaque to the types of those deﬁnitions; without

such a stipulation, those types may cease to be well-formed when the earlier

deﬁnition is made opaque. Furthermore,

abstract

blocks are anti-modular,

requiring users to anticipate all future lemmas about deﬁnitions in a block—

indeed, the Agda standard library [

] uses

abstract

exactly once at the time of

writing. Coq’s conversion tactics are more ﬂexible than Agda’s

abstract

blocks,

but being tactics, their behavior can be harder to predict. The

lock

idiom in

SSReflect is more predictable because it creates opaque deﬁnitions, but comes

in four diﬀerent variations to simplify its use in practice.

Contributions We propose a novel mechanism for ﬁne-grained control over the

unfolding of deﬁnitions in dependent type theory. We introduce language-level

primitives for controlled unfolding that are elaborated into a core calculus with

extension types [

], a connective ﬁrst introduced in the context of homotopy

type theory. We justify our elaboration algorithm by establishing a normalization

theorem (and hence the decidability of type checking and injectivity of type

constructors) for our core calculus, and we have implemented our system for

controlled unfolding in the experimental cooltt proof assistant [29].

Deﬁnitions in our framework are opaque by default, but can be selectively

and locally unfolded as if they were transparent. Our system is ﬁner-grained and

more modular than Agda’s

abstract

blocks: we need not collect all lemmas that

unfold a given deﬁnition into a single block, making our mechanism better suited

to libraries. Our primitives have more predictable meaning and performance

than Coq’s unfolding tactics because they are implemented by straightforward

elaboration into the core calculus (via new types and declaration forms); we

anticipate that this type-theoretic account of controlled unfolding will also provide

a clear path toward integrating our ideas with future language features.

Controlling unfolding in type theory 3

Our core calculus is intensional Martin-Löf type theory extended with proof-

irrelevant proposition symbols

, dependent products

{p}A

over those proposi-

tions, and extension types

{A|p →a}

whose elements are the elements of

that are deﬁnitionally equal to

under the assumption that

is true. Extension

types are similar to the path types

(Path A a0a1)

of cubical type theory [

which classify functions out of an abstract interval

that are deﬁnitionally equal

to a0and a1when evaluated at the interval’s respective endpoints 0,1 : I.

To justify our elaboration algorithm, we prove a normalization theorem for

our core calculus, characterizing its deﬁnitional equivalence classes of types and

terms and as a corollary establishing the decidability of type checking. Our

proof adapts and extends Sterling’s technique of synthetic Tait computability

(STC) [

], which has previously been used to establish parametricity for an

ML-style module calculus [

] and normalization for cubical type theory [

] and

multimodal type theory [

]. Our proof is fully constructive, an improvement on

the prior work of Sterling and Angiuli [

]; we have also corrected an error in the

handling of universes in an earlier revision of Sterling’s doctoral dissertation [

Outline In Section 2 we introduce our controlled unfolding primitives by way of

examples, and in Section 3 we walk through how these examples are elaborated

into our core language of dependent type theory with proposition symbols

and extension types. In Section 4 we present our elaboration algorithm, and

in Section 5 we discuss our implementation of the above in the

cooltt

proof

assistant. In Section 6 we establish normalization and decidability of type checking

for our core calculus. We conclude with a discussion of related work in Section 7.

2 A surface language with controlled unfolding

We begin by describing an Agda-like surface language for a dependent type

theory with controlled unfolding. In Section 4 we will give precise meaning to

this language by explaining how to elaborate it into our core calculus; for now

we proceed by example, introducing our new primitives bit by bit. Our examples

will concern the inductively deﬁned natural numbers and their addition function:

(+) : N→N→N

ze +n=n

su m+n=su (m+n)

2.1 A simple dependency: length-indexed vectors

In our language, deﬁnitions such as

(+)

are opaque by default—they are not un-

folded automatically. To illustrate the need to selectively unfold

(+)

, consider the

indexed inductive type of length-indexed vectors with the following constructors:

vnil :vec ze A

vcons :A→vec n A →vec (su n)A

4 D. Gratzer et al.

Suppose we attempt to deﬁne the append operation on vectors by dependent

pattern matching on the ﬁrst vector. Our goals would be as follows:

(⊕) : vec m A →vec n A →vec (m+n)A

vnil ⊕v=?:vec (ze +n)A

vcons a u ⊕v=?:vec (su m+n)A

As it stands, the goals above are in normal form and cannot be proved;

however, we may indicate that the deﬁnition of

(+)

should be unfolded within

the deﬁnition of (⊕)by adding the following top-level unfolds annotation:

(⊕)unfolds (+)

(⊕) : vec m A →vec n A →vec (m+n)A

With our new declaration, the goals simplify:

vnil ⊕v=?:vec n A

vcons a u ⊕v=?:vec (su (m+n)) A

The ﬁrst goal is solved with

itself; for the second goal, we begin by applying

the vcons constructor:

vcons a u ⊕v=vcons a?:vec (m+n)A

The remaining goal is just our induction hypothesis

u⊕v

. All in all, we have:

(⊕)unfolds (+)

(⊕) : vec m A →vec n A →vec (m+n)A

vnil ⊕v=v

vcons a u ⊕v=vcons a(u⊕v)

2.2 Transitive unfolding

Now suppose we want to prove that

map

distributes over

(⊕)

. In doing so we will

certainly need to unfold map, but it turns out this will not be enough:

map : (A→B)→vec n A →vec n B

map fvnil =vnil

map f(vcons a u) = vcons (f a) (map f u)

map-⊕unfolds map

map-⊕: (f:A→B) (u:vec m A) (v:vec n A)

→map f(u⊕v)≡map f u ⊕map f v

map-⊕fvnil v=?:map f(vnil ⊕v)≡vnil ⊕map f v

map-⊕f(vcons a u)v

?:map f(vcons a u ⊕v)≡vcons (f a) (map f u)⊕map f v

To make further progress we must also unfold (⊕):

Controlling unfolding in type theory 5

map-⊕unfolds map;(⊕)

map-⊕: (f:A→B) (u:vec m A) (v:vec n A)

→map f(u⊕v)≡map f u ⊕map f v

map-⊕fvnil v=?:map f v ≡map f v

map-⊕f(vcons a u)v=

?:vcons (f a) (map f(u⊕v)) ≡vcons (f a) (map f u ⊕map f v)

In our language, unfolding

(⊕)

has the side eﬀect of also unfolding

(+)

: in

other words, unfolding is transitive. To see why this is the case, observe that

the unfolding of

vcons a u ⊕v

vec (su m+n)A

, namely

vcons a(u⊕v)

vec (su (m+n)) A

, would otherwise not be well-typed. From an implementation

perspective, one can think of the transitivity of unfolding as necessary for subject

reduction. Having unfolded map,(⊕), and thus (+), we complete our deﬁnition:

cong : (f:A→B)→a≡a0→f a ≡f a0

cong freﬂ =reﬂ

map-⊕unfolds map; (⊕)

map-⊕: (f:A→B) (u:vec m A) (v:vec n A)

→map f(u⊕v)≡map f u ⊕map f v

map-⊕fvnil v=reﬂ

map-⊕f(vcons a u)v=cong (vcons (f a)) (map-⊕f u v)

2.3 Recovering unconditionally transparent and opaque deﬁnitions

There are also times when we intend a given deﬁnition to be a fully transparent

abbreviation, in the sense of being unfolded automatically whenever possible. We

indicate this with an abbreviation declaration:

abbreviation singleton

singleton :A→vec (su ze)A

singleton a=vcons avnil

Then the following lemma can be deﬁned without any explicit unfolding:

abbrv-example :singleton 5≡vcons 5vnil

abbrv-example =reﬂ

The meaning of the

abbreviation

keyword must account for unfolding

constraints. For instance, what would it mean to make

map-⊕

an abbreviation?

abbreviation map-⊕

map-⊕unfolds map; (⊕)

. . .

We cannot unfold

map-⊕

in all contexts, because its deﬁnition is only well-

typed when

map

and

(⊕)

are unfolded. The meaning of this declaration must,

therefore, be that

map-⊕

shall be unfolded just as soon as

map

and

(⊕)

are

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

ControllingunfoldingintypetheoryDanielGratzer1[0000000319440789],JonathanSterling1[0000000205855564],CarloAngiuli2[0000000295903303],ThierryCoquand3[0000000254295153],andLarsBirkedal1[0000000313200098]1AarhusUniversity2CarnegieMellonUniversity3ChalmersUniversityAbstract.Wepresentanovelmechanismforco...

展开>> 收起<<

Controlling unfolding in type theory Daniel Gratzer10000000319440789 Jonathan Sterling10000000205855564 Carlo Angiuli20000000295903303 Thierry Coquand30000000254295153 and.pdf

共31页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Controlling unfolding in type theory Daniel Gratzer10000000319440789 Jonathan Sterling10000000205855564 Carlo Angiuli20000000295903303 Thierry Coquand30000000254295153 and

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: