Coqで定理を書いてみる

Coqは証明支援系 (Proof Assistant) と呼ばれるシステムで、定理などの証明を構築することができる。
今回はTheoremというCoqコマンドを使ってみる。
このコマンドを使って定理を記述し、宣言することができる。

文法 [Theorem 定理の名前 : 定理の内容.]

最後のドットを忘れないようにしよう。
例えば次のように s という名前の定理を宣言することができる。
定理を宣言するとCoqの証明モードに移行する。

Coq < Theorem s : forall A B C:Prop, (A->B->C) -> (A->B) -> A -> C.


=======================================
 forall A B C:Prop, (A->B->C) -> (A->B) -> A -> C
s <

証明をやっぱりやめて、もとのモードに戻りたいときはAbortというCoqコマンドを使う。

文法 [Abort.]

s < Abort.
Current goal aborted


Coq <