形式上对齐 HOL-Light 与 Rocq 库
Aligning HOL-Light and Rocq libraries formally
浏览论文内容
中文总结 AI 辅助
本文报告了将 HOL-Light 定理形式化翻译至 Rocq 的工作，开发自动化策略替换定义，并引入实数、R^n 空间及极限等新形式化内容。
中文摘要 AI 辅助
我们报告了将 HOL-Light 定理从 HOL-Light 类型/函数翻译为 Rocq 类型/函数上的定理的努力。为此，我们在 Rocq 中开发了策略，以自动化证明过程，这些证明用于将 HOL-Light 归纳类型或递归函数定义替换为 Rocq 中等价但更惯用的定义。我们还解释了如何替换实数的定义，以及诸如 R^n 空间和极限定义等若干数学概念，从而为 Rocq 用户提供了许多此前未在 Rocq 中形式化的逻辑与分析方面的定义和定理。
英文摘要
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.
发表机构
- INRIA（法国国家信息与自动化研究所）
- ENS Paris-Saclay（巴黎萨克雷高等师范学院）
- CNRS（法国国家科学研究中心）
机构由 AI 辅助整理，请以论文原文为准。
