Skip to content

Instantly share code, notes, and snippets.

@davidad
Created August 13, 2020 01:58
Show Gist options
  • Save davidad/98decc5b23a7fe10eb35c8f970bcac25 to your computer and use it in GitHub Desktop.
Save davidad/98decc5b23a7fe10eb35c8f970bcac25 to your computer and use it in GitHub Desktop.
There is exactly one way to choose 0 elements from the empty set.
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment