前提知識

Coq
進次郎構文
Coqをパソコンに入れなくてもこのサイトで一応遊べる
http://proofweb.cs.ru.nl/

本文

今回は任意の命題 aについて、aならばaが成り立つことを証明してみます。
Coqでは命題の型はPropと表現されるのでちゃんと書くと

となります。
Coqで証明するには証明したいものを型として持つオブジェクトを一つ提示すればよいです。
例えばnatという自然数の型を証明したければ、nat型の自然数を一つ（例えば８１０など）を提示すれば証明になります。

Goal Type.
Proof.
exact Type.
Qed.

Goal Type.
Proof.
exact Prop.
Qed.

Goal Type.
Proof.
exact Set.
Qed.

Goal Prop.
Proof.
exact True.
Qed.

Goal Set.
Proof.
exact nat.
Qed.

Goal nat.
Proof.
exact 810.
Qed.

以下は恒等関数の型です。

Theorem A(a:Type):a->a.
Proof.
intro X.
exact X.
Defined.

Definition id(U:Type)(x:U):=x.

Goal A=id.
Proof.
split.
Qed.

PropはType型なので、定理Aの系の一つとして冒頭の進次郎定理が証明できました。

Goal forall a:Prop,a->a.
Proof.
exact A.
Qed.

Goal forall a:Set,a->a.
Proof.
exact A.
Qed.

Goal Type->Type.
Proof.
apply A.
Qed.

Goal nat->nat.
Proof.
apply A.
Qed.