\[\begin{split}\newcommand{\alors}{\textsf{then}} \newcommand{\alter}{\textsf{alter}} \newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\bool}{\textsf{bool}} \newcommand{\case}{\kw{case}} \newcommand{\conc}{\textsf{conc}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\conshl}{\textsf{cons\_hl}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\EqSt}{\textsf{EqSt}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\false}{\textsf{false}} \newcommand{\filter}{\textsf{filter}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\from}{\textsf{from}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\haslength}{\textsf{has\_length}} \newcommand{\hd}{\textsf{hd}} \newcommand{\ident}{\textsf{ident}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\lb}{\lambda} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\Nat}{\mathbb{N}} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\Prod}{\textsf{prod}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\si}{\textsf{if}} \newcommand{\sinon}{\textsf{else}} \newcommand{\Sort}{\cal S} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\true}{\textsf{true}} \newcommand{\Type}{\textsf{Type}} \newcommand{\unfold}{\textsf{unfold}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)} \newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \newcommand{\zeros}{\textsf{zeros}} \end{split}\]

はじめに

この文書は証明アシスタント Coq のリファレンスマニュアルです。Coqを初めて使う方は、まずチュートリアルを読むことをお勧めします。https://coq.inria.fr/documentation や https://github.com/coq/coq/wiki#coq-tutorials には、幾つかのチュートリアルへのリンクがあります。

Coq は、数学的な証明を構築するためにデザインされました。特に、形式仕様やプログラムを記述したり、プログラムが仕様に沿っていることを検証することを目的としています。Coqは、 Gallina と呼ばれる仕様記述言語を提供します。Gallina の項はプログラム・プログラムの性質・性質の証明を表現できます。カリー・ハワード同型対応 を使えば、プログラム・性質・証明は全て Calculus of Inductive Constructions という一つの言語で表現できます。これは \(\lambda\) 計算にリッチな型システムが付いたものです。Coq における論理的判断は全て型付け判断です。Coq システムの心臓部は型検査アルゴリズムで、これは証明の正しさを検査します。言い換えれば、このアルゴリズムはプログラムがその仕様に準拠するか検査します。また、Coq は、 タクティック と呼ばれるプログラムを用いて証明を構築する、対話的証明アシスタントも提供します。

Coq が提供する全てのサービスは、 Vernacular と呼ばれるコマンド言語を読み込ませることで利用できます。

Coq には、ユーザが入力した端からコマンドを実行していく対話モードと、ファイルに書かれたコマンドを順に実行していくコンパイルモードがあります。

  • 対話モードでは、ユーザは順を追って証明を構築したり、利用できる定理や定義をシステムに問い合わせたりできます。対話モードは一般的に, CoqIDE (Coq Integrated Development Environment にて記載)やProof-General [Asp00] 1 を入れた Emacs 、またはブラウザ上で動作する jsCoq (https://github.com/ejgallego/jscoq) のようなIDEの助けを借りて実行されます。デバッグのために、 read-eval-print-loop である coqtop を直接用いることもできます。

  • コンパイルモードは、開発したもの全てを受け取り、その正当性を保証する証明チェッカとして機能します。さらに、 Coq コンパイラは、入力のコンパクトな表現を持つ出力ファイルを生成します。コンパイルモードは coqc コマンドで実行されます。

参考

The Coq commands.

この文書の読み方

この文書はリファレンスマニュアルであり、通読するものではありません。目的の文書を素早く見つけるために、色々な索引を使うことをお勧めします。総合索引に加え、タクティックやコマンド、エラーメッセージ・警告に特化した索引があります。とはいえ、このマニュアルも以下のような構造を持っています。

  • 第1部では、仕様記述言語 Gallina について説明します。仕様記述言語 Gallina および Gallina の拡張 の章では、構文および Calculus of Inductive Constructions におけるプログラムや証明・定理の意味について説明します。The Coq library の章では Coq の標準ライブラリについて説明します。Calculus of Inductive Constructions の章は数学の形式的な説明です。The Module System の章ではモジュールシステムについて説明します。

  • 第2部では、証明エンジンについて説明します。ここは6つの章に分かれています。Vernacular commands の章では、対話的証明と直接的には関係のないコマンド (Vernacular コマンド) を全て挙げます。コマンドは、環境への要求、完全/部分的な評価、ファイルの読み込みやコンパイルなどを行います。どのように証明を始め、終わればいいのか、どうすれば証明を並行して進めることができるかは、 Proof handling の章で説明しています。Tactics の章では、証明の1つまたは複数のステップを成すコマンド (タクティック) を全て挙げます。これらのタクティックを組み合わせて複雑な証明戦略を作るための言語については The tactic language の章で述べています。タクティックの具体例は Detailed examples of tactics の章で説明します。最後に、証明言語 SSReflect について The SSReflect proof language の章で説明します。

  • 第3部は、 Syntax extensions and interpretation scopes の章で|Coq| の構文の拡張方法を、 Proof schemes の章で帰納法の原理を新たに定義する方法を説明しています。

  • 第4部はより実用的なツールについて文書化しています。まず、 The Coq commands の章で、coqc (コンパイルモード) と coqtop (対話モード) の使い方およびオプションについて説明します。次に、 Utilities の章で、 Coq ディストリビューションに付属する様々なユーティリティについて説明します。最後に、 Coq Integrated Development Environment の章で、 CoqIDE について説明します。

  • 第5部では、型強制・正準構造・型クラス・プログラム抽出・特殊なソルバとタクティックといった、いくつかの高度な機能について説明します。全ての項目を知りたい場合は、目次を参照してください。

その他の文書一覧

このマニュアルは Coq についてユーザが求める文書が全て含まれているわけではありません。以下の文書からも様々な情報を得ることができます。

チュートリアル

このマニュアルと対を成す Coq チュートリアルは、新規ユーザが型理論の知識なしに Coq で証明を構築できるようになるまで、優しく導入することを目的としています。その後は、再帰型についてのチュートリアル (RecTutorial.ps) を読むのもいいでしょう。

インストール方法

ソースに付属するテキストファイル INSTALL では、 Coq をインストールする方法について説明しています。

Coq 標準ライブラリ

Coq 標準ライブラリのコメント付きソースコード (仕様のみで、証明を省いたもの)は https://coq.inria.fr/stdlib/ で閲覧できます。

目次

索引

はじめに

言語

証明エンジン

ユーザ拡張

実用ツール

付録

Reference

ライセンス

この作品 (Coq リファレンスマニュアル) はオープン・パブリケーション利用許諾契約書 (v1.0 かそれ以降) で指定された条件と制約に従う限り配布することができる(契約書の最新の版は現在のところ http://www.opencontent.org/openpub/で入手可能である)。オプションAおよびBは選択しない。

1

Proof-General は https://proofgeneral.github.io/から入手可能です。また、マイナーモード Company-Coq [PCC16] (https://github.com/cpitclaudel/company-coq) で拡張することもできます。