Pixel Pedals of Tomakomai

北海道苫小牧市出身の初老の日常

Coqの証明と自然演繹の関係

「Aならば、AならばBならばB」の証明はCoq*1だと以下のように書けます。

Goal forall (A B : Prop), A -> (A -> B) -> B.
Proof.
intros A B.
intro.
intro.
apply H0.
apply H.
Qed.

なんでこれが証明になっているんでしょうか。

Coqのモデルは自然演繹*2だそうですので、自然演繹の推論規則に沿って考えてみます。

Coqでは人間と逆向きに推論を行っていますので、スタート地点は一番下のQed.の地点となります。

  A : Prop
  B : Prop
  H : A
  H0 : A -> B
  ============================

こんな風に4つの条件を仮定をした状態です。自然演繹ではこれに推論規則を適用していきますが、その過程で仮定が消えていきます。これらの仮定が全部消えてくれれば、特別な仮定なしに成り立つことが言えたことになるので、証明終了です。

apply H. を逆向きに実行すると、以下のようになります。これは「仮定Aの元でAが成り立つ」という当たり前の推論規則です。この段階ではまだ仮定は消えません。

  A : Prop
  B : Prop
  H : A
  H0 : A -> B
  ============================
   A

次に apply H0. を逆向きに適用します。これは⊃Eの規則に相当します。

  A : Prop
  B : Prop
  H : A
  H0 : A -> B
  ============================
   B

その手前の intro. は、 H0について⊃I に相当する操作をしていることになります。ここで仮定H0が消えます。

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

さらに手前の intro. は Hについて⊃I を実施しています。ここで仮定Hが消えます。

  A : Prop
  B : Prop
  ============================
   A -> (A -> B) -> B

一番最初のintros. は、∀Fに相当する操作で、これでAとBが消えます。

  ============================
   forall A B : Prop, A -> (A -> B) -> B

めでたく仮定なしで証明したい式が出てきました。これらの話をCoqではなく自然演繹っぽい記号で書くと以下のようになるでしょう。[]は、対応する番号の推論規則の適用で仮定が消えたことを示します。

[A](2)
--- apply H.
 A  [A->B](1)
----------- apply H0.
     B
----------(1) intro.
 (A->B)->B
-------------(2) intro.
A->(A->B)->B  [A:Prop](3)  [B:Prop](3)
------------------------------------(3) intros A B.
          ∀A ∀B A->(A->B)->B

他のtactic も、基本的には自然演繹の推論規則を組み合わせてできているんじゃないかなあと思います(Coq初心者なのでわかりませんけど!)。

*1:Coqについてはプログラミング Coqというシリーズがすごく良心的です。

*2:自然演繹については、直観主義論理の「自然さ」(1) 自然演繹というエントリがわかりやすいです。