HOL-Lightの定義と定理をRocqの自然な記法へ移植する

この論文をやさしく読む

ひとことで言うと

HOL-Lightに蓄積された形式的な数学を、Rocqの利用者が普段使う型や関数に合わせて移す研究です。

何に役立つ？

別の証明支援系ですでに整備された論理・解析の定理をRocqで利用する助けになります。同値な定義への置き換えに必要な証明を自動化しています。

この研究の面白いところ

元の定義をそのまま持ち込むだけでなく、実数や極限などの基本概念をRocqに適した定義へ合わせる点に重点があります。

どこまで分かった？

要旨には移植した定理の総数、処理時間、自動化の成功率は記載されていません。HOL-Lightの全ライブラリが移植済みという主張ではありません。

v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。

アブストラクトの日本語訳

本研究では、HOL-Lightの型や関数に関するHOL-Lightの定理を、Rocqの型や関数に関するRocqの定理へ変換する取り組みを報告する。そのために、HOL-Lightの帰納的な型や再帰関数の定義を、それと同値でありながらRocqでより自然な定義に置き換える際に必要となる証明を、自動化するタクティクをRocq内で開発した。また、実数の定義に加えて、Rⁿ空間や極限の定義など、複数の数学的概念をどのように置き換えたかを説明する。これにより、以前はRocqで形式化されていなかった、論理学と解析学に関する多くの定義や定理をRocqの利用者に提供する。

v1の要旨から自動生成。本文の精読・人による確認は未実施。