自動証明処理系の coq を使って簡単な3段論法を証明してみる。

まず coq を起動する。

% coqtop
Coq <

命題 A B C について考えてみるよ。

Coq < Variables A B C : Prop.
A is assumed
B is assumed
C is assumed

「A ならば B 」というのは命題だよね?

Coq < Check (A -> B).
A -> B
: Prop

じゃあ簡単なトートロジー「A ならば B ならば C」ならば「A ならば B」であり「A ならば C」を証明するよ。

Coq < Goal (A -> B -> C) -> (A -> B) -> A -> C.
1 subgoal

============================
(A -> B -> C) -> (A -> B) -> A -> C

導入する。

Coq < intro H.
1 subgoal

H : A -> B -> C
============================
(A -> B) -> A -> C

いっぺんに同時に導入できるよ。

Coq < intros H’ HA.
1 subgoal

H : A -> B -> C
H’ : A -> B
HA : A
============================
C

仮説 H を適用します。

Coq < apply H.
2 subgoals

H : A -> B -> C
H’ : A -> B
HA : A
============================
A

subgoal 2 is:
B

仮説 HA は正しいよ。

Coq < exact HA.
1 subgoal

H : A -> B -> C
H’ : A -> B
HA : A
============================
B

そして H’ を適用します。

Coq < apply H’.
1 subgoal

H : A -> B -> C
H’ : A -> B
HA : A
============================
A

Coq < assumption.
Proof completed.

証明終わり。

うー、もっとカッコイイ証明をいろいろやってみたいんだけど圧倒的に脳みそが足りない。