Coq

Coqは、証明支援システムの一つ。Coqの核はプログラミング言語Gallina（英語版）を用いる。フランス国立情報学自動制御…

Coq
Coq
作者 フランス国立情報学自動制御研究所, パリ第7大学, エコール・ポリテクニーク, パリ第11大学, リヨン高等師範学校
初版 4.10 (1989年)
最新版
9.0.0 / 2025年3月12日 (17か月前) (2025-03-12)[1]
リポジトリ
ウィキデータを編集
プログラミング
言語		 OCaml
対応OS マルチプラットフォーム
対応言語 多言語対応
種別 定理証明支援系
ライセンス GNU LGPL 2.1
公式サイト The Coq Proof Assistant
テンプレートを表示

Coqは、証明支援システムの一つ。Coqの核はプログラミング言語Gallina（英語版）を用いる。フランス国立情報学自動制御研究所のPI.R2チーム（PPS研究所内にある）が、エコール・ポリテクニーク、フランス国立工芸院、パリ第7大学、パリ第11大学と（かつてリヨン高等師範学校とも）共同して開発している。Hugo Herbelinが事実上の開発代表者である。

2023年10月11日、開発チームは名称をCoqからThe Rocq Proverに変更すると発表し、コードベースやウェブサイトなどの更新を開始した[2]。

特徴

CoqはCalculus of constructions（英語版）という高階型システム(Thierry CoquandとGérard Huetが1984年に創始したもので、英語ではCoCと略せてシステム名Coqに至る)に基づく。正しい証明は正しく型がつくラムダ式であるというカリー＝ハワード同型対応を利用しているので、Coqの証明言語は型付きラムダ計算の一種である。1991年以降Coqが用いているCalculus of Constructionsの変種は、Christine Paulin-Mohringによるもので、帰納的構成を直接含み、Calculus of Inductive Constructions（CIC）という名前がついている。

Coqには

  • 主張を操作する機能
  • 主張の証明を機械的に検査する機能
  • 形式的証明の探索を支援する機能
  • 依存型を用いたプログラムを記述する機能
  • 実行可能な検証済みプログラムを抽出する機能

がある。

加えてCoqには証明の自動化機能が増えている。中にはomegaタクティクというものがあり、プレスバーガー算術の大部分を決定できる。

Coqの最大の達成の中には、

  • 四色定理: Georges GonthierとBenjamin Wernerによって、完全に機械化された証明が2004年に完了した[3]。
  • CompCert: C言語のコンパイラで、Coqによって開発され証明がつき、2006年にリリースされた[4]。
  • Feit-Thompson定理（英語版）: Georges Gonthierと彼のグループによって、2012年9月に証明が完了した[5]。

がある。

CoqはGNU LGPLライセンスで配布されている自由ソフトウェアである。

Ssreflect拡張

Georges GonthierのチームがSsreflect（small scale reflectionの略）というCoqの拡張を開発している。拡張はreflection用の機能にとどまらず、Coqの多くのタクティクの改良版を提供する上に、証明の保守性を高めるコーディング慣習も含んでいる。 Ssreflectの機能には下のようなものがある。

  • 保守性を高めるための機能
    • Coqが自動生成した識別子をユーザが指定できなくなって、Coqのバージョンアップによって証明が通らなくなることを防止する機能
    • 証明の枝を完結させることを明示して、軽微な証明を自動で行わせられる上に、証明が通らなくなったときに修正するべき範囲がわかりやすくなる機能
  • 主張を直接証明する代わりに、Coq内で検証済みの判定機を実行するreflectionという技法に特化した証明タクティク
  • 有限集合上の和や積などの大きな演算子を扱う機能
  • 代数のライブラリ

SsreflectはCeCill-BとCecill-2.0でデュアルライセンスされていて、自由に利用できる。Ssreflectの最新版はCoq 8.4上で動く[6]。

脚注

[脚注の使い方]
  1. ^ “Release Rocq 9.0.0”. 2025年3月23日閲覧。
  2. ^ “Change of Name: Coq -> The Rocq Prover”. 2025年3月23日閲覧。
  3. ^ A computer-checked proof of the Four Colour Theorem Georges Gonthier
  4. ^ CompCertのページ(英語)
  5. ^ 証明完了のアナウンス(英語)
  6. ^ Ssreflectの配布元(英語)

参考文献

  • 萩原学、アフェルト・レナルド『Coq/SSReflect/MathCompによる定理証明　フリーソフトではじめる数学の形式化』森北出版、2018年4月18日。ISBN 978-4-627-06241-2。 

関連項目

外部リンク

Content Disclaimer

Informasi ini disarikan dari Wikipedia dan disajikan kembali untuk tujuan edukasi. Konten tersedia di bawah lisensi CC BY-SA 3.0. Kami tidak bertanggung jawab atas ketidakakuratan data yang bersumber dari kontribusi publik tersebut.

  1. The information displayed on this website is sourced in part or in whole from Wikipedia and has been adapted for the purpose of restating it. We strive to provide accurate and relevant information, however:
  2. There is no guarantee of absolute accuracy. Wikipedia is an open, collaborative project that can be edited by anyone, so information is subject to change.
  3. It is not intended to constitute professional advice. The content displayed is for informational and educational purposes only. For important decisions (e.g., medical, legal, or financial), please consult a professional.
  4. Content copyright. Wikipedia is licensed under the Creative Commons Attribution-ShareAlike License (CC BY-SA). This means that content may be reused with appropriate attribution and shared under a similar license.
  5. Responsible use. Any risk arising from the use of information from this website is entirely the responsibility of the user.