Sierpinski.Sierpinski
Require Export Sierpinski.Hartogs.
Require Import Coq.Logic.Classical.
Require Import Coq.Program.Program.
Require Import Coq.Init.Nat.
Definition Infinite (A : S) :=
Numeral <= A.
Definition Generalized_Continuum_Hypothesis :=
forall x y : S,
Infinite x ->
x <= y <= 𝒫 x ->
x ∼ y \/ y ∼ 𝒫 x.
Definition Well_Ordering_Theorem :=
forall x : S, inhabited (Strict_Well_Order_On x).
Definition Axiom_Of_Choice :=
forall A B : S, forall R : A -> B -> Prop,
(forall x, exists y, R x y) ->
exists f : A -> B, forall x : A, R x (f x).
Definition Axiom_Of_Choice' :=
forall (I : S) (F : I -> S),
(forall i, inhabited (F i)) ->
inhabited (forall i, F i).
Lemma AC_equiv :
Axiom_Of_Choice <-> Axiom_Of_Choice'.
Proof.
unfold Axiom_Of_Choice, Axiom_Of_Choice'.
split; intros AC.
- intros I F H. pose (R (i : I) (A : ⋃ i ∈ I, F i) := A ∈ F i).
destruct (AC _ _ R) as [f Hf].
+ intros i. destruct (H i) as [A]. unshelve eexists.
* exists A. apply in_indexed_union_iff. exists i. apply A.
* unfold R. apply A.
+ refine (inhabits (fun i => _)). exists (f i). apply Hf.
- intros A B R existence.
assert (inhabitation : forall x : A, inhabited `{ y in B | R x y }). {
intros x. destruct (existence x) as [y Hy].
apply inhabits. exists y. apply in_comprehension_iff_typed. exact Hy.
}
destruct (AC _ _ inhabitation) as [f].
exists (fun x : A => element (f x)).
intros x. apply comprehension_condition.
Qed.
Definition Axiom_Of_Choice'' :=
forall (A : S),
(forall x : A, inhabited x) ->
exists f : A -> big_union A,
forall x, f x ∈ x.
Lemma AC_equiv' :
Axiom_Of_Choice <-> Axiom_Of_Choice''.
Proof.
rewrite AC_equiv.
unfold Axiom_Of_Choice', Axiom_Of_Choice''. split.
- intros ac A H.
specialize (ac A id H). cbn in ac. destruct ac as [f].
assert (forall x : A, f x ∈ big_union A). {
setoid_rewrite in_big_union_iff. intros x. exists x. exact _.
}
exists (fun x : A => element (f x)).
exact _.
- intros ac I F H. specialize (ac `{F i | i in I}).
assert (H' : forall x : `{ F i | i in I }, inhabited x). {
intros [x Hx]. cbn. apply in_fun_replacement_iff in Hx.
destruct Hx as [i ->]. apply H.
}
specialize (ac H'). destruct ac as [f Hf]. apply inhabits. intros i.
assert (F i ∈ `{ F i | i in I }). {
apply in_fun_replacement_iff. exists i. reflexivity.
}
exact (element (f (element (F i)))).
Qed.
Lemma Well_Ordering_to_Choice' :
Well_Ordering_Theorem -> Axiom_Of_Choice'.
Proof.
intros well_ordering I F H.
destruct (well_ordering (⋃ i ∈ I, F i)) as [R].
assert (forall i, F i ∈ 𝒫 (⋃ i ∈ I, F i)) by automation.
exact (inhabits (fun i => least_element (element (F i)) (H i))).
Qed.
Lemma Well_Ordering_to_Choice :
Well_Ordering_Theorem -> Axiom_Of_Choice.
Proof. rewrite AC_equiv. exact Well_Ordering_to_Choice'. Qed.
Lemma lemma1 (A B : S) :
A ⊔ A ∼ A ->
A ⊔ B ∼ 𝒫 A ->
𝒫 A <= B.
Proof.
intros H1 H2.
assert (f : A ⊔ B ∼ 𝒫 A × 𝒫 A). {
transitivity (𝒫 A). {
exact H2.
}
transitivity (𝒫 (A ⊔ A)). {
rewrite H1. reflexivity.
}
rewrite power_set_of_disjoint_union. reflexivity.
} destruct f as [f].
clear H1 H2.
assert (H : exists A1 : 𝒫 A, forall A2 : 𝒫 A, Is_From_Right (f⁻¹ `(A1, A2))). {
set (g := π1 ∘ f ∘ inj1 _ _ : A -> 𝒫 A).
assert (H : ~ surjective g). {
intros H. apply (cantors_theorem A).
exact (inhabits (build_surjection g H)).
}
change (~ forall A1, exists a, A1 = g a) in H.
apply not_all_ex_not in H. destruct H as [A1 H]. exists A1.
intros A2.
enough (~ Is_From_Left (f⁻¹ `(A1, A2))). {
destruct (from_left_or_right (f⁻¹ `(A1, A2))); tauto.
}
unfold Is_From_Left. unfold g in H; cbn in g.
intros [a contra]. apply H. exists a.
unfold compose. rewrite <- contra.
rewrite cancel_inverse_right. rewrite left_projection_beta.
reflexivity.
}
destruct H as [A1 H].
unshelve eset (g (A2 : 𝒫 A) := extract_from_right (f⁻¹ `(A1, A2)) : B). {
apply H.
}
simple refine (inhabits (build_injection g _)).
intros A2 A2' H1. unfold g in H1.
apply extract_from_right_is_injective in H1.
apply bijection_is_injective in H1.
apply pair_is_injective_right in H1.
exact H1.
Qed.
Lemma lemma2 (x y : S) :
Generalized_Continuum_Hypothesis ->
Infinite x ->
x ⊔ x ∼ x ->
𝒫 x ⊔ 𝒫 x ∼ 𝒫 x ->
y <= 𝒫 x ->
y <= x \/ 𝒫 x <= y.
Proof.
intros gch. intros H1 H2 H3 H4.
assert (x <= x ⊔ y <= 𝒫 x). {
split.
- apply disjoint_union_is_increasing_on_left.
- rewrite (power_set_is_increasing x) at 1.
rewrite H4. rewrite H3. reflexivity.
}
assert (cases : x ∼ x ⊔ y \/
x ⊔ y ∼ 𝒫 x). {
apply gch; assumption.
} destruct cases as [-> | H5].
- left. apply disjoint_union_is_increasing_on_right.
- right. apply lemma1.
+ assumption.
+ rewrite H5. reflexivity.
Qed.
Theorem sierpinskis_theorem :
Generalized_Continuum_Hypothesis -> Axiom_Of_Choice.
Proof.
intros gch. apply Well_Ordering_to_Choice. intros x.
enough (H : exists α : O, x <= α). {
destruct H as [α [f]].
apply inhabits.
apply (transport_strict_well_order (injection_as_bijection_into_image f)⁻¹).
unshelve refine (restrict_well_order (strict_well_order_on_ordinal α)
(image_of f)).
automation.
}
set (x0 := x ⊔ Numeral).
set (x' n := iter (1 + n) 𝒫 x0).
exists (hartogs_number (x' 0)).
transitivity (x' 0). {
cbn. unfold x0.
rewrite <- power_set_is_increasing.
rewrite <- disjoint_union_is_increasing_on_left.
reflexivity.
}
assert (H1 : forall n, x' n ⊔ x' n ∼ x' n). {
intros n. change (x' n) with (𝒫 (iter n 𝒫 x0)).
symmetry. apply power_set_equiv_power_set_plus_power_set.
induction n.
- cbn. unfold x0. apply disjoint_union_is_increasing_on_right.
- change (iter (Datatypes.S n) 𝒫 x0) with (𝒫 (iter n 𝒫 x0)).
rewrite power_set_is_increasing at 1. rewrite IHn at 1. reflexivity.
}
assert (H2 : (hartogs_number (x' 0) : S) <= x' 6) by
apply hartogs_number_has_upper_bound.
revert H2. generalize 6. intros n H2. induction n.
- apply hartogs_number_is_not_smaller in H2. contradiction.
- assert (cases : (hartogs_number (x' 0) : S) <= x' n \/
x' (1 + n) <= hartogs_number (x' 0)). {
apply lemma2; auto.
- unfold Infinite. clear. induction n.
+ cbn. unfold x0. rewrite <- power_set_is_increasing.
apply disjoint_union_is_increasing_on_right.
+ change (Numeral <= 𝒫 (x' n)).
rewrite IHn. apply power_set_is_increasing.
- apply H1.
} destruct cases as [ | <-].
+ apply IHn. assumption.
+ unfold x'. generalize (1 + n) x0; clear. intros n x0; induction n.
* reflexivity.
* rewrite IHn. rewrite power_set_is_increasing. reflexivity.
Qed.
Require Import Coq.Logic.Classical.
Require Import Coq.Program.Program.
Require Import Coq.Init.Nat.
Definition Infinite (A : S) :=
Numeral <= A.
Definition Generalized_Continuum_Hypothesis :=
forall x y : S,
Infinite x ->
x <= y <= 𝒫 x ->
x ∼ y \/ y ∼ 𝒫 x.
Definition Well_Ordering_Theorem :=
forall x : S, inhabited (Strict_Well_Order_On x).
Definition Axiom_Of_Choice :=
forall A B : S, forall R : A -> B -> Prop,
(forall x, exists y, R x y) ->
exists f : A -> B, forall x : A, R x (f x).
Definition Axiom_Of_Choice' :=
forall (I : S) (F : I -> S),
(forall i, inhabited (F i)) ->
inhabited (forall i, F i).
Lemma AC_equiv :
Axiom_Of_Choice <-> Axiom_Of_Choice'.
Proof.
unfold Axiom_Of_Choice, Axiom_Of_Choice'.
split; intros AC.
- intros I F H. pose (R (i : I) (A : ⋃ i ∈ I, F i) := A ∈ F i).
destruct (AC _ _ R) as [f Hf].
+ intros i. destruct (H i) as [A]. unshelve eexists.
* exists A. apply in_indexed_union_iff. exists i. apply A.
* unfold R. apply A.
+ refine (inhabits (fun i => _)). exists (f i). apply Hf.
- intros A B R existence.
assert (inhabitation : forall x : A, inhabited `{ y in B | R x y }). {
intros x. destruct (existence x) as [y Hy].
apply inhabits. exists y. apply in_comprehension_iff_typed. exact Hy.
}
destruct (AC _ _ inhabitation) as [f].
exists (fun x : A => element (f x)).
intros x. apply comprehension_condition.
Qed.
Definition Axiom_Of_Choice'' :=
forall (A : S),
(forall x : A, inhabited x) ->
exists f : A -> big_union A,
forall x, f x ∈ x.
Lemma AC_equiv' :
Axiom_Of_Choice <-> Axiom_Of_Choice''.
Proof.
rewrite AC_equiv.
unfold Axiom_Of_Choice', Axiom_Of_Choice''. split.
- intros ac A H.
specialize (ac A id H). cbn in ac. destruct ac as [f].
assert (forall x : A, f x ∈ big_union A). {
setoid_rewrite in_big_union_iff. intros x. exists x. exact _.
}
exists (fun x : A => element (f x)).
exact _.
- intros ac I F H. specialize (ac `{F i | i in I}).
assert (H' : forall x : `{ F i | i in I }, inhabited x). {
intros [x Hx]. cbn. apply in_fun_replacement_iff in Hx.
destruct Hx as [i ->]. apply H.
}
specialize (ac H'). destruct ac as [f Hf]. apply inhabits. intros i.
assert (F i ∈ `{ F i | i in I }). {
apply in_fun_replacement_iff. exists i. reflexivity.
}
exact (element (f (element (F i)))).
Qed.
Lemma Well_Ordering_to_Choice' :
Well_Ordering_Theorem -> Axiom_Of_Choice'.
Proof.
intros well_ordering I F H.
destruct (well_ordering (⋃ i ∈ I, F i)) as [R].
assert (forall i, F i ∈ 𝒫 (⋃ i ∈ I, F i)) by automation.
exact (inhabits (fun i => least_element (element (F i)) (H i))).
Qed.
Lemma Well_Ordering_to_Choice :
Well_Ordering_Theorem -> Axiom_Of_Choice.
Proof. rewrite AC_equiv. exact Well_Ordering_to_Choice'. Qed.
Lemma lemma1 (A B : S) :
A ⊔ A ∼ A ->
A ⊔ B ∼ 𝒫 A ->
𝒫 A <= B.
Proof.
intros H1 H2.
assert (f : A ⊔ B ∼ 𝒫 A × 𝒫 A). {
transitivity (𝒫 A). {
exact H2.
}
transitivity (𝒫 (A ⊔ A)). {
rewrite H1. reflexivity.
}
rewrite power_set_of_disjoint_union. reflexivity.
} destruct f as [f].
clear H1 H2.
assert (H : exists A1 : 𝒫 A, forall A2 : 𝒫 A, Is_From_Right (f⁻¹ `(A1, A2))). {
set (g := π1 ∘ f ∘ inj1 _ _ : A -> 𝒫 A).
assert (H : ~ surjective g). {
intros H. apply (cantors_theorem A).
exact (inhabits (build_surjection g H)).
}
change (~ forall A1, exists a, A1 = g a) in H.
apply not_all_ex_not in H. destruct H as [A1 H]. exists A1.
intros A2.
enough (~ Is_From_Left (f⁻¹ `(A1, A2))). {
destruct (from_left_or_right (f⁻¹ `(A1, A2))); tauto.
}
unfold Is_From_Left. unfold g in H; cbn in g.
intros [a contra]. apply H. exists a.
unfold compose. rewrite <- contra.
rewrite cancel_inverse_right. rewrite left_projection_beta.
reflexivity.
}
destruct H as [A1 H].
unshelve eset (g (A2 : 𝒫 A) := extract_from_right (f⁻¹ `(A1, A2)) : B). {
apply H.
}
simple refine (inhabits (build_injection g _)).
intros A2 A2' H1. unfold g in H1.
apply extract_from_right_is_injective in H1.
apply bijection_is_injective in H1.
apply pair_is_injective_right in H1.
exact H1.
Qed.
Lemma lemma2 (x y : S) :
Generalized_Continuum_Hypothesis ->
Infinite x ->
x ⊔ x ∼ x ->
𝒫 x ⊔ 𝒫 x ∼ 𝒫 x ->
y <= 𝒫 x ->
y <= x \/ 𝒫 x <= y.
Proof.
intros gch. intros H1 H2 H3 H4.
assert (x <= x ⊔ y <= 𝒫 x). {
split.
- apply disjoint_union_is_increasing_on_left.
- rewrite (power_set_is_increasing x) at 1.
rewrite H4. rewrite H3. reflexivity.
}
assert (cases : x ∼ x ⊔ y \/
x ⊔ y ∼ 𝒫 x). {
apply gch; assumption.
} destruct cases as [-> | H5].
- left. apply disjoint_union_is_increasing_on_right.
- right. apply lemma1.
+ assumption.
+ rewrite H5. reflexivity.
Qed.
Theorem sierpinskis_theorem :
Generalized_Continuum_Hypothesis -> Axiom_Of_Choice.
Proof.
intros gch. apply Well_Ordering_to_Choice. intros x.
enough (H : exists α : O, x <= α). {
destruct H as [α [f]].
apply inhabits.
apply (transport_strict_well_order (injection_as_bijection_into_image f)⁻¹).
unshelve refine (restrict_well_order (strict_well_order_on_ordinal α)
(image_of f)).
automation.
}
set (x0 := x ⊔ Numeral).
set (x' n := iter (1 + n) 𝒫 x0).
exists (hartogs_number (x' 0)).
transitivity (x' 0). {
cbn. unfold x0.
rewrite <- power_set_is_increasing.
rewrite <- disjoint_union_is_increasing_on_left.
reflexivity.
}
assert (H1 : forall n, x' n ⊔ x' n ∼ x' n). {
intros n. change (x' n) with (𝒫 (iter n 𝒫 x0)).
symmetry. apply power_set_equiv_power_set_plus_power_set.
induction n.
- cbn. unfold x0. apply disjoint_union_is_increasing_on_right.
- change (iter (Datatypes.S n) 𝒫 x0) with (𝒫 (iter n 𝒫 x0)).
rewrite power_set_is_increasing at 1. rewrite IHn at 1. reflexivity.
}
assert (H2 : (hartogs_number (x' 0) : S) <= x' 6) by
apply hartogs_number_has_upper_bound.
revert H2. generalize 6. intros n H2. induction n.
- apply hartogs_number_is_not_smaller in H2. contradiction.
- assert (cases : (hartogs_number (x' 0) : S) <= x' n \/
x' (1 + n) <= hartogs_number (x' 0)). {
apply lemma2; auto.
- unfold Infinite. clear. induction n.
+ cbn. unfold x0. rewrite <- power_set_is_increasing.
apply disjoint_union_is_increasing_on_right.
+ change (Numeral <= 𝒫 (x' n)).
rewrite IHn. apply power_set_is_increasing.
- apply H1.
} destruct cases as [ | <-].
+ apply IHn. assumption.
+ unfold x'. generalize (1 + n) x0; clear. intros n x0; induction n.
* reflexivity.
* rewrite IHn. rewrite power_set_is_increasing. reflexivity.
Qed.