Loading article…
Rocq Prover（旧称Coq）は、 1989年に初めてリリースされた対話型定理証明器です。数学的な主張の表現、これらの主張の証明の機械的な検証、証明自動化ルーチンを使用した形式的証明の探索、形式仕様の構成的証明からの認証済みプログラムの抽出などが可能です。
Rocqは、構成計算の派生である帰納的構成計算の理論に基づいて動作します。Rocqは自動定理証明器ではありませんが、自動定理証明の手法（手続き）と様々な決定手続きを備えています。
計算機学会（ ACM）は、ティエリー・コカン、ジェラール・ユエ、クリスティーヌ・ポーリン＝モーリング、ブルーノ・バラス、ジャン＝クリストフ・フィリアートル、ユーゴ・エルベリン、チェタン・マーシー、イヴ・ベルトー、ピエール・カステランに対し、Rocq（当時はCoqという名称だった）の功績により、2013年ACMソフトウェアシステム賞を授与した。
プログラミング言語として見ると、Rocq は依存型関数型プログラミングモデルを実装しています。[ 2 ]論理システムとして見ると、高階型理論を実装しています。Rocq の開発は、1984 年以来、フランス国立情報学研究所(INRIA)が他の多くのフランスおよび国際的な研究機関と協力して支援してきました。Rocq の開発は Gérard Huet と Thierry Coquand によって開始され、200 人以上[ 3 ]が主に研究者として、その発案以来コア システムに機能を提供してきました。実装チームは、Gérard Huet、Christine Paulin-Mohring、Hugo Herbelin、および Matthieu Sozeau によって順に調整されてきました。Rocq は主にOCamlで実装され、少しCも使用されています。コア システムはプラグインメカニズムによって拡張できます。[ 4 ]
Rocq は Gallina という仕様記述言語を提供しています。[ 5 ] Gallina で書かれたプログラムは弱正規化特性を持ち、常に終了することを意味します。これは、他のプログラミング言語では無限ループ (終了しないプログラム) が一般的であるため、この言語の際立った特性です。[ 6 ]
Rocqで書かれた証明の例として、自然数の次の数を取ると偶奇性が反転するという補題の証明を考えてみましょう。証明を簡潔に保つために、 Danvy [ 7 ]によって導入された折りたたみ・展開戦術が使用されています。
From Stdlib Require Import Arith Nat Bool .Fixpoint is_even ( n : nat ) : bool := match n with | 0 => true | S n' => negb ( is_even n' ) end .補題is_even_0 : is_even 0 = true 。証明。反射律。証明終了。補題is_even_S n : is_even ( S n ) = negb ( is_even n ).証明.反射律.証明完了.補題successor_flips_evenness n : is_even n = negb ( is_even ( S n )).証明. rewrite is_even_S . destruct ( is_even n ). * simpl . reflexivity . * simpl . reflexivity . Qed .この証明では、まず標準ライブラリからブール値と自然数の定義をインポートし、次にis_even数値が偶数かどうかを返す関数を定義します。その後、この関数に関する 3 つの補題が証明されます。最初の補題は、の定義式を単に書き直したものでありis_even、Rocq はこれらの式を知っているため、証明は非常に短くなります。最後の補題は、2 番目の補題を最初に適用した後、場合分けを用いて証明されます。星印は、*そこから新しいサブケースが始まることを示しています。
イギリス、ケンブリッジのマイクロソフトリサーチのジョルジュ・ゴンティエとINRIAのベンジャミン・ヴェルナーは、Rocqを使用して、2002年に完成した4色定理の概観可能な証明を作成しました。 [ 8 ] 彼らの研究は、Rocqの重要な拡張であるSSReflect（「小規模反射」）パッケージの開発につながりました。[ 9 ]その名前にもかかわらず、SSReflectによってRocqに追加された機能のほとんどは汎用機能であり、計算反射プログラミングスタイルの証明に限定されません。これらの機能には以下が含まれます。
setより強力なマッチングを備えた改良された戦術SSReflectはCoq 8.7以降、Rocqのメインディストリビューションの一部として配布されています。[ 10 ]
ガリーナ項を明示的に構築することに加えて、Rocq は組み込み言語 Ltac または OCaml で記述されたタクティクスの使用をサポートしています。これらのタクティクスは証明の構築を自動化し、証明における自明または明白なステップを実行します。 [ 15 ]いくつかのタクティクスは、さまざまな理論の決定手順を実装しています。たとえば、「ring」タクティクスは、結合法則と可換法則による書き換えによって、環または半環の公理を法とする等式の理論を決定します。[ 16 ]たとえば、次の証明は、整数環における複雑な等式をわずか 1 行の証明で確立します。[ 17 ]
Require Import ZArith . Open Scope Z_scope . Goal forall a b c : Z , ( a + b + c ) ^ 2 = a * a + b ^ 2 + c * c + 2 * a * b + 2 * a * c + 2 * b * c . intros ; ring . Qed .組み込みの決定手続きは、空理論（「congruence」）、命題論理（「tauto」）、量化子なし線形整数演算（「lia」）、線形有理数/実数演算（「lra」）にも利用できます。[ 18 ] [ 19 ]さらに、クリーネ代数[ 20 ]や特定の幾何学的目標[ 21 ]など、ライブラリとして決定手続きが開発されています。
旧名Coq はフランス語で「雄鶏」を意味し、ティエリー・コカン、構成計算、またはCoCの名前をもじったもので、研究開発ツールに動物の名前を付けるフランスの伝統に由来しています。[ 22 ] 1991 年まで、コカンは構成計算と呼ばれる言語を実装しており、当時は単にCoCと呼ばれていました。1991 年に、拡張帰納的構成計算に基づく新しい実装が開始され、構成計算をジェラール・ユエと共に開発し、クリスティン・ポーリン＝モーリングと共に帰納的構成計算に貢献したコカンへの間接的な言及として、名前がCoCからCoqに変更されました。 [ 23 ] 2023 年 10 月 11 日、開発チームは、Coq が今後数か月でThe Rocq Proverに改名されることを発表し、コード ベース、ウェブサイト、および関連ツールの更新を開始しました。[ 24 ]正式な名称変更は、2025 年 3 月に Rocq 9.0 がリリースされた際に行われた。[ 25 ]新しい名前は、システムが最初に開発されたInria Rocquencourtに由来し、神話上の鳥Rocに関連しており、以前の名前の鳥の参照を維持している。[ 26 ]
