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.