Coq 演習 1

こちらの PDF が素晴らしいとのことなので 「Coq/SSReflect/MathComp による定理証明」より先にやってみる。
http://herb.h.kobe-u.ac.jp/coq/coq.pdf

2.1.8 まで読んだので演習問題をやる。2.1.5 の論理和のところでちょっと詰まった。destruct して 2 つにゴールが割れるところは、1 つ目と 2 つ目でゴールペインの仮定が変わるのね。あと contradiction は矛盾律であり、~A と ~~A なので終わりということらしい。超初歩らしい。

演習問題 1. はできた。

Section Practice1.
Variables A B C: Prop.

Lemma P1:  (A -> (B -> C)) -> ((A -> B) -> (A -> C)).
Proof.
intros.
apply H.
trivial.
apply H0.
trivial.
Qed.

Lemma P2: ~(A /\ B) -> (A -> ~B).
Proof.
intros.
intro.
apply H.
split.
trivial.
trivial.
Qed.

Lemma P3: ((A /\ B) -> C) -> (A -> (B -> C)).
Proof.
intros.
apply H.
split.
trivial.
trivial.
Qed.

Lemma P4: (B -> A) -> ((C -> A) -> ((B \/ C) -> A)).
Proof.
intros.
destruct H1.
apply H.
trivial.
apply H0.
trivial.
Qed.

Lemma P5: (~A /\ ~B) <-> ~(A \/ B).
Proof.
split.
intros.
intro.
destruct H.
destruct H0.
apply H.
trivial.
apply H1.
trivial.

intros.
split.
intro.
apply H.
left.
trivial.
intro.
apply H.
right.
trivial.
Qed.

Lemma P6: (~A \/ ~B) -> ~(A /\ B).
Proof.
intros.
intro.
destruct H0.
destruct H.
apply H.
trivial.
apply H.
trivial.
Qed.

End Practice1.