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

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

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

Coqで書いた定理を証明してみる

Coq入門 intro intros apply Qed

証明モードのときは今までのCoqコマンドに加えて、タクティックというものを使うことができる。
タクティックは必ず小文字で始まり、ドットで終わる。

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

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

A : Prop B : Prop C : Prop H : (A->B->C) H0 : (A->B) H1 : A ======================================= C
s < apply H.
subgoal 1

A : Prop B : Prop C : Prop H : (A->B->C) H0 : (A->B) H1 : A ======================================= A
subgoal 2 B
s < apply H1. (* subgoal 1 証明終わり *)

A : Prop B : Prop C : Prop H : (A->B->C) H0 : (A->B) H1 : A ======================================= B
s < apply H0.

A : Prop B : Prop C : Prop H : (A->B->C) H0 : (A->B) H1 : A ======================================= A
s < apply H1. (* subgoal 2 証明終わり *)
Proof completed.

最後にQedというCoqコマンドでこの定理の証明を完成させることができる。

s < Qed.
証明
s is defined.

Coq <