The Rocqshop 2025

This paper present Rocq-ditto, an OCaml library to write transformations of Rocq ASTs. While Rocq-ditto is still at an experimental stage, it already enables the implementation of simple transformations such as the one presented here, as well as more complex ones such as a transformation to replace instances of auto with the explicit steps found by the auto proof search.

This talk shares a testimony of how a software engineer ended up learning the Rocq proof assistant without the support of an academic environment. In doing so, I aim to provide an outside perspective on the quality of the available online resources, the difficulties encountered, some highlights and shortcomings, and some proof design patterns that emerged spontaneously while proving a novel algorithm over the course of a few weekends.

hol2dk is a tool that allows to translate HOL Light proofs to Rocq. But for the translated theorems to be usable, one has to "align" translated HOL Light types and definitions to their Rocq defined counterparts by proving they are equal. I will present the tactics I have written in Ltac to automate these alignments in the case of inductive types and total recursive functions and show the comparison with previous work done without these tactics.

Inquisitive logic provides a framework for studying both declarative and interrogative sentences in one setting using inquisitive disjunction and the inquisitive existential quantifier. In its support semantics, inquisitive formulae are interpreted by information states which are sets of classical first-order models (over a fixed domain). These models themselves are considered to be possible worlds. Note that one can restrict information states to be finite, which leads to bounded inquisitive logic; further restriction of semantics to at most n possible worlds (note no restriction on the cardinality of the domain of individuals!) is called n-boundedness. When mechanizing calculi with such semantics in Rocq, the representation of states is crucial. Using our Autosubst-based formalization of a labelled sequent calculus proposed by Litak and Sano as a case study (and comparing it with an earlier ND calculus by Ciardelli and Grilletti), we discuss whether one can/should use boolean predicates of type World -> bool (decidable by definition), or rather arbitrary functions of type World -> Prop.

We claim that small inversions are a very useful tool when writing non-trivial dependently typed programs and reasoning about them. The approach is illustrated on a typical small example, followed by more general explanations on the method.

In Rocq, types are classified in different universes, e.g., computationally relevant types enjoying large elimination live in Type whereas propositions (resp. strict propositions) are members of Prop (resp. SProp). While this system offers great expressivity, it also leads to the duplication of definitions, e.g., the dependent pair inductive type has $3^3 = 27$ possible instances: one for each combination of the sort of the carrier, of the type family and sort of the pair. Moreover, several recent works have appealed for distinct sorts, e.g., the two-level type theory to separate univalent and strict types, the reasonably exceptional type theory to distinguish exceptional and pure types or the reasonably gradual type theory to name a few. Refinements of the current sort system has also been explored, for instance by Keller and Lasson and Winterhalter. In order to accomodate the different sorts already implemented in Rocq and to easily implement and integrate new ones, Poiret et al. have proposed an extension of this system that introduces (prenex) polymorphism over sorts, named SortPoly. Even though SortPoly makes it possible to write, for example, a single inductive type for dependent pairs, it lacks the crucial property of having a principal type: some definitions still have to be duplicated. Moreover, others issues stemming from the subtle interactions between sorts arise in SortPoly, e.g., the impossibility to define the most generic record type or eliminator. To address these concerns, we introduce BoundedSortPoly, a theory of sort polymorphism extended with bounds reflecting the required elimination constraint between sort variables. In this document, we present our implementation of BoundedSortPoly in Rocq by focusing on the features we provide, and the imposed restrictions.

We will present our formalization of graph theory in Rocq, which is intended for expressing and proving integer invariants of graphs. Namely, we have formalized variations of matching subsets of edges of a graph, showing that their maximum or minimum sizes satisfy various inequalities. Such inequalities were described without formalization in the context of commutative algebra. Our motivation lies in finding more general or precise results supported by a proof checker. We rely on the mathcomp-finmap and mathcomp-classical packages, and leverage classical reasoning to deal with sets of edges or vertices. Whether these technicalities can lead to differences in flexibility or ease of reasoning would be an interesting question, whose answer we want to seek by presenting our work.

Finster and Mimram have defined a dependent type theory called CaTT, which describes the structure of ω-categories. Types in homotopy type theory with their higher identity types form weak ω-groupoids, so they are in particular weak ω-categories. In this article, we show that this principle makes homotopy type theory into a model of CaTT, by defining a translation principle that interprets an operation on the cells of an ω-category as an operation on higher identity types. We then illustrate how this translation allows to leverage several mechanisation principles that are available in CaTT, to reduce the proof effort required to derive results about the structure of identity types, such as the existence of an Eckmann-Hilton cell.

The dissemination of and interaction with Coq developments remains a significant challenge, often confined to static documents or code repositories that lack dynamism. We present an experience report on integrating Coq into hotdocX, a novel web platform that transforms documents into interactive, AI-augmented applications. By leveraging a `jsCoq` template within the hotdocX ecosystem, we create a new paradigm for "live" formal artifacts. This enables not only interactive educational tutorials and "papers-with-proofs" but also a creator economy for formal methods content. Furthermore, we explore the profound synergy between the browser-native jsCoq and Emdash, hotdocX's own dependently-typed logical framework. This opens a tangible pathway towards a browser-editable, extensible Coq-light kernel, presenting new opportunities for research in tactic development, meta-theory, and education.

We have used Interaction Trees to formalize and verify the front-end of the Jasmin compiler, relying on an integration of coinductive denotational semantics with Relational Hoare Logic. A crucial element in our approach is the definition of an appropriate relation to compare programs, which makes it possible to simplify the reasoning about undefined behaviour.

We introduce LLM4Docq, a project to bootstrap high-quality documentation for the MathComp library in Rocq using large language models (LLMs) and expert feedback. Our approach combines automated docstring generation with a human-in-the-loop annotation process: LLMs generate initial docstrings for formal statements, and experts review and refine them through a collaborative platform. The resulting dataset is used to fine-tune a domain-specific LLM for Rocq, enabling natural language retrieval, code documentation, and small scale context-dependent auto-formalization tasks.

While the MiniF2F dataset exists for Lean, Isabelle/HOL, and MetaMath, it has not been formalized in Rocq, limiting cross-system comparisons in automated theorem proving. We investigate whether state-of-the-art LLMs can automatically translate formal theorems between proof assistants. Using a three-stage methodology from basic prompting to multi-turn conversations with error feedback, we successfully translated 478 out of 488 theorems (98%) from MiniF2F to Rocq. Expert validation of 150 translations confirmed high accuracy with only 3 errors. This work provides a complete Rocq formalization of MiniF2F and demonstrates the viability of LLM-based cross-proof-assistant translation.