読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

Coqで定理を書いてみる

Coq入門 Theorem Abort

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 <