Coq
 | |
 | |
| 作者 | フランス国立情報学自動制御研究所, パリ第7大学, エコール・ポリテクニーク, パリ第11大学, リヨン高等師範学校 |
|---|---|
| 初版 | 4.10 (1989年) |
| 最新版 |
9.2.0 
/ 2026年3月27日 |
| リポジトリ | |
| プログラミング 言語 | OCaml |
| 対応OS | マルチプラットフォーム |
| 対応言語 | 多言語対応 |
| 種別 | 定理証明支援系 |
| ライセンス | GNU LGPL 2.1 |
| 公式サイト |
rocq-prover |
Rocq Prover（旧称Coq）は、証明支援システムの一つ。Rocq Proverの核はプログラミング言語Gallinaを用いる。フランス国立情報学自動制御研究所のPI.R2チーム（PPS研究所内にある）が、エコール・ポリテクニーク、フランス国立工芸院、パリ第7大学、パリ第11大学と（かつてリヨン高等師範学校とも）共同して開発している。Hugo Herbelinが事実上の開発代表者である。
2023年10月11日、開発チームは名称をCoqからThe Rocq Proverに変更すると発表し、コードベースやウェブサイトなどの更新を開始した。
特徴
Rocq ProverはCalculus of constructionsという高階型システム(Thierry CoquandとGérard Huetが1984年に創始したもので、英語ではCoCと略せてシステム名Coqに至る)に基づく。正しい証明は正しく型がつくラムダ式であるというカリー＝ハワード同型対応を利用しているので、Rocq Proverの証明言語は型付きラムダ計算の一種である。1991年以降Rocq Proverが用いているCalculus of Constructionsの変種は、Christine Paulin-Mohringによるもので、帰納的構成を直接含み、Calculus of Inductive Constructions（CIC）という名前がついている。
Rocq Proverには
- 主張を操作する機能
- 主張の証明を機械的に検査する機能
- 形式的証明の探索を支援する機能
- 依存型を用いたプログラムを記述する機能
- 実行可能な検証済みプログラムを抽出する機能
がある。
加えてRocq Proverには証明の自動化機能が増えている。中にはomegaタクティクというものがあり、プレスバーガー算術の大部分を決定できる。
Rocq Proverの最大の達成の中には、
- 四色定理: Georges GonthierとBenjamin Wernerによって、完全に機械化された証明が2004年に完了した。
- CompCert: C言語のコンパイラで、Rocq Proverによって開発され証明がつき、2006年にリリースされた。
- Feit-Thompson定理: Georges Gonthierと彼のグループによって、2012年9月に証明が完了した。
がある。
Ssreflect拡張
Georges GonthierのチームがSsreflect（small scale reflectionの略）というRocq Proverの拡張を開発している。拡張はreflection用の機能にとどまらず、Rocq Proverの多くのタクティクの改良版を提供する上に、証明の保守性を高めるコーディング慣習も含んでいる。 Ssreflectの機能には下のようなものがある。
- 保守性を高めるための機能
- Rocq Proverが自動生成した識別子をユーザが指定できなくなって、Rocq Proverのバージョンアップによって証明が通らなくなることを防止する機能
- 証明の枝を完結させることを明示して、軽微な証明を自動で行わせられる上に、証明が通らなくなったときに修正するべき範囲がわかりやすくなる機能
- 主張を直接証明する代わりに、Rocq Prover内で検証済みの判定機を実行するreflectionという技法に特化した証明タクティク
- 有限集合上の和や積などの大きな演算子を扱う機能
- 代数のライブラリ
SsreflectはCeCill-BとCecill-2.0でデュアルライセンスされていて、自由に利用できる。Ssreflectの最新版はCoq 8.4上で動く。
脚注
- ↑ “Rocq 9.2.0”. 27 March 2026.
{{cite web2}}: Cite webテンプレートでは|access-date=引数が必須です。 (説明) - ↑ “Change of Name: Coq -> The Rocq Prover”. 2025年3月23日閲覧。
- ↑ A computer-checked proof of the Four Colour Theorem Georges Gonthier
- ↑ CompCertのページ(英語)
- ↑ 証明完了のアナウンス(英語)
- ↑ Ssreflectの配布元(英語)
参考文献
- 萩原学、アフェルト・レナルド『Coq/SSReflect/MathCompによる定理証明 フリーソフトではじめる数学の形式化』森北出版、2018年4月18日。ISBN 978-4-627-06241-2。