ZFCで遊ぼう！（２）

こんにちは、AAGです。Coqは初心者です。
今回は 前回 の続きとなっています。（概要以降はみなくても大丈夫です。）
今回は前回の内容のCoqによる証明です。
書き方は このサイト を参考にしました。
また、Coqの代わりに このサイト を使用しました。（動作に違いはないはずです。）

証明（コード）

      (*関係記号∊*)
Axiom In : Set -> Set -> Prop.
Notation "a ∊ b":=(In a b)(at level 50, no associativity).

(*外延性公理/axiom of extensionality*)
Axiom Ax_Ex : forall x y : Set, (forall z : Set, z ∊ x <-> z ∊ y) -> x = y.

(*分出公理図式/axiom schema of separation*)
Axiom Ax_S_S : forall (P : Set -> Prop)(x : Set),
 exists y, forall z : Set, z ∊ y <-> z ∊ x /\ P z.
Definition infty(N:Set):=(exists e : Set, e ∊ N /\ forall z : Set,~(z ∊ e))/\
(forall n : Set, n ∊ N -> exists s : Set, s ∊ N /\ forall z : Set, z ∊ s <-> z ∊ n \/ z = n).

(*無限公理/axiom of infinity*)
Axiom Ax_inf : exists X : Set, infty X.


(*自然数の集合の存在*)
Theorem nat_ex : exists N : Set, infty N /\ forall X x : Set, infty X-> x ∊ N -> x ∊ X.
Proof.
destruct Ax_inf. (*無限公理*)
destruct (Ax_S_S (fun y:Set => forall A:Set, infty A -> y ∊ A) x). (*分出公理*)
exists x0.
split.


destruct H.
split.
destruct H.
destruct H.
exists x1.
split.
apply H0.
split.
apply H.
intros.
destruct H3.
destruct H3.
destruct H3.
assert (x1=x2).
apply (Ax_Ex x1 x2). (*外延性公理*)
split.
intro.
apply (H2 z) in H6.
contradiction.
intro.
apply (H5 z) in H6.
contradiction.
rewrite H6.
exact H3.
exact H2.

intros.
apply H0 in H2.
destruct H2.
destruct (H1 n H2).
exists x1.
destruct H4.
split.
apply (H0 x1).
split.
exact H4.
intros.
generalize H6.
intro.
apply (H3 A) in H7.
destruct H6.
destruct (H8 n H7).
destruct H9.
assert (x2=x1).
apply (Ax_Ex x2 x1). (*外延性公理*)
split.
intro.
apply (H5 z).
apply (H10 z).
exact H11.
intro.
apply (H10 z).
apply (H5 z).
exact H11.
destruct H11.
exact H9.
exact H5.


intros.
destruct (H0 x1).
destruct (H3 H2).
apply (H6 X).
exact H1.
Qed.

    

おわりに

気が向いたらコメント等を使い、見やすさを向上させたいです。
何か、疑問点や間違った点、感想などをコメントしていただけると幸いです。
もし、次回があったら自然数の基本的な内容を証明したいと思います。
ありがとうございました。