Coq 演習 3

http://herb.h.kobe-u.ac.jp/coq/coq.pdf の続き。
2.2.5 まで読んだ。

演習問題 3.

Section PredicateLogic.
Variable A: Type.
Variable P Q: A -> Prop.
Variable R: A -> (A -> Prop).
Variable t: A.

Lemma all_imply: (forall x: A, P x) -> P t.
Proof.
intro.
apply (H t).
Qed.

Lemma imply_exists: (P t) -> exists x, P x.
Proof.
intro.
exists t.
trivial.
Qed.

Lemma alpha_all: (forall x: A, P x) -> forall y: A, P y.
Proof.
intro.
intro.
apply H.
Qed.

Lemma all_not_not_ex: (forall x: A, ~P x) -> ~exists x: A, P x.
Proof.
intro.
intro.
destruct H0.
apply (H x).
trivial.
Qed.

Lemma Ex31: ~(exists x: A, P x) -> (forall x: A, ~P x).
Proof.
intro.
intro.
intro.
apply H.
exists x.
trivial.
Qed.

Lemma Ex32: (exists x: A, ~P x) -> ~(forall x: A, P x).
Proof.
intro.
intro.
destruct H.
apply H.
apply (H0 x).
Qed.

Lemma Ex33: (forall x, P x /\ Q x) <-> (forall x, P x) /\ (forall x, Q x). 
Proof.
split.
intro.
split.
apply H.
apply H.
intro.
destruct H.
split.
trivial.
trivial.
Qed.

Lemma Ex34: (exists x: A, P x \/ Q x) <-> (exists x: A, P x) \/ (exists x:A, Q x).
Proof.
split.
intros.
destruct H.
destruct H.
left.
exists x.
trivial.
right.
exists x.
trivial.
intros.
destruct H.
destruct H.
exists x.
left.
trivial.
destruct H.
exists x.
right.
trivial.
Qed.

Lemma Ex35: (exists x, forall y, R x y) -> (forall y, exists x, R x y).
Proof.
intros.
destruct H.
exists x.
trivial.
Qed.

一応解けたが、問題 3 のヒントに destruct (H x) の記載があるが実行するとエラーになる。何かわかってないことがありそうだが…