Rocq Lemmas Search
I develope a website (https://lemmasearch.com/) for searching theorems in the Rocq standard library. I use the Rocq OCaml API and modify the Rocq compiler to extract theorems. The theorems are extracted at runtime, therefore theorems from modules that require parameter instantiation are not included. I use BM25 for theorem retrieval, which eliminates the need to input standard Rocq statements.
The website is still under development. If you have any suggestions, please feel free to contact me via email.
Project Selection
On the left side of the search bar, we can choose which project to search for theorems in. Currently, there are two projects: the Coq standard library (8.20.0) and MathComp. “All” means searching across all current projects.
Pattern Matching
Currently, the search supports a simple pattern matching. Use pattern:rule. to specify a rule (note: there must be a period at the end!). The current pattern match is implemented using regular expressions; the rule between pattern: and . will be converted into a regular expression.
As shown in the figure below, the pattern comm pattern:nat. specifies that the lemma must contain the string “nat”. The search engine first filters the theorems that match the pattern, and then uses the BM25 algorithm to further filter the remaining queries comm among the matched theorems.
The pattern currently supports the notation “_”, as shown in the figure below, the query rev length pattern:_ ++ _ = _ ++ _. means that the theorems matching the pattern _ ++ _ = _ ++ _. are first filtered, and then use the BM25 algorithm to index the string rev length among these theorems.
Term Information
Currently, the search results also include information about terms. For each theorem in the search results, the subterms within the theorem and the inductive types it depends on are now included. Clicking “Details” will display information about the terms in the theorem.