Aligning HOL-Light and Rocq libraries formally
En palabras de los autores
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.
Apareció: martes, 22 de septiembre. arXiv. Preprint con versión publicada.
Versión publicada: LPAR-26 - 26th Conference on Logic for Programming, Artificial intelligence, and Reasoning, Oct 2026, Spetses Island, Greece