Why Rocq?

The Rocq Prover follows from over 40 years of research in Dependent Type Theory and Interactive Theorem Proving. It is based on the Predicative, Polymorphic and Cumulative Calculus of Inductive Constructions (PCUIC), a dependently-typed formal language for constructive mathematics that allows to express complex, higher-order mathematical statements and functional programs. PCUIC includes general schemes for the definition of families of mutual or nested inductive and coinductive types, that can be used to model and program with finite or infinite data structures and predicates.

The Calculus of Constructions¹, due to Thierry Coquand and Gérard Huet, was born out of a generalization of the polymorphic λ-calculus (a.k.a. System F^ω2) and Martin-Löf Type Theory³, integrating an infinite, predicative and cumulative hierarchy of universes Type@{i} for computational types and an impredicative universe of propositions Prop for proof-irrelevant propositions.

Based on this distinction between computations and proofs, PCUIC supports a well-behaved notion of erasure used by its extraction mechanisms, allowing to produce efficient programs in standard programming languages from formal developments. While being based on programming language theory and constructive mathematical foundations, PCUIC also accomodates using classical axioms in its propositional universes without affecting its good theoretical properties. PCUIC supports sort and universe polymorphism allowing to write generic definitions depending on universes. Beyond this, the system supports a notion of primitive types including 63-bit integers, IEEE-754 floats, persistent arrays and strings for efficient computation with primitive values. The following section details these features in more details.

• Universes, Typical Ambiguity, and Implicit Cumulativity:

  The Gallina surface language of the Rocq Prover supports the notion of typical ambiguity for universe levels, going back to the seminal work of Whitehead and Russell in Principia Mathematica⁴, which allows implicit handling of the relation between universe levels (in their case, ordinals of sets/classes).

  An anonymous Type occurrence represents a floating universe variable that can get constrained depending on its use in the rest of the definitions. The predicative universe hierarchy Type@{i} is cumulative, hence uses of universes can results in inclusion constraints, e.g. Type@{i} <= Type@{j}. The Rocq Prover handles this graph of universes and constraints incrementaly and checks that the universe graph is acyclic at all times ensuring consistency of the definitions. The user can hence write formal developments without ever needing to annotate universes, letting the Rocq elaboration engine take care of it.

  This system was first designed by Huet⁵ and evolved over the years with Hugo Herbelin⁶ extending it to handle algebraic universes and a limited form of polymorphism.

• Universe and Sort Polymorphism: Since Rocq 9.0, both universes and sorts can be abstracted over in inductive types, definitions and proofs. This polymorphism allows to share constructions between predicative and impredicative, proof-relevant or proof-irrelevant, and even user-defined universes. See the paper for example uses of custom sorts.
• (Co-)Inductive Type Families, mutual and nested: PCUIC is an evolution of the Calculus of Inductive Constructions introduced by Thierry Coquand⁷ and Christine Paulin-Mohring^8,9 as an extension of the Calculus of Constructions with schemes for inductive types and families. Cumulativity for (co)-inductive types was added later by Amin Timany and Matthieu Sozeau¹⁰, allowing to lift cumulativity through inductive definitions. Inductive types are a central modeling tool in the language: they allow to represent both computational data structures like natural numbers and lists as well as logical judgments like predicates, relations and typing systems. In the Gallina language, inductive types can be consumed by fixpoint computations that are checked to be terminating thanks to a so-called syntactic guard condition. The Rocq tactics allow to perform induction and inversion reasoning on these inductive structures. Co-inductive types and co-recursion are also available to model infinite structures and judgments, like bisimulation relations. A high-level dependent pattern-matching compiler is available through the Equations¹¹ package as part of the Rocq Platform.
• Extraction: The separation of propositions and types in PCUIC enables the sound erasure of computationally-irrelevant information such as type annotations and proof terms from Rocq terms. This process results in terms of the pure untyped λ-calculus extended with (co)-datatypes representing (co-)inductive values. The Rocq prover is a pioneer in developing this mechanism to extract relatively efficient programs from (constructive) proofs. Extraction for the Calculus of Constructions was first introduced by Paulin-Mohring¹² and continually refined with extensions of the calculus to culminate in the landmark PhD of Pierre Letouzey¹³, which provides both operational and semantic results on extraction and comes with an implementation that can target the OCaml, Haskell and Scheme languages. Extraction can be used to develop reasonably efficient programs. For example, the extracted CompCert compiler runs in time comparable to the GCC compiler in many cases, while providing an incomparable correctness guarantee!
• Definitional Proof Irrelevance: The SProp sort refines the orginal Prop sort of the Calculus of Constructions by providing a definitionally proof-irrelevant universe of propositions, that is closed under the standard type formers¹⁴. Thanks to SProp, proofs of propositions really are indistinguishable and do not need to be reduced at any point during a proof or computation, resulting in a more comfortable experience in formalizations mixing computations and proofs.
• Efficient Definitional Equality and Recuction Machines: The Rocq Prover includes two efficient definitional equality checkers: vm_compute and native_compute. The vm_compute checker uses a tailor-made compilation of call-by-value strong reduction to bytecode close to OCaml's bytecode interpreter, designed by Benjamin Grégoire and Xavier Leroy¹⁵. The native_compute checker uses a compilation scheme that directly links to the native OCaml compiler, for heavy-duty computations, designed by Maxime Dénès¹⁶.
• Certified Type Theory: The Rocq Prover is based on the formal verification of its type theory implementation and extraction system, developed in the MetaRocq project. It provides¹⁷ alternative certified proof checkers and erasure procedures that minimize the trusted code base and increases user confidence in its results.

• Metaprogramming Languages: The built-in Ltac2 typed tactic programming language enables the design of predictable and comfortable automation for proofs at a high-level of abstraction, with native handling of the proof state and backtracking.

  As part of the Rocq Platform, two additional metaprogramming languages are available:

  • A low level of abstraction is provided by the MetaRocq project which uses Rocq itself as the metaprogramming language. It allows directly working with the core term syntax and prove meta-theorems on the typing judgments of Rocq inside Rocq.
  • An alternative high-level language is provided by Rocq-Elpi, which interfaces Rocq with λ-prolog, a logic programming language allowing to naturally express proof-search, unification and elaboration problems. Rocq-Elpi is at the core of Hierarchy-Builder, a metaprogramming tool that allows the effective development of hierarchies of structures in Rocq in an entirely declarative fashion. It handles in particular all structures used in the Mathematical Components libraries.