# The HOL-Light library of Multivariate Real analysis in Rocq

Claudio Sacerdoti Coen, Abdelghani Alidra, Frédéric Blanqui

<figure><img src="image_1.png" /></figure>

To cite this version:

Claudio Sacerdoti Coen, Abdelghani Alidra, Frédéric Blanqui. The HOL-Light library of Multivariate Real analysis in Rocq. RocqPL 2026 - Rocq for Programming Languages, Frédéric Besson; Benjamin Delaware, Jan 2026, Rennes, France. hal-05464922

HAL Id: hal-05464922

https://inria.hal.science/hal-05464922v1

Submitted on 19 Jan 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# The HOL-Light library of Multivariate Real analysis in Rocq

Claudio Sacerdoti Coen

Department of Computer Science and Engineering -
University of Bologna

Italy

## Abstract

In this paper we present Coq-HOL-Light, a library with more than 20,000 mathematical theorems on Real analysis in Rocq. This library is a translation from the HOL-Light proof assistant. By proving the equivalence between a number of types, functions and predicates in HOL-Light and their counterpart in the Rocq standart library, we make this library directly usable in Rocq developments. We also present our indexing and retrieval tools, specially tailored for searching mathematical entities in the Coq-HOL-Light library with special facilities for the Rocq community. All tools underpinning our methodology are publicly available guarantying the reproducibility of the processes detailed in this paper. We argue that this work is relevant to researchers and practitioners who wish to harness HOL-Light's comprehensive analysis library to support the construction of Rocq developments.

## ACM Reference Format:

Claudio Sacerdoti Coen, Abdelghani Alidra, and Frédéric Blanqui.
2026. The HOL-Light library of Multivariate Real analysis in Rocq.
In . ACM, New York, NY, USA, 3 pages. https://doi.org/10.1145/nnnnnnn.nnnnnnn

## 1 Introduction and problem statement

HOL-Light is a popular proof assistant offering an extensive library of mathematical theorems in analysis, which would be of significant interest to the Rocq community. However, making such a library available in Rocq falls under the well-known challenge of achieving true interoperability between distinct mathematical systems[1]. Indeed, a proof translation between the two systems is only truly useful when the resulting theorems are expressed in terms of the Rocq standard library, allowing users to apply them directly within their

Abdelghani Alidra

Frédéric Blanqui

Univ. Paris-Saclay, ENS Paris-Saclay, CNRS, INRIA, LMF

France

development projects. Achieving this alignment, however, requires substantial effort, as the definitions of types and functions often differ significantly between systems such as HOL-Light and Rocq—most notably because HOL-Light relies extensively on Hilbert’s choice operator, while Rocq is based on inductive types and recursive definitions. Moreover, even a globally consistent library contains multiple, distinct representations of identical mathematical objects—one per originating system—with no built-in mechanism to identify or relate them. Also, HOL-Light proof trees are usually very large, which become challenging to translate, re-verify and search.

In a previous work [2], the third author introduced a method for fully automating the translation of proofs from HOL-Light to Rocq, leveraging Dedukti as an intermediate language and developing a library, Coq-HOL-Light, based on the classical logic of HOL-Light that can be easily integrated into other Rocq developments.

**Contribution:** Building on this foundation, the present paper provides an updated, practical overview of the generated library and its integration into Rocq, while extending a recent work [3] on indexing and retrieval in large heterogeneous libraries tailored specifically to the Coq-HOL-Light library, to enhance the user experience of Rocq users when working with the library artefacts.

## 2 The Coq-HOL-Light library

To achieve translation of libraries from HOL-Light to Rocq while addressing the challenges mentioned in section 1, the third author developed a tool-supported method called hol2dk<fnref n="1" />. Rather than translating the HOL-Light library directly into Rocq, it proceeds through Dedukti<fnref n="2" /> and Lambdapi<fnref n="3" /> as intermediate representation. This multi-stage translation pipeline facilitates reusability and allows us to effectively manage the considerable size and complexity of HOL-Light proof trees. Moreover, the Lambdapi files produced during this process serve as the foundation for the implementation of our indexing and retrieval tools, as detailed in Section 3.

We obtain readable and directly usable Rocq libraries derived from HOL-Light developments. In an earlier work [2], the third author reported the translation of a portion of

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org.

*Conference’17, Washington, DC, USA*

© 2026 Copyright held by the owner/author(s). Publication rights licensed to ACM.

ACM ISBN 978-x-xxxx-xxxx-x/YYYY/MM

https://doi.org/10.1145/nnnnnnn.nnnnnnn

<footnote n="1">¹https://github.com/Deducteam/hol2dk</footnote>

<footnote n="2">²https://github.com/Deducteam/Dedukti</footnote>

<footnote n="3">³https://github.com/Deducteam/lambdapi</footnote>
HOL-Light's analysis library comprising 448 lemmas. More recently, this Rocq library has been significantly extended with additional types and functions originating from HOL-Light's Multivariate library. The newly released version now includes over 20,000 theorems covering a broad range of mathematical domains— such as arithmetic, well-founded relations, lists, real numbers, integers, set theory, permutations, group theory, matroids, metric spaces, homology, vector spaces, determinants, topology, convexity, paths, polytopes, Brouwer degree, derivatives, Clifford algebras, integration, measure theory, complex analysis, and transcendental functions.

The resulting Rocq library is publicly available on the Opam repository<fnref n="4" /> and can be installed via:
```
opam repo add rocq-released https://rocq-prover.org/opam/released && opam install coq-hol-light
```

It can then be directly used in any Rocq development through the standard import mechanism.

In the next section, we will see how existing tools based on Dedukti/Lambdapi for indexing and searching large heterogeneous mathematical libraries have been leveraged for the Coq-HOL-Light library.

## 3 Indexing and retrieval

Indexing and searching across large, heterogeneous libraries, such as the one discussed in this work, remain challenging tasks [4, 5]. In our previous research, we proposed a method and an accompanying tool specifically designed to mitigate these difficulties [3]. This approach is supported by tooling built atop the Lambdapi rewriting engine, which provides a dedicated textual command for indexing Lambdapi and Dedukti files originating from heterogeneous formal libraries. Both textual commands and a web-based interface have been developed to support searching within heterogeneous Dedukti and Lambdapi libraries. These tools provide a query language that allows complex queries to be constructed from atomic ones [3]. This was made possible through the use of alignments represented as Lambdapi files containing rewriting rules between the different encodings. To support this mechanism, we first extended the Lambdapi rewriting engine to implement query normalization and approximation[3]. These modifications enabled the formulation of queries that are independent of any specific encoding, allowing users to retrieve relevant statements from multiple sources.

However, the existing tools still relied heavily on Lambdapi syntax: queries had to be expressed using Lambdapi notation, and the results were displayed as Lambdapi terms, even when the corresponding lemmas or definitions were available in Rocq. Such limitations could represent a significant obstacle for Rocq users, who naturally expect to search and browse libraries using the familiar Rocq syntax and presentation style.

To address these limitations, we adapted and extended the tools described in [3] to deliver a Rocq-tailored user experience for efficiently exploring and retrieving mathematical content from the Coq-HOL-Light library.

First, we enhanced the search tool to parse terms expressed in a minimal subset of the Rocq language. In particular, it now recognizes standard Rocq syntax such as `forall`, `exists`, `\` and `\` in place of their Unicode Lambdapi counterparts. Combined with the alignment mechanism described above, this extension provides a more natural and intuitive interface for Rocq users.

Second, we augmented the indexing command with a `-sources` flag, linking Rocq source files to the corresponding Lambdapi-indexed code. As a result, the search tool can now display results in both Rocq and Lambdapi formats, while accurately pointing to the relevant Rocq file and location of each matched result. Moreover, search queries and results are now interpreted up to alignment, thereby eliminating ambiguities and avoiding duplicate matches arising from overloaded symbols.

It is worth mentioning that these modifications did not negatively impact the performance of our tools. Indexing the entire library on a machine equipped with a AMD EPYC 7443 24-Core Processor processor and 47 GB of RAM takes only 23.42 seconds producing an index of 111 MB on disk, while the search engine typically returns results within just a few milliseconds.

In addition, and although not specific to Rocq users, the overall user experience has been further improved through the extension of the query language with regular expression support for finer-grained result filtering, as well as incremental result rendering, which ensures a smooth and responsive interface even when handling a very large number of search results.

The new search tool is publicly available on

https://lambdapi.saclay.inria.fr/coq-hol-light.

## 4 Conclusion and future works

In this short paper, we have presented Coq-HOL-Light, a Multivariate real analysis library for Rocq, along with a suite of supporting tools designed to facilitate its efficient use in practical developments. This work complements our previous publications [2, 3] and the accompanying online documentation. The code supporting the methods presented in this work is publicly available in the corresponding GitHub repositories, including references to Docker images to facilitate reproducibility.

Future directions include optimizing the translation pipeline to reduce library size and proof-checking delays, extending the approach to additional source libraries (such as Lean and Isabelle), enhancing Rocq syntax support in query formulation, and improving the integration of the search tool within existing Rocq development environments.

<footnote n="4">⁴https://github.com/Deducteam/coq-hol-light</footnote>
References

[1] D. J. Howe, "Importing mathematics from hol into nuprl," in *International Conference on Theorem Proving in Higher Order Logics*, pp. 267–281, Springer, 1996.

[2] F. Blanqui, "Translating HOL-Light proofs to Coq," in *LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024*, vol. 100 of *EPiC Series in Computing*, pp. 1–18, EasyChair, 2024.

[3] C. Sacerdoti Coen and A. Alidra, "Indexing and retrieval in a heterogeneous formal library," in *International Conference on Intelligent Computer Mathematics*, pp. 258–275, Springer, 2025.

[4] F. Guidi and C. S. Coen, "A survey on retrieval of mathematical knowledge," *Math. Comput. Sci.*, vol. 10, no. 4, pp. 409–427, 2016.

[5] P. Dadure, P. Pakray, and S. Bandyopadhyay, "Mathematical information retrieval: A review," *ACM Comput. Surv.*, vol. 57, no. 3, pp. 61:1–61:34, 2025.