Coqで選択公理⇔ツォルンの補題を証明してみた(前編)

(*
このプログラムはZ^- -Inf(ZFCから置換公理、無限公理、基礎の公理、選択公理を除いた公理系)で
選択公理(選択関数の存在)とツォルンの補題が同値になることを一から証明しています。
予備知識はCoqの使い方だけと思います。
他のライブラリは必要ありません。
コードに関してはもっと短くしたり、記号の名前もいい感じにできると思いますが、時間の都合で妥協しています、お許しください。

選択公理(選択関数の存在)⇒ツォルンの補題の証明でタワーを使っています。
タワーの定義から空集合がタワーの元になることを削れるようなので、その分証明を短くしました。
*)

(*排中律*)
Axiom Middle:forall a:Prop, a\/~a.

(*背理法*)
Theorem RAAF:forall a:Prop, (~a -> False) -> a.
Proof.
intros.
specialize (Middle a).
intro.
destruct H0.
apply H0.
apply H in H0.
destruct H0.
Qed.

(*背理法のコマンド*)
Ltac RAA:=apply RAAF; intro.

(*一意性*)
Theorem Uni:forall P:Set -> Prop, (exists! x:Set, P x) -> forall x y:Set, P x -> P y -> x=y.
Proof.
intros.
destruct H.
destruct H.
apply H2 in H0.
apply H2 in H1.
rewrite <- H0.
apply H1.
Qed.

Section Axioms.

(*所属関係∈*)
Axiom In:Set -> Set -> Prop.

(*公理系はZ^- -Inf*)
(*外延性公理*)
Axiom AxEx: forall x y:Set,(forall z:Set, In z x <-> In z y) -> x = y.

(*分出公理図式*)
Axiom AxSS: forall (P:Set -> Prop) (x:Set), exists y, forall z:Set, In z y <-> In z x /\ P z.

(*和集合公理*)
Axiom AxUnion: forall x:Set, exists u, forall y z:Set, In z y -> In y x -> In z u.

(*対公理*)
Axiom AxPairing: forall x y:Set, exists p, In x p /\ In y p.

(*冪集合公理*)
Axiom AxPower: forall x:Set, exists p, forall z:Set, (forall y:Set, In y z -> In y x) -> In z p.

End Axioms.

Section Extensionality_Specification.

(*部分集合⊆*)
Definition Sbs(x y:Set):= forall z:Set, In z x -> In z y.

(*部分集合の反射性*)
Theorem RefSbs:forall x:Set, Sbs x x.
Proof.
unfold Sbs.
intros.
apply H.
Qed.

(*部分集合の推移性*)
Theorem TraSbs:forall x y z:Set, Sbs x y -> Sbs y z -> Sbs x z.
Proof.
unfold Sbs.
intros.
apply H0.
apply (H z0 H1).
Qed.

(*部分集合の反対称性*)
Theorem AnSySbs:forall x y:Set, Sbs x y -> Sbs y x -> x = y.
Proof.
intros.
apply AxEx. (*外延*)
split.
apply H.
apply H0.
Qed.

(*重要*)
(*{x|P(x)}の存在*)
Theorem ExSetIff: forall P:Set -> Prop, 
  (exists x, forall z:Set, P z -> In z x)
  -> exists y, forall z:Set, In z y <-> P z.
Proof.
intros.
destruct H.
specialize (AxSS P x).
intro.
destruct H0.
exists x0.
split.
intro.
apply H0.
apply H1.
intro.
apply H0.
split.
apply (H z H1).
apply H1.
Qed.

(*{x|P(x)}のwell-defined*)
Theorem WDSet: forall P:Set -> Prop,
 (exists y, forall z:Set, In z y <-> P z)
 -> exists! y, forall z:Set, In z y <-> P z.
Proof.
intros.
destruct H.
exists x.
split.
apply H.
intros.
apply AxEx. (*外延*)
intro.
specialize (H z).
specialize (H0 z).
split.
intro.
apply H0.
apply H.
apply H1.

intro.
apply H.
apply H0.
apply H1.
Qed.

(*重要*)
(*{x|P(x)}のwell-defined*)
Theorem WDSetIffU: forall P:Set -> Prop, 
  (exists x, forall z:Set, P z -> In z x)
  -> exists! y, forall z:Set, In z y <-> P z.
Proof.
intros.
apply WDSet.
apply (ExSetIff P H).
Qed.

(*共通部分のwell-defined*)
Theorem WDBCap:forall a:Set, 
 (exists w, In w a) ->
 exists!i, forall z:Set, In z i <-> forall x:Set, In x a -> In z x.
Proof.
intros.
destruct H.
apply WDSetIffU.
exists x.
intros.
apply (H0 x H).
Qed.

Axiom BCap:Set -> Set.
Axiom AxBCap:forall a z:Set, (exists w, In w a) ->
 In z (BCap a) <-> forall x:Set, In x a -> In z x.

(*0個の共通部分は意地でも回避*)
Theorem AxInBCap:forall a w z:Set,
 In w a -> In z (BCap a) <-> forall x:Set, In x a -> In z x.
Proof.
intros.
apply (AxBCap a z).
exists w.
apply H.
Qed.

(*z∈a⇒∩a⊆z*)
Theorem BCapSbs:forall a z:Set, In z a -> Sbs (BCap a) z.
Proof.
unfold Sbs.
intros.
apply (AxInBCap a z z0 H).
apply H0.
apply H.
Qed.

End Extensionality_Specification.

Section Pairing_Union.

(*対集合のwell-defined*)
Theorem WDPair:(forall x y:Set,
 exists! p:Set, forall z:Set, In z p <-> z = x \/ z = y).
Proof.
intros.
apply WDSetIffU.
specialize (AxPairing x y).
intro.
destruct H.
exists x0.
intros.
destruct H0.
rewrite H0.
apply H.
rewrite H0.
apply H.
Qed.

(*対集合∀z(z∈{x,y}:⇔z=x∨z=y)*)
Axiom PR:Set -> Set -> Set.
Axiom AxPR:forall x y z:Set, In z (PR x y) <-> z=x \/ z=y.

(*x∈{x,y}*)
Theorem PRInL:forall x y:Set, In x (PR x y).
Proof.
intros.
apply AxPR.
left.
reflexivity.
Qed.

(*y∈{x,y}*)
Theorem PRInR:forall x y:Set, In y (PR x y).
Proof.
intros.
apply AxPR.
right.
reflexivity.
Qed.

(*一点集合{x}:={x,x}*)
Definition Sngl(x:Set):= PR x x.

(*∀z(z∈{x}⇔z=x)*)
Theorem AxSngl:forall x z:Set, In z (Sngl x) <-> z=x.
Proof.
split.
intro.
apply AxPR in H.
destruct H.
apply H.
apply H.

intro.
apply AxPR.
left.
apply H.
Qed.

(*x∈{x}*)
Theorem InSngl:forall x:Set, In x (Sngl x).
Proof.
intro.
apply AxSngl.
reflexivity.
Qed.

(*{x}={y}⇒x=y*)
Theorem SnglMono:forall x y:Set, Sngl x = Sngl y -> x = y.
Proof.
intros.
apply AxSngl.
rewrite <- H.
apply InSngl.
Qed.

(*{x,y}={z}⇒x=z∧y=z*)
Theorem PRSnglEQ:forall x y z:Set, PR x y = Sngl z -> x = z /\ y = z.
Proof.
intros.
split.
apply AxSngl.
rewrite <- H.
apply PRInL.

apply AxSngl.
rewrite <- H.
apply PRInR.
Qed.


(*順序対(x,y):={{x},{x,y}}*)
Definition OP(x y:Set):= PR (Sngl x) (PR x y).

(*順序対の特徴づけ*)
Theorem OPC:forall x y X Y:Set, OP x y = OP X Y -> x = X /\ y = Y.
Proof.
intros.
unfold OP in H.

cut (x = X).
intro.
split.
apply H0.
rewrite H0 in H.

cut (Y = X \/ Y = y).
intro.
destruct H1.
rewrite H1 in H.
rewrite H1.
apply (PRSnglEQ X y X).
apply (PRSnglEQ (Sngl X) (PR X y)).
rewrite H.
reflexivity.

rewrite H1.
reflexivity.

cut (PR X Y = Sngl X \/ PR X Y = PR X y).
intro.
destruct H1.
left.
apply (PRSnglEQ X Y X H1).

apply AxPR.
rewrite <- H1.
apply PRInR.

apply AxPR.
rewrite H.
apply PRInR.

cut (Sngl x = Sngl X \/ Sngl x = PR X Y).
intro.
destruct H0.
apply SnglMono.
apply H0.
symmetry in H0.
symmetry.
apply (PRSnglEQ X Y x H0).

apply AxPR.
rewrite <- H.
apply (PRInL (Sngl x) (PR x y)).
Qed.

(*分出->和集合公理の言い換え*)
Theorem AxUnionIff:
 (forall x:Set, exists u, forall y z:Set, In z y -> In y x -> In z u)
  <-> forall x:Set, exists u, forall z:Set, In z u <-> exists y, In y x /\ In z y.
Proof.
split.
intros.
apply ExSetIff.
specialize (H x).
destruct H.
exists x0.
intros.
destruct H0.
destruct H0.
apply (H x1 z H1 H0).

intros.
specialize (H x).
destruct H.
exists x0.
intros.
apply H.
exists y.
split.
apply H1.
apply H0.
Qed.

(*和集合公理の言い換え*)
Theorem AxUIff:forall x:Set, exists u, forall z:Set, In z u <-> exists y, In y x /\ In z y.
Proof.
apply AxUnionIff.
apply AxUnion.
Qed.

(*和集合のwell-defined*)
Theorem WDUnion:forall x:Set, exists!u, forall z:Set, In z u <-> exists y, In y x /\ In z y.
Proof.
intro.
apply WDSet.
apply AxUnionIff.
apply AxUnion.
Qed.

(*和集合*)
Axiom BCup:Set -> Set.
Axiom AxBCup:forall x:Set, forall z:Set, In z (BCup x) <-> exists y, In y x /\ In z y.

(*z∈y⇒y∈x⇒z∈∪x*)
Theorem InInBCup:forall x y z:Set, In z y -> In y x -> In z (BCup x).
Proof.
intros.
apply AxBCup.
exists y.
split.
apply H0.
apply H.
Qed.

(*y∈x⇒y⊆∪x*)
Theorem SbsBCup:forall x y:Set, In y x -> Sbs y (BCup x).
Proof.
intros.
unfold Sbs.
intros.
apply (InInBCup x y z H0 H).
Qed.

(*外延、分出、対、和集合*)
(*2つの集合の和集合のwell-defined*)
Theorem WDCup:forall x y:Set, exists!u, forall z:Set, In z u <-> In z x \/ In z y.
Proof.
intros.
apply WDSetIffU.
exists (BCup (PR x y)).
intros.
apply AxBCup.
destruct H.
exists x.
split.
apply PRInL.
apply H.
exists y.
split.
apply PRInR.
apply H.
Qed.

(*2つの集合の和集合*)
Axiom Cup:Set -> Set -> Set.
Axiom AxCup:forall x y z:Set, In z (Cup x y) <-> In z x \/ In z y.

(*x⊆x∪y*)
Theorem SbsCupL:forall x y:Set, Sbs x (Cup x y).
Proof.
unfold Sbs.
intros.
apply AxCup.
left.
apply H.
Qed.

(*y⊆x∪y*)
Theorem SbsCupR:forall x y:Set, Sbs y (Cup x y).
Proof.
unfold Sbs.
intros.
apply AxCup.
right.
apply H.
Qed.

(*x∪x=x*)
Theorem IdCup:forall x:Set, Cup x x = x.
Proof.
intro.
apply AxEx.
split.
intro.
apply AxCup in H.
destruct H.
apply H.
apply H.
intro.
apply AxCup.
left.
apply H.
Qed.

(*x⊆y⇒y⊆x∪{z}⇒x=y∨y=x∪{z}*)
Theorem SbsCupSnglOr:forall x y z:Set,
 Sbs x y -> Sbs y (Cup x (Sngl z)) -> x = y \/ y = Cup x (Sngl z).
Proof.
intros.
specialize (Middle (In z y)).
intro.
destruct H1.

right.
apply AxEx.
split.
apply H0.
intro.
apply AxCup in H2.
destruct H2.
apply (H z0 H2).
apply AxSngl in H2.
rewrite H2.
apply H1.

left.
apply AxEx.
split.
apply H.
intro.
specialize (H0 z0 H2).
apply AxCup in H0.
destruct H0.
apply H0.
apply AxSngl in H0.
rewrite H0 in H2.
contradiction.
Qed.

Section Pairing_Union.

中編
https://qiita.com/Meizen_OS/items/4dde1a9c8fbfa649db0a

後編
https://qiita.com/Meizen_OS/items/662eef622cf989f8b5ba