CoqIdeを使ってみる
実は、私もマニュアルを読んだわけではないのですが、適当にいじってみたら、 Coqよりも使いやすい部分もあったので、ここで簡単に紹介しておきます。
上記は起動したばかりの状態です。もしここから、直接入力して定理の証明を したいなら、画面左側の、Unnamed Bufferなるタブの付いている白いところに 入力していくことになります。やってみましょう。
Unnamed Bufferのところに入力しただけなら、Enterキーを押したくらいでは CoqIdeは何も反応してくれません。上記の図ではSection ML.からapply H.まで 文字の背景が緑色になっていますが、そうはなっていないと思います。 CoqIdeに反応してもらうには、次のように
Navigation→Forwardとすると、1行ずつ文字の背景が緑になって、しかも 画面右側の上半分の白いところにCoqのときのような出力がでます。（Coqのときは 出力があったのに、CoqIdeでは何も出力されないこともあるようです。 上記の例で言えば、CoqではVariables A B C:Prop.の後も、A is assumedのような 出力がありますが、CoqIdeでは何も出力されません。）
CoqIdeでいいのは、Navigation→Backwardで、証明を戻ることができること です。Coqでも証明を戻ることは可能ですが、やはり見易さはCoqIdeの方が ずっと上です。また、どういう規則かはわかりませんが、上記でもわかるように、 いくつかの単語の色が赤になったり青になったりしています。スペルミスが 発見しやすくて助かります。
また、画面左側の白い部分でのコピーや貼り付けは、Edit→Copyでコピー、 Edit→Pasteで貼り付けができます。WindowsのときのようにCtrl+cや、Ctrl+vでも OKです。ただ、Coqの出力（画面右上の白い部分）でのコピーは、（コピーしたい 範囲をマウスでドラッグして選んだ上で）Ctrl+Insertでできます。