move folder

Author: choukh

Meta.v Axiom/Meta.v

@@ -14,6 +14,7 @@ Tactic Notation "contra" := contra as ?H.
 
 Declare Scope set_scope.
 Delimit Scope set_scope with set.
+Delimit Scope type_scope with type.
 Open Scope set_scope.
 
 Parameter set : Type.
@@ -58,7 +59,12 @@ Qed.
 Notation "'∃' ! x .. y , P" :=
   (ex (unique (λ x, .. (ex (unique (λ y, P))) ..)))
   (at level 200, x binder, right associativity,
-   format "'[' '∃' ! '/ ' x .. y , '/ ' P ']'") : type_scope.
+   format "'[' '∃' ! '/ '  x .. y ,  '/ ' P ']'") : type_scope.
+
+Notation "'∃' ! x .. y ∈ A , P" :=
+  (∃! x, x ∈ A ∧ (.. (∃! y, y ∈ A ∧ P) ..))
+  (at level 200, x binder, right associativity,
+   format "'[' '∃' ! '/ '  x .. y  ∈  A ,  '/ ' P ']'") : set_scope.
 
 (* 经典明确描述 *)
 Axiom classical_definite_description : ∀ (A : Type) (P : A → Prop),

ZFC0.v Axiom/ZFC0.v

@@ -2,7 +2,7 @@
 (** adapted from the thesis by Jonas Kaiser, November 23, 2012 **)
 (** Coq coding by choukh, April 2020 **)
 
-Require Export ZFC.Meta.
+Require Export ZFC.Axiom.Meta.
 
 (**=== 公理1: 外延公理 ===**)
 (* 两个集合相等当且仅当它们包含相同的成员 *)
@@ -13,6 +13,15 @@ Proof.
   intros A B [x [Hx Hx']] Hext. apply Hx'. congruence.
 Qed.
 
+Tactic Notation "ext" :=
+  apply ExtAx; split; intros.
+
+Tactic Notation "ext" ident(H) :=
+  apply ExtAx; split; intros H.
+
+Tactic Notation "ext" ident(x) ident(H) :=
+  apply ExtAx; intros x; split; intros H.
+
 (** Sub是集合的子集关系。
     我们用 A ⊆ B 表示 "A是B的子集"，用 A ⊈ B 表示 "A不是B的子集"。 *)
 Definition Sub := λ A B, ∀x ∈ A, x ∈ B.
@@ -62,8 +71,7 @@ Qed.
 (* Introduction rule of empty set (空集的介入) *)
 Lemma EmptyI : ∀ A, (∀ x, x ∉ A) → A = ∅.
 Proof.
-  intros A E. apply ExtAx.
-  split; intros H.
+  intros A E. ext.
   - exfalso. eapply E. apply H.
   - exfalso0.
 Qed.
@@ -147,9 +155,9 @@ Qed.
 (* 空集的并集是空集 *)
 Fact union_empty : ⋃∅ = ∅.
 Proof.
-  apply ExtAx. split.
-  - intros. apply UnionAx in H as [a [H _]]. exfalso0.
-  - intros. exfalso0.
+  ext.
+  - apply UnionAx in H as [a [H _]]. exfalso0.
+  - exfalso0.
 Qed.
 
 (**=== 公理4: 幂集公理 ===**)
@@ -169,11 +177,8 @@ Proof. intros. apply PowerAx. apply sub_refl. Qed.
 (* 若集合是空集的幂集的成员，那么这个集合是空集 *)
 Example only_empty_in_power_empty: ∀ x, x ∈ 𝒫 ∅ → x = ∅.
 Proof.
-  intros.
-  apply PowerAx in H.
-  unfold Sub in H.
-  apply ExtAx. split; intros.
-  - apply H. apply H0.
+  intros. ext.
+  - apply PowerAx in H. apply H. apply H0.
   - exfalso0.
 Qed.
 
@@ -208,7 +213,7 @@ Qed.
 Lemma repl_ext : ∀ G F A, (∀a ∈ A, F a = G a) →
   {F a | a ∊ A} = {G a | a ∊ A}.
 Proof with auto.
-  intros. apply ExtAx. split; intros Hx.
+  intros. ext Hx.
   - apply ReplAx in Hx as [y [Hy Hx]].
     apply ReplAx. exists y. split... rewrite <- H...
   - apply ReplAx in Hx as [y [Hy Hx]].

ZFC1.v Axiom/ZFC1.v

@@ -2,7 +2,7 @@
 (** adapted from the thesis by Jonas Kaiser, November 23, 2012 **)
 (** Coq coding by choukh, April 2020 **)
 
-Require Export ZFC.ZFC0.
+Require Export ZFC.Axiom.ZFC0.
 
 (*** ZFC集合论1：配对，单集，二元并，集族的并 ***)
 
@@ -59,8 +59,7 @@ Qed.
 (* 配对是顺序无关的 *)
 Theorem pair_ordering_agnostic : ∀ a b, {a, b} = {b, a}.
 Proof.
-  intros. apply ExtAx.
-  split; intros.
+  intros. ext.
   - apply PairE in H.
     destruct H as [H1|H2].
     + subst x. apply PairI2.
@@ -183,7 +182,7 @@ Qed.
 Lemma character_of_single : ∀ A, ∀x ∈ A, (∀y ∈ A, x = y) → A = ⎨x⎬.
 Proof.
   intros A x Hx H.
-  apply ExtAx. split; intros.
+  ext.
   - apply H in H0. subst. apply SingI.
   - apply SingE in H0. subst. apply Hx.
 Qed.
@@ -228,7 +227,7 @@ Qed.
 (* 任意集合的单集的并就是原集合 *)
 Lemma union_single : ∀ A, ⋃ ⎨A⎬ = A.
 Proof.
-  intros. apply ExtAx. split; intros.
+  intros. ext.
   - apply UnionAx in H as [a [H1 H2]].
     apply SingE in H1. subst. apply H2.
   - eapply UnionI. apply SingI. apply H.
@@ -239,13 +238,13 @@ Lemma union_one : ⋃ 1 = ∅.
 Proof. exact (union_single ∅). Qed.
 
 (* 集合的并等于空集当且仅当该集合是零或壹 *)
-Lemma union_empty_iff : ∀ A, ⋃ A = ∅ ↔ A = ∅ ∨ A = 1.
+Lemma union_eq_empty : ∀ A, ⋃ A = ∅ ↔ A = ∅ ∨ A = 1.
 Proof with eauto.
   split; intros.
   - destruct (classic (A = ∅)). left...
     apply EmptyNE in H0 as [a Ha].
     destruct (classic (a = ∅)). {
-      right. apply ExtAx. intros b. split; intros Hb.
+      right. ext b Hb.
       - destruct (classic (b = ∅)).
         + rewrite H1. apply SingI.
         + exfalso. apply EmptyNE in H1 as [x Hx].
@@ -263,7 +262,7 @@ Qed.
 (* 贰的并是壹 *)
 Lemma union_two : ⋃ 2 = 1.
 Proof.
-  apply ExtAx. split; intro.
+  ext.
   - apply UnionAx in H as [a [H1 H2]].
     apply TwoE in H1 as [].
     + rewrite H in H2. exfalso0.
@@ -274,7 +273,7 @@ Qed.
 (* 零的幂集是壹 *)
 Lemma power_empty : 𝒫 ∅ = 1.
 Proof.
-  apply ExtAx. split; intros.
+  ext.
   - apply PowerAx in H. apply OneI2.
     apply sub_empty. apply H.
   - apply PowerAx. apply OneE in H.
@@ -284,7 +283,7 @@ Qed.
 (* 集合的单集的幂集 *)
 Lemma power_single : ∀ a, 𝒫 ⎨a⎬ = {∅, ⎨a⎬}.
 Proof.
-  intros. apply ExtAx. split; intros.
+  intros. ext.
   - apply PowerAx in H.
     apply subset_of_single in H as []; subst.
     apply PairI1. apply PairI2.
@@ -325,7 +324,7 @@ Qed.
 
 Lemma bunion_self : ∀ A, A ∪ A = A.
 Proof.
-  intros. apply ExtAx. split; intros Hx.
+  intros. ext Hx.
   - apply BUnionE in Hx as []; auto.
   - apply BUnionI1; auto.
 Qed.
@@ -358,7 +357,7 @@ Proof.
     apply H in H1.
     eapply member_of_member_of_two_is_zero. apply H2. apply H1.
   }
-  apply ExtAx. split; intros.
+  ext.
   - apply H1 in H2. subst. apply OneI1.
   - apply UnionAx. exists 1. split.
     + apply ReplAx in H0. apply H0. 
@@ -368,7 +367,7 @@ Qed.
 Fact funion_const : ∀ X F C,
   ⦿ X → (∀x ∈ X, F x = C) → ⋃{F x | x ∊ X} = C.
 Proof.
-  intros. apply ExtAx. split; intros.
+  intros. ext.
   - apply FUnionE in H1. destruct H1 as [y [H1 H2]].
     apply H0 in H1. subst. auto.
   - destruct H as [y H]. eapply FUnionI.
@@ -397,4 +396,11 @@ Proof.
     rewrite H2. apply TwoI1.
 Qed.
 
+Lemma repl_eq_1 : ∀ F A, {F x | x ∊ A} = 1 → ∀ x ∈ A, F x = ∅.
+Proof with eauto.
+  intros F A H x Hx. contra.
+  assert (F x ∈ 1). rewrite <- H. eapply ReplI...
+  apply SingE in H1...
+Qed.
+
 Close Scope ZFC1_scope.

ZFC2.v Axiom/ZFC2.v

@@ -2,7 +2,7 @@
 (** adapted from the thesis by Jonas Kaiser, November 23, 2012 **)
 (** Coq coding by choukh, April 2020 **)
 
-Require Export ZFC.ZFC1.
+Require Export ZFC.Axiom.ZFC1.
 
 (*** ZFC集合论2：集合建构式，任意交，二元交，有序对，笛卡尔积 ***)
 
@@ -71,7 +71,7 @@ Qed.
 Lemma sep_ext : ∀ A P Q,
   (∀x ∈ A, P x ↔ Q x) → {x ∊ A | P x} = {x ∊ A | Q x}.
 Proof with auto.
-  intros. apply ExtAx. split; intros Hx.
+  intros. ext Hx.
   - apply SepE in Hx as [Hx HP].
     apply SepI... apply H...
   - apply SepE in Hx as [Hx HQ].
@@ -174,7 +174,7 @@ Lemma disjoint_bunion_injective : ∀ A B C,
   A ∪ C = B ∪ C → A = B.
 Proof with auto.
   intros * Hdja Hdjb Heq.
-  apply ExtAx. split; intros Hx.
+  ext Hx.
   - assert (Hx': x ∈ A ∪ C) by (apply BUnionI1; auto).
     rewrite Heq in Hx'. apply BUnionE in Hx' as []...
     exfalso. apply (disjointE A C x)...
@@ -193,7 +193,7 @@ Definition π2 := λ p, ⋃ {x ∊ ⋃p | x ∈ ⋂p → ⋃p = ⋂p}.
 
 Lemma op_union : ∀ x y, ⋃<x, y> = {x, y}.
 Proof.
-  intros. apply ExtAx. intros a. split; intros.
+  intros. ext a H.
   - apply UnionAx in H.
     destruct H as [A [H1 H2]].
     apply PairE in H1. destruct H1.
@@ -207,7 +207,7 @@ Qed.
 
 Lemma op_inter : ∀ x y, ⋂<x, y> = ⎨x⎬.
 Proof.
-  intros. apply ExtAx. intros a. split; intros.
+  intros. ext a H.
   - apply InterE in H as [_ H].
     apply H. apply PairI1.
   - apply SingE in H. subst. apply InterI.
@@ -228,7 +228,7 @@ Proof.
   unfold π2. intros.
   rewrite op_union in *.
   rewrite op_inter in *.
-  apply ExtAx. intros a. split; intros.
+  ext a H.
   - apply UnionAx in H... destruct H as [A [H1 H2]].
     apply SepE in H1 as [H3 H4].
     apply PairE in H3. destruct H3.
@@ -332,7 +332,7 @@ Qed.
 
 Fact cprod_single_single : ∀ x, ⎨x⎬ × ⎨x⎬ = ⎨<x, x>⎬.
 Proof with auto.
-  intros. apply ExtAx. split; intros Hx.
+  intros. ext Hx.
   - apply CProdE1 in Hx as [a [Ha [b [Hb Hx]]]].
     apply SingE in Ha. apply SingE in Hb. subst...
   - apply SingE in Hx. subst. apply CProdI...
@@ -341,7 +341,7 @@ Qed.
 Fact cprod_alternative_definition : ∀ A B,
   A × B = ⋃ {{<a, b> | b ∊ B} | a ∊ A}.
 Proof with auto.
-  intros. apply ExtAx. split; intros Hx.
+  intros. ext Hx.
   - apply CProdE1 in Hx as [a [Ha [b [Hb Hx]]]]. subst x.
     apply UnionAx. exists {<a, b> | b ∊ B}. split.
     + apply ReplAx. exists a. split...

ZFC3.v Axiom/ZFC3.v

@@ -2,7 +2,7 @@
 (** adapted from the thesis by Jonas Kaiser, November 23, 2012 **)
 (** Coq coding by choukh, April 2020 **)
 
-Require Export ZFC.ZFC2.
+Require Export ZFC.Axiom.ZFC2.
 
 (*** ZFC集合论3：无穷公理，选择公理，正则公理 ***)
 

CoqMakefile

@@ -7,7 +7,7 @@
 ##         #     GNU Lesser General Public License Version 2.1          ##
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
-## GNUMakefile for Coq 8.13.1
+## GNUMakefile for Coq 8.13.2
 
 # For debugging purposes (must stay here, don't move below)
 INITIAL_VARS := $(.VARIABLES)
@@ -218,7 +218,7 @@ COQDOCLIBS?=$(COQLIBS_NOML)
 # The version of Coq being run and the version of coq_makefile that
 # generated this makefile
 COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
-COQMAKEFILE_VERSION:=8.13.1
+COQMAKEFILE_VERSION:=8.13.2
 
 COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)")
 

CoqMakefile.conf

@@ -8,7 +8,7 @@
 #                                                                             #
 ###############################################################################
 
-COQMF_VFILES = Meta.v ZFC0.v ZFC1.v ZFC2.v ZFC3.v lib/Essential.v lib/EpsilonInduction.v lib/EpsilonImpliesAC.v lib/Class.v EST2.v EX2.v EST3_1.v EST3_2.v EST3_3.v EX3_1.v EX3_2.v EST7_1.v lib/Relation.v lib/FuncFacts.v EST4_1.v EST4_2.v EST4_3.v EX4.v lib/Natural.v lib/NatIsomorphism.v lib/WosetMin.v EST5_1.v EST5_2.v EST5_3.v EST5_4.v EX5.v EST5_5.v EST5_6.v EST5_7.v lib/Real.v EST6_1.v lib/algebra/Inj_2n3m.v lib/IndexedFamilyUnion.v lib/Dominate.v lib/ChoiceFacts.v lib/Choice.v EST7_2.v EST7_3.v EST7_4.v EST7_5.v EST6_2.v EX6_1.v lib/NaturalFacts.v lib/OrdFacts.v EST6_3.v EST6_4.v EX6_2.v EST6_5.v EST6_6.v EX6_3.v lib/Cardinal.v EX7_1.v EX7_2.v lib/Ordinal.v lib/ZornsLemma.v EST7_6.v lib/ScottsTrick.v EX7_3.v lib/LoStruct.v lib/WoStructExtension.v EST8_1.v EST8_2.v EST8_3.v EST8_4.v EX8_1.v EX8_2.v EX8_3.v EX8_4.v EST8_5.v EST8_6.v EST8_7.v
+COQMF_VFILES = Axiom/Meta.v Axiom/ZFC0.v Axiom/ZFC1.v Axiom/ZFC2.v Axiom/ZFC3.v Lib/Essential.v Lib/EpsilonInduction.v Lib/EpsilonImpliesAC.v Lib/Class.v Theory/EST2.v Theory/EX2.v Theory/EST3_1.v Theory/EST3_2.v Theory/EST3_3.v Theory/EX3_1.v Theory/EX3_2.v Theory/EST7_1.v Lib/Relation.v Lib/FuncFacts.v Theory/EST4_1.v Theory/EST4_2.v Theory/EST4_3.v Theory/EX4.v Lib/Natural.v Lib/NatIsomorphism.v Lib/WosetMin.v Theory/EST5_1.v Theory/EST5_2.v Theory/EST5_3.v Theory/EST5_4.v Theory/EX5.v Theory/EST5_5.v Theory/EST5_6.v Theory/EST5_7.v Lib/Real.v Theory/EST6_1.v Lib/algebra/Inj_2n3m.v Lib/IndexedFamilyUnion.v Lib/Dominate.v Lib/ChoiceFacts.v Lib/Choice.v Theory/EST7_2.v Theory/EST7_3.v Theory/EST7_4.v Theory/EST7_5.v Theory/EST6_2.v Theory/EX6_1.v Lib/NaturalFacts.v Lib/OrdFacts.v Theory/EST6_3.v Theory/EST6_4.v Theory/EX6_2.v Theory/EST6_5.v Theory/EST6_6.v Theory/EX6_3.v Lib/Cardinal.v Theory/EX7_1.v Theory/EX7_2.v Lib/Ordinal.v Lib/ZornsLemma.v Theory/EST7_6.v Lib/ScottsTrick.v Theory/EX7_3.v Lib/LoStruct.v Lib/WoStructExtension.v Theory/EST8_1.v Theory/EST8_2.v Theory/EST8_3.v Theory/EST8_4.v Theory/EX8_1.v Theory/EX8_2.v Theory/EX8_3.v Theory/EX8_4.v Theory/EST8_5.v Theory/EST8_6.v Theory/EST8_7.v
 COQMF_MLIFILES = 
 COQMF_MLFILES = 
 COQMF_MLGFILES = 
@@ -36,7 +36,7 @@ COQMF_CMDLINE_COQLIBS =
 
 COQMF_LOCAL=0
 COQMF_COQLIB=/usr/local/lib/coq/
-COQMF_DOCDIR=/usr/local/Cellar/coq/8.13.1/share/doc/coq/
+COQMF_DOCDIR=/usr/local/Cellar/coq/8.13.2/share/doc/coq/
 COQMF_OCAMLFIND=/usr/local/opt/ocaml-findlib/bin/ocamlfind
 COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67   -safe-string -strict-sequence
 COQMF_WARN=-warn-error +a-3