# dist_not_existsとdist_exists_or (ソフトウェアの基礎、Coq)のメモ

```(** **** Exercise: 1 star (dist_not_exists)  *)
(** Prove that "[P] holds for all [x]" implies "there is no [x] for
which [P] does not hold." *)

Theorem dist_not_exists : forall (X:Type) (P : X -> Prop),
(forall x, P x) -> ~ (exists x, ~ P x).
Proof.
intros TypeX P H. (**xとXが紛らわしいので**)
unfold not.
intros H2.
destruct H2 as [m Hm].
apply Hm.
apply H with (x := m). Qed.
(** [] *)

(** **** Exercise: 2 stars (dist_exists_or)  *)
(** Prove that existential quantification distributes over
disjunction. *)

Theorem dist_exists_or : forall (X:Type) (P Q : X -> Prop),
(exists x, P x \/ Q x) <-> (exists x, P x) \/ (exists x, Q x).
Proof.
intros X P Q.
split.
- intros H0. destruct H0 as [m Hm]. destruct Hm as [HP | HQ].
* apply or_introl. apply ex_intro with (witness:= m). apply HP.
* apply or_intror. apply ex_intro with (witness:= m). apply HQ.
- intros H0. destruct H0 as [HP | HQ].
* destruct HP as [m Hm]. apply ex_intro with (witness:= m). apply or_introl. apply Hm.
* destruct HQ as [m Hm]. apply ex_intro with (witness:= m). apply or_intror. apply Hm. Qed.
(** [] *)```