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.
(** [] *)