(Link)

Authors: Yves Bertot and Pierre Castéran (INRIA Sophia-Antipolis)

Reference: Bertot, Yves, and Pierre Castéran. Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer, 2004.

Why this paper? Cited by Transformer-Based Models Are Not Yet Perfect At Learning to Emulate Structural Recursion, Single-set cubical categories and their formalisation with a proof assistant, and Formalizing the ∞-Categorical Yoneda Lemma

I’ve written before about the Coq Proof Assistant . Since then, after years of bravely ignoring the sniggers its French name produced among English speakers, the developers have decided to remain it Rocq in honour of Rocquencourt, the French town in which much of the development took place. The good news for the authors of this week’s book, should they ever decide to produce a new edition, is that Rocq’Art is an even better name.

This book is intended to be a comprehensive tutorial for Rocq which both acts as an introduction for newcomers and as a reference book for advanced techniques. This makes it fairly long and detailed and, as usual, I did not attempt to read every word within the week I give myself for each blog post; I also will not repeat anything in my earlier post on the prover itself.

A part of the book that interested me that I did not discuss last time is the substantial discussion on the different universes (types of types) available in Rocq: Set, Prop, and Type. The elements of Set are called specifications, which are inhabited by programs, whereas Prop contains the propositions, inhabited by proofs. Given the well known Curry-Howard isomorphism between proofs and programs it may seem odd that these notions are distinguished, but the core reason is that Rocq is not designed to run programs. Instead, programs that are verified in Rocq are extracted to another more efficient language, such as OCaml. In this process programs in Set are retained, whereas proofs about that program in Prop, their job done, are discarded. Set and Prop are both themselves elements of the hierarchy of types called Type. Another distinction between Set and Prop is the impredicativity of the latter; we can define a proposition with a universal quantifier ranging over any type, but cannot do the corresponding construction on Set.

I do find a little peculiar that this book continues to be cited in papers in the way it is with the references I looked at this week: where Rocq is mentioned, even very briefly, this book is the citation attached. The reason I find this odd is that Coq’Art is moderately old with respect to the development of Rocq, and its discussion of coinductive types for example is out of date, as even is their look at universes (we now also have SProp, which is a variant of Prop with a property called definitional proof irrelevance). The Rocq user manual, which is updated much more frequently and is fairly readable, does seem like a better option as a generic citation to me. However Coq’Art does seem to be an excellent option still as a reference manual for a would-be expert user.