Automating formal translation between hol-light and rocq mathematical libraries
Aligning HOL-Light and Rocq libraries formally
Logic in Computer Science
Summary
Mathematicians use computer systems to check if complicated mathematical ideas are true, but different systems use different ways to write these ideas. The authors worked on moving math from one system called HOL-Light to another called Rocq by creating tools that rewrite definitions automatically. They managed to transfer important math ideas like real numbers and limits so Rocq can understand things that were only in HOL-Light before. This helps expand Rocq’s math knowledge without starting from scratch.
What this means in practice
- •For formal methods engineers: Automate porting proofs and definitions from HOL-Light to Rocq to integrate verified mathematical results across proof systems.
- •For software verification teams: Enhance Rocq’s library with foundational math theorems previously only available in HOL-Light, enabling more comprehensive software correctness proofs.
Authors
Frédéric Blanqui, Antoine Gontard
Abstract
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.