Library hilbert.Enumeration
Set Implicit Arguments.
Require Import Coq.Sets.Image.
Require Import PartialFun.
Require Import Epsilon.
Require Import Classical_sets.
Implicit Arguments In [U].
Section Definitions.
Variable D : Type.
Inductive segment_bound : Set :=
all_nats : segment_bound
| less_than : nat -> segment_bound.
Definition nat_segment (b : segment_bound) : Ensemble nat :=
match b with all_nats => (fun i => True)
| less_than p => (fun i=> i < p)
end.
Inductive enumerates (b : segment_bound)
(X : Ensemble D)(Rf:nat -> D -> Prop)
:Prop :=
enumerates_i :
rel_bijection (nat_segment b) X Rf ->
enumerates b X Rf.
Lemma empty_enumeration :
enumerates (less_than 0) (Empty_set _) (fun i d => True) .
Proof.
split;auto.
split.
red.
simpl;inversion 1.
red.
inversion 1.
red.
inversion 1.
red.
contradiction.
red.
inversion 2.
Qed.
Inductive denumerable (X : Ensemble D ) : Prop :=
denumerable_intro : forall b Rf, enumerates b X Rf -> denumerable X.
Lemma denumerable_empty : denumerable (Empty_set D).
Proof.
esplit.
eexact empty_enumeration.
Qed.
Lemma denumerable_add_disj : forall (X : Ensemble D )
a , denumerable X ->
~ (In X a) ->
denumerable (Add _ X a).
Proof.
intros X a H;case H.
intro b; case b;intros.
exists all_nats (fun n x => match n with 0 => x=a | S p => Rf p x end).
split.
split.
simpl.
red;intros.
case H0.
case a0; intros.
exists a;auto.
case H3.
intros.
red in H4.
apply H4.
simpl;auto.
red;intro a0;case a0;intros.
subst a;red.
right;auto.
unfold In. split;auto.
left.
case H0;intros.
case H4;intros.
red in H6.
apply H6 with n.
simpl;auto.
auto.
red.
intro a0;case a0;intros.
subst a;auto.
case H0;intros.
case H5;intros.
red in H8;eapply H8.
2:eauto.
simpl;auto.
auto.
red.
intros.
case H0; intros.
case H3;intros.
red in H7.
case H2.
intros.
case (H7 _ H9).
intros.
exists (S x0).
simpl;auto.
destruct 1.
exists 0;simpl;auto.
split;auto.
red;auto.
case H0;intros.
case H2;intros.
red.
intros a0 a' ;case a0; case a'.
auto.
intros.
subst b0.
red in H4.
case H1.
eapply H4.
2:eauto.
simpl;auto.
intros.
subst b0.
red in H4.
case H1.
eapply H4.
2:eauto.
simpl;auto.
intros.
replace n0 with n.
auto.
red in H7.
eapply H7;eauto.
exists (less_than (S n)) (fun n x => match n with 0 => x=a | S p => Rf p x end).
split.
split.
simpl.
red.
intro a0; case a0.
exists a;auto.
intros.
red in H2.
case H0.
intros.
case H3;intros.
red in H4.
apply H4.
simpl;red;auto with arith.
red;intro a0;case a0;intros.
subst a;red.
right;auto.
unfold In. split;auto.
left.
case H0;intros.
case H4;intros.
red in H6.
apply H6 with n0.
simpl;red;auto.
simpl in H2; red in H2.
auto with arith.
auto.
red.
intro a0;case a0;intros.
subst a;auto.
case H0;intros.
case H5;intros.
red in H8;eapply H8.
2:eauto.
simpl;auto.
simpl in H2; red in H2.
red;auto with arith.
auto.
red.
intros.
case H0; intros.
case H3;intros.
red in H7.
case H2.
intros.
case (H7 _ H9).
intros.
exists (S x0).
simpl;auto.
case H10;split;auto.
red.
simpl in H11; red in H11.
auto with arith.
destruct 1.
exists 0;simpl;auto.
split;auto.
red;auto.
auto with arith.
red.
case H0.
destruct 1.
intros a0 a' ;case a0; case a'.
auto.
intros.
subst b0.
red in H3.
case H1.
eapply H3.
2:eauto.
simpl;auto.
red.
simpl in H8; red in H8.
auto with arith.
intros.
subst b0.
red in H3.
case H1.
eapply H3.
2:eauto.
simpl;red;auto.
simpl in H7;auto with arith.
intros.
replace n1 with n0.
auto.
red in H6.
eapply H6;eauto.
simpl;red; simpl in H9; auto with arith.
simpl;red; simpl in H10; auto with arith.
Qed.
Definition seq_range (f : nat -> D) :=
fun x => exists n:nat, f n = x.
Definition seq_range_opt (f : nat -> optionT D) :=
fun x => exists n:nat, f n = SomeT x.
Lemma seq_range_enumeration : forall f, injective _ _ f ->
enumerates all_nats (seq_range f) (fun i x => f i = x).
split.
simpl.
split;red;intros.
exists (f a);auto.
exists a; auto.
subst b;auto.
case H0.
intros x ;exists x;split;auto.
split.
apply H.
subst b;auto.
Qed.
End Definitions.
Lemma denumerable_bij_rel : forall (A B : Type)
(Da : Ensemble A)(Db : Ensemble B)
(g : A -> B -> Prop),
denumerable Da ->
rel_bijection Da Db g ->
denumerable Db.
Proof.
intros.
case H;intros;clear H.
case H0;intros.
exists b (fun n y => exists x, In (nat_segment b) n /\ Rf n x /\ g x y).
split.
case H1;auto.
case H1;intros.
case H7;intros.
split;red;intros.
case (H8 a);auto.
intros.
case (H x);auto.
red in H9.
eapply H9;eauto.
intros.
exists x0.
exists x.
auto.
case H14; intros.
decompose [and] H15.
clear H15.
red in H2.
eapply H2;eauto.
case H14;intros x (H1x,(H2x,H3x)).
case H15;intros y (H1y,(H2y,H3y)).
clear H14 H15.
red in H3. eapply H3;eauto.
replace b0 with b'.
auto.
eapply H3;eauto.
replace y with x;auto.
red in H10;eapply H10;eauto.
case (H4 b0 H13).
intros x (Hx,H'x).
case (H11 x Hx);intros n (Hn,H'n).
exists n;split;auto.
exists x;split;auto.
case H15;intros x (Hx,(H1x,H2x)).
case H16;intros y (Hy,(H1y,H2y)).
assert (x=y).
eapply H5;eauto.
subst y.
eapply H12;eauto.
Qed.
Lemma denumerable_bij_fun : forall (A B : Type)
(Da : Ensemble A)(Db : Ensemble B)
(g : A -> B),
denumerable Da ->
fun_bijection Da Db g ->
denumerable Db.
Proof.
intros.
apply denumerable_bij_rel with (Da:=Da)(Db:=Db)(g:=fun a b => In Da a /\ In Db b /\ b= g a).
auto.
eapply bijection_fun_rel with g;auto.
split.
intuition.
intuition.
case H0;intros.
red in H3.
subst b;eapply H3;eauto.
Qed.
Lemma denumerable_bij_funR : forall (A B : Type)
(Da : Ensemble A)(Db : Ensemble B)
(g : A -> B),
denumerable Db ->
fun_bijection Da Db g ->
denumerable Da.
Admitted.
Lemma denumerable_inj : forall (A B : Type)
(Da : Ensemble A)(Db : Ensemble B)
(g : A -> B -> Prop),
denumerable Db ->
rel_domain Da g ->
rel_codomain Da Db g ->
rel_functional Da g ->
rel_inj Da g ->
denumerable Da.
Proof.
destruct 1;intros.
Admitted.
Lemma denumerable_incl : forall (A : Type)
(Da Db: Ensemble A),
(Included _ Da Db) ->
denumerable Db ->
denumerable Da.
Proof.
intros.
eapply denumerable_inj with A Db (fun a b : A => a = b);auto.
red;intros.
exists a; auto.
red;intros.
subst b;auto.
red;intros.
subst a;auto.
red;intros.
subst b;auto.
Qed.
Lemma denumerable_add : forall (D:Type)(X : Ensemble D )
a , denumerable X ->
denumerable (Add _ X a).
Proof.
intros.
case (classic (In X a)).
intro;rewrite Non_disjoint_union;auto.
intro; apply denumerable_add_disj;auto.
Qed.