Library denumerable.Denumerable
A formalization of denumerable sets.
Require Import Ensembles.
Require Import Even.
Require Import Div2.
Add LoadPath "../hilbert".
Require Import PartialFun.
Require Import GRelations.
Require Import Arith_lemmas.
Set Implicit Arguments.
Implicit Arguments rel_injection.
Implicit Arguments rel_surjection.
Section Denumerable.
Section Definitions.
Variable U : Type.
Variable A : Ensemble U.
Let Dnat : Ensemble nat := Full_set nat.
Predicate for relations which number the elements of A.
These relations map each element of A to at least one integer, but they are not required to be functional (injectivity is only needed to ensure that A is denumerable).
These relations map each element of A to at least one integer, but they are not required to be functional (injectivity is only needed to ensure that A is denumerable).
Definition rel_numbers (R: GRelation U nat) := rel_injection A Dnat R.
Predicate for relations which enumerate A.
Definition rel_enumerates (R : GRelation nat U) := rel_surjection Dnat A R.
A is denumerable when there exists an injection from
A
to Full_set nat
.
Definition denumerable : Prop := exists R, rel_numbers R.
Section Equivalence_with_surjection.
Theorem denumerable_surj :
denumerable <-> exists R, rel_enumerates R.
Proof.
split.
unfold denumerable; intro denum.
destruct denum as (R, R_enum).
exists (rel_inv A Dnat R).
red; apply R_inv_surj.
assumption.
intro ex_surj.
elim ex_surj; intros R R_surj.
exists (rel_inv Dnat A R).
red.
apply R_inv_inj.
assumption.
Qed.
End Equivalence_with_surjection.
End Definitions.
Variable U : Type.
Union _ A B
is denumerable if A
and B
are denumerable.
Section Denumerable_union.
Section Denumerable_union_lemmas.
Variables E F : Ensemble U.
Variables RE RF : U -> nat -> Prop.
Hypothesis RE_enum : rel_numbers E RE.
Hypothesis RF_enum : rel_numbers F RF.
Inductive R_union (x : U) : nat -> Prop :=
from_E : forall n : nat, In E x -> RE x n -> R_union x (double n)
| from_F : forall n : nat, In F x -> RF x n -> R_union x (S (double n)).
Lemma R_union_domain : rel_domain (Union U E F) R_union.
Proof.
intros a aInUnion.
induction aInUnion.
red in RE_enum; destruct RE_enum as (Hdomain, _, _).
red in Hdomain.
destruct (Hdomain x).
assumption.
exists (double x0).
apply from_E; assumption.
red in RF_enum; destruct RF_enum as (Hdomain, _ , _).
red in Hdomain.
destruct (Hdomain x).
assumption.
exists (S (double x0)).
apply from_F; assumption.
Qed.
Lemma R_union_codomain : rel_codomain (Union U E F) (Full_set nat) R_union.
Proof.
split.
Qed.
Remark R_union_double:
forall (x : U) (n : nat), R_union x (double n) -> RE x n.
Proof.
intros x n R_x_2n.
inversion R_x_2n.
replace n with n0.
assumption.
apply double_inj.
assumption.
case (not_double_is_s_double _ _ H).
Qed.
Remark R_union_S_double :
forall (x : U) (n : nat), R_union x (S (double n)) -> RF x n.
Proof.
intros x n R_x_s2n.
inversion R_x_s2n.
symmetry in H.
case (not_double_is_s_double _ _ H).
replace n with n0.
assumption.
apply double_inj.
assumption.
Qed.
Lemma R_union_inj : rel_inj (Union U E F) R_union.
Proof.
intros a a' b a_In_Union a'_In_Union a_R_b a'_R_b.
inversion a_R_b as [na a_In_E a_RE_na dna_b | na a_In_F a_RF_na sdna_b].
inversion a'_R_b as [na' a'_In_E a'_RE_na' dna'_b | na' a'_In_F a'_RF_na' sdna'_b].
destruct RE_enum as (_, _, RE_inj).
apply RE_inj with na'; try assumption.
replace na' with na; try assumption.
apply double_inj.
symmetry in dna'_b; transitivity b; assumption.
rewrite <- dna_b in sdna'_b.
case not_double_is_s_double with na' na; assumption.
inversion a'_R_b as [na' a'_In_E a'_RE_na' dna'_b | na' a'_In_F a'_RF_nb sdna'_b].
rewrite <- sdna_b in dna'_b.
symmetry in dna'_b.
case not_double_is_s_double with na na'; assumption.
destruct RF_enum as (_, _, RF_inj).
apply RF_inj with na'; try assumption.
replace na' with na; try assumption.
apply double_inj.
symmetry in sdna'_b.
rewrite <- sdna_b in sdna'_b.
injection sdna'_b; trivial.
Qed.
Lemma R_union_enumerates : rel_numbers (Union U E F) R_union.
Proof.
split.
apply R_union_domain.
apply R_union_codomain.
apply R_union_inj.
Qed.
End Denumerable_union_lemmas.
Theorem denumerable_union (E : Ensemble U) (F : Ensemble U) :
denumerable E -> denumerable F -> denumerable (Union U E F).
Proof.
intros E F E_den F_den.
destruct E_den as (RE, RE_enum).
destruct F_den as (RF, RF_enum).
exists (R_union E F RE RF).
apply R_union_enumerates; assumption.
Qed.
End Denumerable_union.
Section Denumerable_inclusion.
Variables E F : Ensemble U.
Section Denumerable_inclusion_lemmas.
Variable RE : U -> nat -> Prop.
Hypothesis RE_enum : rel_numbers E RE.
Hypothesis F_in_E : Included _ F E.
Lemma R_inclusion_domain : rel_domain F RE.
Proof.
intros a a_In_F.
destruct RE_enum as (RE_domain, _, _).
apply RE_domain.
apply F_in_E.
assumption.
Qed.
Lemma R_inclusion_codomain : rel_codomain F (Full_set nat) RE.
Proof.
split.
Qed.
Lemma R_inclusion_inj : rel_inj F RE.
Proof.
intros a a' b a_In_F a'_In_F a_R_B a_'R_b.
destruct RE_enum as (_, _, RE_inj).
apply (RE_inj a a' b); try apply F_in_E; assumption.
Qed.
Lemma R_inclusion_enumerates : rel_numbers F RE.
Proof.
split.
apply R_inclusion_domain.
apply R_inclusion_codomain.
apply R_inclusion_inj.
Qed.
End Denumerable_inclusion_lemmas.
Theorem denumerable_inclusion :
denumerable E -> Included _ F E -> denumerable F.
Proof.
intros E_denum F_in_E.
destruct E_denum as (RE, RE_enum).
exists RE.
apply R_inclusion_enumerates; assumption.
Qed.
End Denumerable_inclusion.
Section Infinite_union.
Variable A : Ensemble (Ensemble U).
Definition Infinite_union (x : U) : Prop :=
exists b, In A b /\ In b x.
Section Infinite_union_lemmas.
Variable R : Ensemble U -> nat -> Prop.
Variable R_n : nat -> U -> nat -> Prop.
Hypothesis R_enums : rel_numbers A R.
Hypothesis R_n_enums :
forall n : nat, forall b : Ensemble U,
In A b -> R b n -> rel_numbers b (R_n n).
Fixpoint laboureur (n : nat) : nat * nat :=
match n with
0 => (0, 0)
| S n => match laboureur n with
(0, m) => (S m, 0)
|(S n, m) => (n, S m)
end
end.
Let laboureur_1 : nat * nat -> nat := fun couple =>
let (p, q) := couple in
div2 ((p+q+1)*(p+q)) + q.
Let lab_rel (p1 : nat*nat) (p2 : nat*nat) : Prop :=
let (p, q) := p1 in let (p', q') := p2 in
(p + q < p' + q') \/ (p + q = p' + q' /\ p' < p).
Require Import Arith.
Require Import Wellfounded.
Require Import Relations.
Require Import Wf_nat.
Let f : nat * nat -> sigT (fun _ : nat => nat) := fun cpl =>
let (p, q) := cpl in existT (fun _ : nat => nat) (p + q) q.
Let R_lab := (fun x y => (lexprod _ (fun _ => nat) lt (fun _ => lt)) (f x) (f y)).
Lemma lexof_wf :
well_founded R_lab.
Proof.
unfold R_lab.
apply wf_inverse_image with (R := lexprod _ (fun _ => nat) lt (fun _ => lt)).
apply wf_lexprod; intros; apply lt_wf.
Qed.
Lemma lab_rel_wf :
well_founded lab_rel.
Proof.
apply wf_incl with R_lab.
intros (p, q) (p', q') Hlab_rel.
case Hlab_rel.
intros Hin.
unfold R_lab; unfold f; apply left_lex; assumption.
intros (Hdiag, Hin).
unfold R_lab; unfold f; rewrite Hdiag; apply right_lex.
case (le_lt_dec q' q).
intros Hqin.
case (lt_irrefl (p + q)).
pattern (p + q) at 1; rewrite Hdiag.
apply plus_lt_le_compat; assumption.
trivial.
apply lexof_wf.
Qed.
Require Import ArithRing.
Remark double_lab_1 :
forall p q, double (laboureur_1 (p, q)) = ((p+q+1)*(p+q)) + double q.
Proof.
intros p q.
unfold laboureur_1.
rewrite (double_plus (div2 ((p + q + 1) * (p + q)))).
rewrite <- (even_double ((p + q + 1) * (p + q))).
trivial.
apply even_prod.
Qed.
Lemma lab_bij :
forall p q, laboureur (laboureur_1 (p, q)) = (p, q).
intros p q.
generalize (p, q).
intros p0; pattern p0; apply (well_founded_ind lab_rel_wf).
clear p q p0.
intros (p, q) IH.
induction q.
induction p.
compute; trivial.
replace (laboureur_1 (S p, 0)) with (S (laboureur_1 (0, p))).
unfold laboureur.
fold laboureur.
replace (laboureur (laboureur_1 (0, p))) with (0, p).
trivial.
symmetry; apply IH.
left; auto with arith.
apply double_inj.
rewrite (double_S (laboureur_1 (0, p))).
rewrite (double_lab_1 0 p).
rewrite (double_lab_1 (S p) 0).
rewrite <- (plus_n_O (S p)).
rewrite (plus_O_n p).
unfold double.
rewrite (plus_O_n 0); rewrite <- (plus_n_O ((S p + 1) * S p)).
replace (S p) with (p + 1).
rewrite (plus_2 ((p + 1) * p + (p + p))).
ring.
omega.
replace (laboureur_1 (p, S q)) with (S (laboureur_1 (S p, q))).
unfold laboureur; fold laboureur.
replace (laboureur (laboureur_1 (S p, q))) with (S p, q).
trivial.
symmetry; apply IH.
right; split; omega.
apply double_inj.
rewrite (double_S (laboureur_1 (S p, q))).
rewrite (double_lab_1 (S p) q).
rewrite (double_lab_1 p (S q)).
rewrite (plus_2 ((S p + q + 1) * (S p + q) + double q)).
replace (S q) with (q + 1).
replace (S p) with (p + 1).
unfold double.
ring.
omega. omega.
Qed.
Definition R_union_qcq (x : U) (n : nat) :=
match laboureur n with
(p, q) => exists b, (In A b /\ R b p) /\ (In b x /\ R_n p x q)
end.
Lemma R_union_qcq_domain :
rel_domain Infinite_union R_union_qcq.
Proof.
intros a a_In_Union.
elim a_In_Union.
intros b (b_In_A, a_In_b).
cut (exists p, R b p).
intros ex_p; elim ex_p; intros p b_R_p.
cut (exists q, R_n p a q).
intros ex_q; elim ex_q; intros q a_Rn_q.
exists (laboureur_1 (p, q)).
red.
replace (laboureur (laboureur_1 (p, q))) with (p, q).
exists b.
repeat split; assumption.
symmetry; apply lab_bij.
destruct (R_n_enums b_In_A b_R_p) as (R_n_domain, _, _).
apply R_n_domain.
assumption.
destruct R_enums as (R_domain, _, _).
apply R_domain.
assumption.
Qed.
Lemma R_union_qcq_codomain :
rel_codomain Infinite_union (Full_set nat) R_union_qcq.
Proof.
split.
Qed.
Lemma R_union_qcq_inj :
rel_inj Infinite_union R_union_qcq.
Proof.
intros a a' n a_In_Union a'_In_Union a_Ru_n a'_Ru_n.
red in a_Ru_n; generalize a_Ru_n; case_eq (laboureur n).
intros p q lab_eq ex_b.
red in a'_Ru_n; generalize a'_Ru_n; case_eq (laboureur n).
intros p' q' lab'_eq.
assert (p_eq : p = p').
transitivity (fst (laboureur n));
[rewrite lab_eq | rewrite lab'_eq]; compute; trivial.
assert (q_eq : q = q').
transitivity (snd (laboureur n));
[rewrite lab_eq | rewrite lab'_eq]; compute; trivial.
rewrite <- p_eq; rewrite <- q_eq.
intro ex_b'.
elim ex_b; intros b ((b_In_A, b_R_p), (b'_In_A, a_Rnp_q)).
elim ex_b'; intros b' H.
assert (b_eq : b = b').
destruct H as (H0, H1); destruct H0; destruct H1.
destruct R_enums as (_, _, R_inj).
apply R_inj with p; assumption.
rewrite <- b_eq in H.
destruct H as ((_, _), (a'_In_b, a'_Rnp_q)).
destruct (R_n_enums b_In_A b_R_p) as (_, _, Rn_inj).
apply Rn_inj with q; assumption.
Qed.
Lemma R_union_qcq_numbers :
rel_numbers Infinite_union R_union_qcq.
Proof.
split.
apply R_union_qcq_domain.
apply R_union_qcq_codomain.
apply R_union_qcq_inj.
Qed.
End Infinite_union_lemmas.
Section Indexed_union_lemmas_2.
Variable R : GRelation (Ensemble U) nat.
Hypothesis R_enum : rel_numbers A R.
Hypothesis all_b_denum : forall b : Ensemble U, In A b -> denumerable b.
Require Import Epsilon.
Let b_n (n : nat) :=
epsilon (Empty_set U) (fun b => In A b /\ R b n).
Remark bn_R_n :
forall n, (exists b, In A b /\ R b n) -> R (b_n n) n.
Proof.
intros n ex_b.
pattern (b_n n); hilbert_e.
intros a (_, a_R_n); assumption.
Qed.
Let R_b (b : Ensemble U) :=
epsilon (fun _ _ => True) (fun R => rel_numbers b R).
Remark Rb_numbers_b :
forall b, In A b -> rel_numbers b (R_b b).
Proof.
intros b b_In_A.
pattern (R_b b); hilbert_e.
apply all_b_denum.
assumption.
Qed.
Let R_n (n : nat) (x : U) (m : nat) :=
(exists b, R b n) /\ R_b (b_n n) x m.
Remark Rn_numbers_bn :
forall n : nat, In A (b_n n) -> R (b_n n) n -> rel_numbers (b_n n) (R_n n).
Proof.
intros n bn_In_A.
split.
intros x x_In_b.
destruct (Rb_numbers_b bn_In_A) as (Rb_dom, _, _).
elim (Rb_dom x); try assumption.
intros m x_Rb_m.
exists m.
split; [exists (b_n n) | idtac]; assumption.
split.
intros x x' m x_In_bn x'_In_bn (ex_b, x_Rb_m) (_, x'_Rb_m).
destruct (Rb_numbers_b bn_In_A) as (_, _, Rb_inj).
apply Rb_inj with m; assumption.
Qed.
Let b_p (b : Ensemble U) :=
epsilon 0 (fun p => b = b_n p).
Remark R4 :
forall b : Ensemble U, In A b -> b = b_n (b_p b).
Proof.
intros b b_In_A.
pattern (b_p b); hilbert_e.
destruct R_enum as (R_dom, _, R_inj).
elim (R_dom b b_In_A).
intros p b_R_p.
exists p.
pattern (b_n p); hilbert_e.
exists b; split; assumption.
intros a (a_In_A, a_R_p).
apply R_inj with p; assumption.
Qed.
Lemma all_b_relation :
exists R_n : nat -> U -> nat -> Prop,
forall n : nat, forall b : Ensemble U, In A b -> R b n -> rel_numbers b (R_n n).
Proof.
exists R_n.
intros n b b_In_A b_R_n.
assert (b = b_n n).
pattern (b_n n); hilbert_e.
exists b; split; assumption.
destruct R_enum as (_, _, R_inj).
intros a (a_In_A, a_R_p).
apply R_inj with n; assumption.
rewrite H; rewrite H in b_In_A; rewrite H in b_R_n.
apply Rn_numbers_bn; assumption.
Qed.
End Indexed_union_lemmas_2.
Theorem denumerable_union_qcq :
denumerable A ->
(forall b : Ensemble U, In A b -> denumerable b) -> denumerable Infinite_union.
Proof.
intros A_denum all_b_denum.
elim A_denum; intros R R_enum.
elim all_b_relation with R; try assumption.
intros R_n R_n_enum.
exists (R_union_qcq R R_n).
apply R_union_qcq_numbers; assumption.
Qed.
End Infinite_union.
Section Denumerable_empty.
Lemma denumerable_empty :
denumerable (Empty_set U).
Proof.
pose (R := fun (_ : U) (_ : nat) => False).
exists R.
split.
intros x.
destruct 1.
split.
intros x x' n x_In_empty.
case x_In_empty.
Qed.
End Denumerable_empty.
Section Denumerable_singleton.
Variable x : U.
Lemma denumerable_singleton :
denumerable (Singleton _ x).
Proof.
pose (R := fun (y : U) (n : nat) => y = x).
exists R.
split.
intros y y_In_s.
exists 0.
inversion y_In_s.
rewrite <- H; unfold R; reflexivity.
split.
intros y y' n y_In_s y'_In_s _ _.
inversion y_In_s.
inversion y'_In_s.
subst y; auto.
Qed.
End Denumerable_singleton.
Section seq_range.
Definition seq_range (f : nat -> U) :=
fun x => exists n : nat, f n = x.
Require Import Coq.Sets.Image.
Lemma seq_range_denumerable :
forall f, denumerable (seq_range f).
Proof.
intros f.
pose (R := fun (x : U) (n : nat) => f n = x).
exists R.
split.
intros x.
destruct 1.
exists x0.
unfold R. assumption.
split.
intros x x' n x_In_sr x'_In_sr x_R_n x'_R_n.
unfold R in x_R_n.
unfold R in x'_R_n.
subst x; auto.
Qed.
End seq_range.
Section denumerable_bijection.
Variable V : Type.
Variable A : Ensemble U.
Variable B : Ensemble V.
Variable g : U -> V.
Hypothesis g_bij : fun_bijection A B g.
Lemma denumerable_bij_fun :
denumerable A -> denumerable B.
Proof.
intro A_denum.
red in A_denum.
elim A_denum; intros Ru Ru_num.
pose (Rv := fun (y : V) (n : nat) => exists x : U, In A x /\ g x = y /\ Ru x n).
exists Rv.
split.
intros y y_In_B.
destruct Ru_num as (Ru_dom, _, _).
unfold Rv.
destruct g_bij as (_, g_onto, _).
elim g_onto with y; try assumption.
intros x (x_In_A, gx_eq_y).
elim Ru_dom with x; try assumption.
intros b x_Ru_b.
exists b; exists x; repeat split; assumption.
split.
intros y y' n y_In_B y'_In_B y_Rv_n y'_Rv_n.
unfold Rv in y_Rv_n; unfold Rv in y'_Rv_n.
elim y_Rv_n; intros x (x_In_A, (gx_eq_y, x_Ru_n)).
elim y'_Rv_n; intros x' (x'_In_A, (gx'_eq_y', x'_Ru_n)).
assert (x_eq : x = x').
destruct Ru_num as (_, _, Ru_inj).
apply Ru_inj with n; assumption.
rewrite <- gx_eq_y; rewrite x_eq; assumption.
Qed.
Lemma denumerable_bij_funR :
denumerable B -> denumerable A.
Proof.
intro B_denum.
elim B_denum; intros Rv Rv_num.
pose (Ru := fun (x : U) (n : nat) => Rv (g x) n).
exists Ru.
split.
intros x x_In_A.
unfold Ru.
destruct Rv_num.
apply H.
destruct g_bij.
apply H2; assumption.
split.
intros x x' n x_In_A x'_In_A x_Ru_n x'_Ru_n.
unfold Ru in x_Ru_n. unfold Ru in x'_Ru_n.
destruct Rv_num.
destruct g_bij; auto.
apply H4; auto.
apply H1 with n; auto.
Qed.
End denumerable_bijection.
Section Finite_is_denumerable.
Require Import Finite_sets.
Variable A : Ensemble U.
Hypothesis A_finite : Finite _ A.
Theorem denumerable_finite : denumerable A.
Proof.
elim A_finite.
apply denumerable_empty.
intros A0 A0_finite A0_denum x x_nIn_A0.
unfold Add.
apply denumerable_union.
assumption.
apply denumerable_singleton.
Qed.
End Finite_is_denumerable.
End Denumerable.