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

証明モードのときは今までの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 <