■

メイドさんに教わったCoqというものをマニュアルと格闘しながら理解したつもり。

Variables A B : Prop

A と B は命題だよ。

Theorem mp : (A->B)->A->B.
auto.
Qed.

modus ponens ぐらいは自動で証明できるよ。

Variable p : A->B.
Variable a : A.

なぜか知らないけど、A->B が証明できたとするよ。証明は p だよ。
なぜか知らないけど、A も証明できたとするよ。証明は a だよ。

Goal B.
exact (mp p a).
Qed.

そしたら B も証明できるよ。(mp p a) が証明だよ。

証明した事実は関数として使えるんだ！！！
というか、こういう基本的なことはチュートリアルの最初に書いといてくれ。
自分で気づくまで三日も無駄に費やした…