Aligning HOL-Light and Rocq libraries formally
In the authors' words
We report on our efforts to translate HOL-Light theorems on HOL-Light types/functions into Rocq theorems on Rocq types/functions. To this end, we developed in Rocq tactics to automate the proofs required for replacing a HOL-Light inductive type or recursive function definition by an equivalent but more idiomatic one in Rocq. We also explain how we replaced the definition of real numbers, as well as a number of mathematical notions like Rn spaces and the definition of limit, hence providing to Rocq users many definitions and theorems in logic and analysis that had not been formalized in Rocq before.
Appeared: Tuesday, September 22. arXiv. Preprint with a published version.
Published version: LPAR-26 - 26th Conference on Logic for Programming, Artificial intelligence, and Reasoning, Oct 2026, Spetses Island, Greece