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