Extraction and Search in Rocq: Theorems, Definitions and Their dependencies Jian Fang and Yingfei Xiong(B)
arXiv:2606.04704v1 [cs.SE] 3 Jun 2026
Key Laboratory of High Confidence Software Technologies (Peking University), Ministry of Education; School of Computer Science, Peking University, Beijing, China [email protected], [email protected]
Abstract. Rocq (Coq) are now widely used in various fields, including software verification and mathematical proofs. When proving a new theorem, users often need to search and apply proven theorems to assist the current proof process. However, the current search command is limited to the environment of imported modules and cannot search for theorems outside of this scope. Furthermore, tool developers and researchers may want to obtain detailed information about theorems, such as theorem’s names, statements, and dependencies. But there are currently no user-friendly and efficient tools available for extracting comprehensive information from Rocq projects. We introduce a Rocq theorem extraction and analysis tool, TheoremExtr, which is capable of analyzing theorem composition and extracting theorems, dependencies, and definitions from both parsing phase and runtime. We extracted 71,795 theorems and their dependencies from 32 open-source projects from the Rocq community. In addition, we extracted 27,481 definitions and their types among these projects. We also developed a website that supports cross-project similarity search for theorems and definitions. The tool is available at https://github.com/Rw1nd/TheoremExtr, and the search website is available at https://lemmasearch.com/. Keywords: Theorem proving · Software verification · Local search.
1
Introduction
Interactive theorem provers (ITPs) such as Rocq [12], are widely employed in computer science [6, 7] and mathematics [10]. Users construct formal proofs by manually writing proof scripts and need to reference previously proven theorems. However, Rocq currently lacks a unified theorem repository, like mathlib4 in Lean 4 [14]. Users have to manually search within projects to determine whether the required theorems already exist. Furthermore, researchers who wish to extract theorems from Rocq projects must acquire additional development knowledge (e.g., language server protocol), which increases the barrier. These give the following challenges: The search methods is limited. The Search command in Rocq is restricted to searching theorems within the current run-time environment. It cannot perform
2
J Fang, Y Xiong
cross-project searches or access theorems that have not been imported into the active environment. This limitation imposes an additional burden on users, who must manually search through open-source projects to determine whether required theorems exist. Theorem extraction is challenging. For researchers in domains such as automated theorem proving and large language models (LLMs) for formal methods [8, 15], extracting theorems from Rocq projects is essential to obtain comprehensive information (e.g., types, dependent functions). As illustrated in Figure 1, the theorem demonstrates a property of insertion sort in [1]. This example shows that a single theorem may depend on numerous definitions distributed across multiple files. However, mature and user-friendly tools to assist researchers in extracting those information are currently unavailable.
Fig. 1. Theorem and its dependencies
Our work. To address these challenges, we developed TheoremExtr, a theorem extraction and analysis tool. The tool collects data from both Rocq’s parsing phase and runtime to extract comprehensive information for each theorem, including its statement, dependent functions, and type definitions. Users can obtain detailed information from a project using a single command and a simple Python script, requiring minimal Rocq knowledge. Notably, we use the runtime only to analyze theorem dependencies and type information, without extracting runtime execution state information, such as stack or heap data. The contributions of this paper are as follows: – We implemented TheoremExtr, a tool that extracts theorems and their internal dependency definitions, achieving a balance between run-time efficiency and user-friendliness.
Title Suppressed Due to Excessive Length
3
– We extracted theorems from the Rocq platform, a distribution of the Rocq prover with libraries and plugins, as well as other open-source projects. Based on the extracted theorems and definitions, we developed a website available at https://lemmasearch.com. The website provides cross-project search capabilities with similarity search and localization to original project sources.
2
Approach
We observe that relying only on syntactic-level extraction in the parsing phase has significant limitations. For instance, a function definition within the current theorem might depend on files imported from external files. Moreover, the definition of a theorem may contain implicit arguments, which need to be analyzed according to the specific runtime context. And extracting information exclusively at runtime fails to capture precise scope information and line numbers for each theorem.
Fig. 2. Overview of TheoremExtr
Therefore, we need to combine the results of both analyses. Our tool TheoremExtr, comprises three components, as shown in Figure 2: i) Parser-stage data extraction, which is integrated into the Rocq compiler and extracts theoremrelated and file information. ii) Run-time extraction that extracts data during runtime. iii) The merging tool that combines the parser-stage data and run-time information. Our tool takes a Rocq project as input and outputs theoremsrelated data from the project. 2.1
Parser-stage data extraction
This component extracts data from the syntax by modifying portions of the Rocq compiler code. The component retrieves data from the following elements: i) statements (theorem statements or definition declarations), ii) scopes (modules, segments), iii) file information (file names, file path), iv) names (theorem names or definition names), v) line numbers. To retrieve various types of data, we appropriately integrate our data extraction code based on the data structures
4
J Fang, Y Xiong
defined in the Rocq source code. The extraction methods for different elements are described below. Statements and names. Building upon the original logic of the Rocq compiler, we add auxiliary functions to extract theorem statements, definitions, and their names based on the data structure that represents the abstract syntax tree. The detailed definition of this data structure can be found in [13]. And our code is implemented without altering the original compiler logic. TheoremExtr identifies each theorem by using its absolute path combined with the theorem name. When we use the nature number type nat, the name of nat is Coq.Init.Datatypes.nat. To enable a one-to-one correspondence with theorems or definitions, we also record the name of the file being compiled and its absolute path. Scopes. To correlate the theorems within a module with the information obtained during run-time, we need to manually manage the scope of the module during the parser-stage extraction. In Rocq, modules can contain theorems and proofs. When the parser processes module-related code, we identify the data to be extracted by marking the current scope. Theorems defined between the start and end of a module are considered internal to the module. File information and line numbers. When the Rocq compiler compiles a file, it locates the corresponding file based on its file path. During code parsing, the compiler records the location of each theorem and definition within the file. We capture this information during compilation for the files. With these approaches, the data for each theorem or definition can be extracted at compile time. Our extraction method has a negligible impact on compilation efficiency. 2.2
Run-time Extraction
Since Rocq supports extending its commands through plugins, we extract data from Rocq’s environment by implementing a Rocq plugin. Rocq plugins execute at run-time and can access all information within the current environment. To extract theorem-related information, we first retrieve all theorems accessible in the current environment. Due to the syntactic omission in some theorem types, we need to analyze their concrete types to obtain complete type definitions. And we analyze each subterm in the theorem to determine whether it is a function or an inductive type. For the inductive types used in theorems, we extract their concrete definitions. To align with the data from the parserstage data, the plugin must also record the absolute path and the name of each theorem. 2.3
Merging Tool
The merging tool combines the data obtained from parser-stage extraction with the data extracted at run-time. TheoremExtr use the names of theorems to merge information for the same theorems or definitions. For data obtained from
Title Suppressed Due to Excessive Length
5
parser-stage extraction, we reconstruct the complete full name by combining the compilation path, filename, scope, and theorem name. For data obtained at runtime, the theorem names are already full names and can be used directly. By merging the data from these two sources, TheoremExtr ultimately provides complete information for each theorem or definition and saves it to a JSON file.
3
Implementation and Usage
This section introduce the implementation and usage of extraction tool TheoremExtr and the search website. Extraction Tools. We implemented TheoremExtr on Rocq 8.20.0. We modified the codes in the Rocq compiler to extract data from the parse phase. Use coqc command to compile the Rocq files, and it will generate a new JSON file in the target directory. Additionally, we implemented a Rocq plugin that introduces a new command, Createdb, enabling the extraction of data from run-time. To use the plugin, users must first import all libraries to be extracted and then invoke the Createdb command, as shown in the following code: Require Import Target.Lib. ... Createdb.
When the plugin completes extraction, a new JSON file is generated in the default path. The Python script merges these two parts of data. All experiments were conducted on a machine equipped with an Intel Core Ultra 7 265K processor and 48 GB of RAM, running Ubuntu 22.04.5 LTS under the Windows Subsystem for Linux (WSL). Table 1 reports the time overhead per project, measured as the combined cost of parser-stage data extraction and runtime extraction. Table 1: Time overhead per project (in seconds).
Project coq-aac-tactics mathcomp-algebra-tactics mathcomp-analysis mathcomp-bigenough coq-bignums coq-itauto compcert coq-corn coq-equations coq-ext-lib coq-fcsl-pcm
Parser-stage Runtime data extraction (s) extraction (s) Total (s) 4 12 447 1 11 55 254 172 6 4 41
5 29 157 6 10 5 75 1679 1 7 51
9 41 604 7 21 60 329 1851 7 11 92
6
J Fang, Y Xiong
Parser-stage Runtime data extraction (s) extraction (s) Total (s)
Project coq-gappa coq-hott coq-htt coq-relation-algebra coq-stdlib coq-coqeal coq-coqprime coq-coquelicot mathcomp-finmap coq-flocq coq-interval coq-iris coq-math-classes mathcomp coq-mtac2 mathcomp-multinomials coq-quickchick mathcomp-real-closed coq-reglang coq-stdpp coq-vst
13 41 39 37 79 61 27 34 10 66 85 126 28 238 18 25 12 47 19 43 509
10 37 28 7 198 59 21 10 7 14 26 1369 18 14 6 31 8 34 16 147 143
23 78 67 44 277 120 48 44 17 80 111 1495 46 252 24 56 20 81 35 190 652
Total
2564
4226
6790
Fig. 3. Theorem search website
Search website. We selected 32 open-source projects from the Rocq platform (version 2025.01.0) and the Rocq community for extraction, resulting in
Title Suppressed Due to Excessive Length
7
a total of 71,795 theorems and 27,481 definitions. We used Flask [5] to build a theorem search website. The website utilizes the BM25 [9] algorithm to enable similarity search. As shown in Figure 3, when searching for theorems related to memory storage, one can directly use store mem as the keywords for the search. The search results show that the CompCert project contains relevant theorems. In contrast, using a general search engine with the same keywords fails to find the related Rocq theorems. Moreover, users need to know in advance which projects are relevant. The results demonstrate that our website can search lemmas across projects and provides dependencies and associated types. To enable the localization of theorems within their original projects, each theorem name is hyperlinked to its corresponding location in the original code repository.
4
Related work
Currently, several tools are available for extracting data from Rocq. CoqPyt [3] is a Python-based extraction framework that relies on coq-lsp [2]. However, compared to TheoremExtr, it lacks the capability to analyze dependency information within theorems. Coq SerAPI [4] is another tool capable of extracting internal data from Coq. However, it requires users to learn additional protocol commands. In contrast, TheoremExtr provides a more user-friendly interface, as it can be operated using simple Rocq commands. Coq-lsp [2] can also be used for extracting data from Rocq. However, it requires additional knowledge of the LSP protocol [11], which is not specific to Rocq. And there are also serveral theorem datasets, such as Coqgym [16] and CoqStoq [15]. However, these datasets are either outdated or lack scalability, making it challenging to migrate across different Rocq versions. TheoremExtr is implemented based on the Rocq compiler and its plugins, making it easily portable across different versions of Rocq.
5
Conclusion and future work
We developed the tool TheoremExtr, which is capable of extracting theorems and definitions during the parsing and run-time phases of Rocq. TheoremExtr is user-friendly and has a low learning curve. Using TheoremExtr, we extracted 71,795 theorems and 27,481 definitions from 32 open-source projects and developed a search website to support similarity search. Moreover, since our approach is built directly upon Rocq itself, it offers excellent scalability. In addition, TheoremExtr can be used in LLM training or within LLM agents. TheoremExtr can access richer theorem information, it provides more Rocq corpora for training LLMs and supplies more informative feedback for LLM agents. Currently, TheoremExtr has been implemented on Rocq version 8.20.0. Due to differences between Rocq versions, we plan to extend the implementation to all future versions of Rocq.
8
J Fang, Y Xiong
References 1. Appel, A.W.: Verified Functional Algorithms, Software Foundations, vol. 3. Electronic textbook (2025) 2. Arias, E.J.G., Caglayan, A., Itzhaky, S., Ramachandra, R.: Language server protocol native server for coq (2024), https://rocq-prover.org/doc/V8.20.0/refman/ index.html 3. Carrott, P., Saavedra, N., Thompson, K., Lerner, S., Ferreira, J.F., First, E.: Coqpyt: Proof navigation in python in the era of llms. In: d’Amorim, M. (ed.) Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering, FSE 2024, Porto de Galinhas, Brazil, July 1519, 2024. pp. 637–641. ACM (2024). https://doi.org/10.1145/3663529.3663814, https://doi.org/10.1145/3663529.3663814 4. Gallego Arias, E.J.: SerAPI: Machine-Friendly, Data-Centric Serialization for Coq. Tech. rep., MINES ParisTech (Oct 2016), https://hal-mines-paristech. archives-ouvertes.fr/hal-01384408 5. Grinberg, M.: Flask web development. " O’Reilly Media, Inc." (2018) 6. Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D.A., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an os kernel. In: Matthews, J.N., Anderson, T.E. (eds.) Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11-14, 2009. pp. 207–220. ACM (2009). https://doi.org/10.1145/1629575.1629596, https://doi.org/10.1145/1629575.1629596 7. Krebbers, R., Leroy, X., Wiedijk, F.: Formal C semantics: Compcert and the C standard. In: Klein, G., Gamboa, R. (eds.) Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8558, pp. 543–548. Springer (2014). https://doi.org/10.1007/ 978-3-319-08970-6_36, https://doi.org/10.1007/978-3-319-08970-6_36 8. Lu, M., Delaware, B., Zhang, T.: Proof automation with large language models. In: Filkov, V., Ray, B., Zhou, M. (eds.) Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, ASE 2024, Sacramento, CA, USA, October 27 - November 1, 2024. pp. 1509–1520. ACM (2024). https://doi.org/10.1145/3691620.3695521, https://doi.org/ 10.1145/3691620.3695521 9. Lù, X.H.: Bm25s: Orders of magnitude faster lexical search via eager sparse scoring (2024), https://arxiv.org/abs/2407.03618 10. Mahboubi, A., Tassi, E.: Mathematical components. Online book (2021) 11. Microsoft: Language server protocol, https://microsoft.github.io/ language-server-protocol/ 12. The Coq Development Team: The Coq reference manual – release 8.20.0 (2024), https://rocq-prover.org/doc/V8.20.0/refman/index.html 13. The Coq Development Team: Rocq ocaml api (2024), https://rocq-prover.org/ doc/V8.20.0/api/coq-core/Vernacexpr/index.html#type-synpure_vernac_ expr 14. The mathlib4 Development Team: The math library of lean 4 (2025), https:// rocq-prover.org/doc/V8.20.0/refman/index.html 15. Thompson, K., Saavedra, N., Carrott, P., Fisher, K., Sanchez-Stern, A., Brun, Y., Ferreira, J.F., Lerner, S., First, E.: Rango: Adaptive retrieval-augmented proving
Title Suppressed Due to Excessive Length
9
for automated software verification. In: 47th IEEE/ACM International Conference on Software Engineering, ICSE 2025, Ottawa, ON, Canada, April 26 - May 6, 2025. pp. 347–359. IEEE (2025). https://doi.org/10.1109/ICSE55347.2025.00161, https://doi.org/10.1109/ICSE55347.2025.00161 16. Yang, K., Deng, J.: Learning to prove theorems via interacting with proof assistants (2019), https://arxiv.org/abs/1905.09381