証明の実際
実際にこれから、公理的集合論の定理をCoqを使って次々と証明していく わけですが、そのやり方は、まず定理（補題）とそれを証明するtacticsを列挙した テキストファイルを作ります。例えば次の
Section ML.
Variables A B C:Prop.
Theorem s : (A -> (B -> C)) -> (A -> B) -> (A -> C).
Proof.
intros H Hab Ha.
apply H.
assumption.
apply Hab.
assumption.
Qed.
End ML.
のような内容のテキストファイルです。このときファイルの拡張子は「.v」に します。例えば今の例ではsss.vとしましょう。 一番わかりやすいのは、CoqIdeでそのsss.vを開いてみることでしょうか。 そしてNavigation→Endをやってエラーが出なければ証明できていることに なります。コンパイルする方法もあります。やり方は（sss.vを開いた上で） Compile→Compile Bufferです。 この場合もエラーが出なければ、証明ができていることになります。さらに、 このコンパイルの場合、sss.voなる「.voファイル」が作成されます。 いずれ、しょっちゅうコンパイルすることになりますので、コンパイルの仕方は よく覚えておいてください。