Library auto

auto

まず、forall (P : Prop), P -> P という命題を例として考えます。 この命題は auto 一発で証明できます。

ここで No more subgoals. と表示されて、証明できたことがわかります。 構築された証明項は Show Proof というコマンドで表示できます。

(fun (P : Prop) (H : P) => H)

Show Proof とすると私の環境 (CoqIDE) では以下のように表示されます。

(fun (P : Prop) (H : P) => H)

(fun (P : Prop) (H : P) => H) は Gallina の式です。 Gallina というのは Coq に組み込まれている ML のような言語で、 ここで使っているように証明項にも用いますし、 Gallina で直接プログラムを書くこともあります。 (fun (P : Prop) (H : P) => ...) というのは Gallina の関数抽象で、カリー化されているのでじつは (fun (P : Prop) => (fun (H : P) => ...)) と同じものです。 関数型言語を知っていればだいたいわかるとは思いますが、 (fun (P : Prop) => ...) は Prop 型の値 P を受け取って ... の部分を返す関数抽象です。 Prop というのは命題の型です。 ですから、Prop 型の値である P は命題です。 というわけでカリーハワード対応により P は型でもあります。 ですが、このように型を普通の引数として受け取るのはちょっと見慣れない形かもしれません。 Gallina では型も普通に引数として 受けとることができ、受け取った型はそれ以降の引数の型などに使うことができます。 (fun (P : Prop) (H : P) => H) は、 プログラムの世界の言葉で表現するなら、 Prop 型の値Pを受け取り、P型の値Hを受け取り、Hを返す関数です。 証明の世界の言葉で表現するなら、 命題Pを受け取り、Pの証明Hを受け取り、Hを返す関数です。 そのような関数が存在することが、forall (P : Prop), P -> P の証明である、ということです。

ところで、Qed としたときに Unnamed_thm is defined と表示されます。 つまり、Unnamed_thm という定理が定義された、ということですが、 もちろん、後で使いたい定理にこういう内容に関係ない名前をつけるのはよくありません。 自分で定理に名前をつけるときには Goal ではなく Lemma や Theorem で証明を始めます。 Lemmaというのは補題で、Theoremというのは定理ですが、 機能的な違いはとくにありません。ここでは常に Lemma をつかうことにします。

証明しようとしているのは上と同じく forall (P : Prop), P -> P という命題であり、 これはその証明に LemmaPP という名前をつけよう、という指定です。

証明が終った後、Print LemmaPP とすると以下のように表示されます。

LemmaPP = fun (P : Prop) (H : P) => H
     : forall P : Prop, P -> P

これは、LemmaPP の値は fun (P : Prop) (H : P) => H という値であり、 その型は forall P : Prop, P -> P である、という意味です。 プログラムの世界で解釈すれば、まさに LemmaPP という定数は 構築した証明項を値として定義されている、 というわけです。