davidad · August 13, 2020 01:58 · Aug 13, 2020
diff --git a/0_0_1.v b/0_0_1.v
@@ -0,0 +1,94 @@
+Parameter set : Set.
+Parameter In : (set * set) -> Prop.
+
+Definition subset (A B : set) : Prop :=
+  forall x : set, In(x,A) -> In(x,B).
+
+Axiom ZF_extensionality :
+  forall X Y : set,
+    (forall z : set, In(z,X) <-> In(z,Y))
+    -> X = Y.
+
+Axiom ZF_specification :
+  forall (P: set -> Prop), forall X : set,
+  sig (fun (S : set) =>
+    forall z : set,
+    In(z,S) <-> (In(z,X) /\ P(z)) ).
+
+Axiom ZF_powerset :
+  forall X : set,
+  sig (fun (Y : set) =>
+    forall Z : set,
+    subset Z X -> In(Z,Y) ).
+
+Axiom ZF_pairing :
+  forall X Y : set,
+  sig (fun (Z : set) =>
+    In(X,Z) /\ In(Y,Z) ).
+
+Axiom ZF_emptyset :
+  sig (fun (X : set) =>
+    forall y : set,
+    not(In(y,X)) ).
+
+Lemma proper_powerset : 
+  forall X : set,
+  sig (fun (Y : set) =>
+    forall Z : set,
+    subset Z X <-> In(Z,Y) ).
+Proof.
+  intros.
+  destruct (ZF_powerset X) as [px].
+  destruct (ZF_specification (fun z => subset z X) px) as [ppx].
+  firstorder.
+Qed.
+
+Definition subsets_of : set -> set := fun X =>
+  proj1_sig (proper_powerset X).
+
+Definition specified (P : set -> Prop) (X : set) : set :=
+  proj1_sig (ZF_specification P X).
+
+Definition Empty : set := proj1_sig ZF_emptyset.
+Definition Zero : set := Empty.
+
+Lemma one : sig (fun (One : set) => forall z : set, In(z, One) <-> z = Zero).
+Proof.
+  destruct (ZF_pairing Zero Zero) as [pzz].
+  destruct (ZF_specification (fun z => z = Zero) pzz) as [one].
+  exists one.
+  firstorder.
+  rewrite H1.
+  firstorder.
+Qed.
+
+Definition One : set := proj1_sig one.
+
+Ltac use_properties_of X x :=
+  unfold X in *;
+  let S := fresh "S" in pose proof (proj2_sig x); remember (proj1_sig x) as S eqn:Seq; clear Seq.
+
+Theorem exactly_one_zero_subset_of_empty_set : (specified (fun s => s = Zero) (subsets_of Empty)) = One.
+Proof.
+  apply ZF_extensionality.
+  intuition.
+  all: use_properties_of One one;
+       use_properties_of specified (ZF_specification (fun s => s = Zero) (subsets_of Empty));
+       unfold Zero in *;
+       use_properties_of Empty ZF_emptyset;
+       use_properties_of subsets_of (proper_powerset S0).
+  { apply H0.
+    apply ZF_extensionality.
+    pose proof (H1 z).
+    intuition;
+    rewrite <- H7 in *;
+    trivial. }
+  { assert (zZ : z = S1) by firstorder.
+    rewrite zZ.
+    apply H1.
+    intuition.
+    apply (proj2_sig (proper_powerset S1)).
+    unfold subset; trivial. }
+Qed.
+
+Check exactly_one_zero_subset_of_empty_set.
No results found