Coqで証明　述語論理　スコープに関する命題の続き

Require Import Utf8 Classical.

Parameter U:Type.

Parameter P:U->Prop.

Parameter Q:Prop.

Parameter t:U.

Goal (∀x,P x)∧Q↔(∀x,P x∧Q).
Proof.
split.
intros.
destruct H.
split.
eapply H.
assumption.
split.
intro.
eapply H.
apply(H t).
Qed.

Goal (∃x,P x)∧Q↔(∃x,P x∧Q).
Proof.
split.
intro.
destruct H,H.
exists x.
split.
assumption.
assumption.
intro.
destruct H,H.
split.
exists x.
assumption.
assumption.
Qed.

Goal (∀x,P x)∨Q↔(∀x,P x∨Q).
Proof.
split.
intros.
destruct H.
left.
eapply H.
right.
assumption.
intro.
apply NNPP.
intro.
apply H0.
left.
intro.
destruct(H x).
assumption.
apply NNPP.
intro.
apply H0.
right.
assumption.
Qed.

Goal (∃x,P x)∨Q↔(∃x,P x∨Q).
Proof.
split.
intro.
destruct H.
destruct H.
exists x.
left.
assumption.
exists t.
right.
assumption.
intro.
destruct H,H.
left.
exists x.
assumption.
right.
assumption.
Qed.

Goal ((∀x,P x)→Q)↔(∃x,P x→Q).
Proof.
split.
intro.
apply NNPP.
intro.
apply H0.
exists t.
intro.
apply H.
intro.
apply NNPP.
contradict H0.
exists x.
intro.
contradiction.
intros.
destruct H.
apply H.
eapply H0.
Qed.

Goal ((∃x,P x)→Q)↔(∀x,P x→Q).
Proof.
split.
intros.
apply H.
exists x.
assumption.
intros.
destruct H0.
eapply H.
eassumption.
Qed.

Goal (Q→∀x,P x)↔(∀x,Q→P x).
Proof.
split.
intros.
eapply(H H0).
intros.
eapply H.
assumption.
Qed.

Goal (Q→∃x,P x)↔(∃x,Q→P x).
Proof.
split.
intro.
apply NNPP.
intro.
apply H0.
exists t.
intro.
destruct(H H1).
contradict H0.
exists x.
trivial.
intros.
destruct H.
exists x.
exact(H H0).
Qed.