Coq 演習 2

http://herb.h.kobe-u.ac.jp/coq/coq.pdf の続き。
2.1.9 古典論理 まで読んだ。排中律を手に入れた。

演習問題 2.

Require Import Classical.

Variable A B C: Prop.

Lemma Taiguu: (~B -> ~A) -> (A -> B).
Proof.
intros.
apply NNPP.
intro.
generalize H0.
apply H.
trivial.
Qed.

Lemma Peirce: ((A -> B) -> A) -> A.
Proof.
intros.
apply imply_to_or in H.
destruct H.
apply imply_to_and in H.
destruct H.
trivial.
trivial.
Qed.

Lemma P1: ~(A /\ B) -> ~A \/ ~B.
Proof.
apply not_and_or.
Qed.

Lemma P2: ((A -> ~A) -> B) -> ((A -> B) -> B).
Proof.
intros.
apply imply_to_or in H.
destruct H.
apply imply_to_and in H.
destruct H.
apply H0.
trivial.
trivial.
Qed.

Lemma P3: (~B -> ~A) -> ((~B -> A) -> B).
Proof.
intros.
apply imply_to_or in H.
destruct H.
apply NNPP in H.
trivial.
apply imply_to_or in H0.
destruct H0.
apply NNPP in H0.
trivial.
contradiction.
Qed.

Lemma P4: (A -> B) \/ (B -> A).
Proof.
apply NNPP.
intro.
apply not_or_and in H.
destruct H.
apply imply_to_and in H.
destruct H.
apply imply_to_and in H0.
destruct H0.
contradiction.
Qed.

一応解けた。感覚はまだよくわからないが、タブローのときのように -> を OR か AND に変えていくと道が開ける感はある。