まずは
いきなりCoqで定理の証明をするのではなく、まずはいじってみます。 ではCoqを起動してみましょう。（今回はCoqIdeではなく、Coqの方にしましょう。）
| Welcome to Coq 8.1pl3 (Dec. 2007) Coq < |
コマンドプロンプトのような窓がでて、その中に上記のような文字が表示されていることと思います（数字は多少違うかも）。
その中の Coq <のことをCoqの プロンプト（単にプロンプト）と呼ぶことにします。但し、 < の前にある Coqの部分は、 状況に応じて変化しますので、そのときはびっくりしないでください。
さて、インストールしたばかりのCoqでも自然数は理解しているはずです。 Checkコマンドで確認してみましょう。（Coqは大文字と小文字を区別しますので注意 してください。また、他の場所でコピーした文字列をCoqに貼り付けることができ ます。Coqの窓の一番上のバー（左端にCoqと文字がある）を右クリックして、編集->貼り付けを選べば貼り付けることができます。）
| Welcome to Coq 8.1pl3 (Dec. 2007) Coq < Check 3.<Enter> 3 : nat Coq < |
Check 3. の最後のピリオドは忘れないでください。Coqでは、命令の最後に必ずピリオドを 打たなくてはなりません。また、<Enter> の部分は、Enterキーを押すことを表したもので、皆さんの実際の画面には表示され ないはずです。（以後面倒なので、この<Enter>は、 なるべく表示しないで済ますことにします。）
さて、命令Check 3.に対してCoqの出力は
| 3 : nat |
と出ています。途中で改行が入っていますが、これは普通 3 : nat と表記します。 これは「3の型はnatである」とか「3はnat型である」とか、「3は型natを持っている」 などと読みます。そして、このnat型というのは、Coqの中で自然数を扱うための 型です。結局、Checkコマンドと言うのは型を確認する コマンドなのです。
Coqは十進法を理解しているので、「3」なる表記が使えますが、本当の姿は違います。Coqでの「3」の本当の姿を見てみましょう。それにはUnset Printing Notations.なる命令を使います。（その命令を元に戻すにはSet Printing Notations.なる命令を使います。）
| Welcome to Coq 8.1pl3 (Dec. 2007) Coq < Check 3. 3 : nat Coq < Unset Printing Notations. Coq < Check 3. S (S (S O)) : nat Coq < Check 4. S (S (S (S O))) : nat Coq < Check 0. O : nat Coq < Set Printing Notations. Coq < Check 3. 3 : nat Coq < Check 0. 0 : nat Coq < |
上記のUnset Printing Notations.の直後のCheck 3.に対するCoqの出力を見ると、 「3」の本当の姿は「S (S (S O))」であることがわかります。また、「0」（数字の ゼロ）の本当の姿は「O」（アルファベットの大文字のオー）であることにも注意 してください。
せっかく自然数を扱ったので、Coqに計算もさせてみましょう。
|
Coq < Eval compute in ((5 - 1) * 7). = 28 : nat Coq < Eval compute in (5 - 8). = 0 : nat Coq < |
Coqでは、掛け算の記号は「*」を使います。また、今のCoqの状態ではCoqは自然数は理解していても整数は理解していないはずです。つまり、負の数を理解していません。上記の「5 - 8」の計算はエラーにしてもいいのでしょうが、Coqでは「小さい自然数 引く 大きい自然数」は0にしてしまうようです。（というか、帰納的関数ではあたりまえ？）