Extraction and Search in Rocq: Theorems, Definitions and Their dependencies
This tool addresses the need for efficient extraction and search of theorems and definitions across Rocq projects, benefiting Rocq users and tool developers.
The authors developed TheoremExtr, a tool for extracting theorems, definitions, and dependencies from Rocq projects, and created a cross-project similarity search website. They extracted 71,795 theorems and 27,481 definitions from 32 open-source projects.
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.