Library Coq.Reals.Runcountable

Require Import Coq.Reals.Rdefinitions.
Require Import Coq.Reals.Raxioms.
Require Import Rfunctions.
Require Import Coq.Reals.RIneq.
Require Import Coq.Logic.FinFun.
Require Import Coq.Logic.ConstructiveEpsilon.

Definition enumeration (A : Type) (u : nat -> A) (v : A -> nat) : Prop :=
  (forall x : A, u (v x) = x) /\ (forall n : nat, v (u n) = n).

Definition in_holed_interval (a b hole : R) (u : nat -> R) (n : nat) : Prop :=
  Rlt a (u n) /\ Rlt (u n) b /\ u n <> hole.

Lemma in_holed_interval_dec (a b h : R) (u : nat -> R) (n : nat)
  : {in_holed_interval a b h u n} + {~in_holed_interval a b h u n}.

Definition point_in_holed_interval (a b h : R) : R :=
  if Req_EM_T h (Rdiv (Rplus a b) (INR 2)) then (Rdiv (Rplus a h) (INR 2))
  else (Rdiv (Rplus a b) (INR 2)).

Lemma middle_in_interval : forall a b : R, Rlt a b -> (a < (a + b) / INR 2 < b)%R.

Lemma point_in_holed_interval_works (a b h : R) :
  Rlt a b -> let p := point_in_holed_interval a b h in
             Rlt a p /\ Rlt p b /\ p <> h.

Definition first_in_holed_interval (u : nat -> R) (v : R -> nat) (a b h : R)
  : enumeration R u v -> Rlt a b
    -> { n : nat | in_holed_interval a b h u n
                /\ forall k : nat, in_holed_interval a b h u k -> n <= k }.

Lemma first_in_holed_interval_works (u : nat -> R) (v : R -> nat) (a b h : R)
  (pen : enumeration R u v) (plow : Rlt a b) :
  let (c,_) := first_in_holed_interval u v a b h pen plow in
  forall x:R, Rlt a x -> Rlt x b -> x <> h -> x <> u c -> c < v x.

Definition first_two_in_interval (u : nat -> R) (v : R -> nat) (a b : R)
           (pen : enumeration R u v) (plow : Rlt a b)
  : prod R R :=
  let (first_index, pr) := first_in_holed_interval u v a b b pen plow in
  let (second_index, pr2) := first_in_holed_interval u v a b (u first_index) pen plow in
  if Rle_dec (u first_index) (u second_index) then (u first_index, u second_index)
  else (u second_index, u first_index).

Lemma split_couple_eq : forall {a b c d : R}, (a,b) = (c,d) -> a = c /\ b = d.

Lemma first_two_in_interval_works (u : nat -> R) (v : R -> nat) (a b : R)
  (pen : enumeration R u v) (plow : Rlt a b) :
  let (c,d) := first_two_in_interval u v a b pen plow in
  Rlt a c /\ Rlt c b
  /\ Rlt a d /\ Rlt d b
  /\ Rlt c d
  /\ (forall x:R, Rlt a x -> Rlt x b -> x <> c -> x <> d -> v c < v x).

Definition tearing_sequences (u : nat -> R) (v : R -> nat)
  : (enumeration R u v) -> nat -> { ab : prod R R | Rlt (fst ab) (snd ab) }.

Lemma tearing_sequences_projsig (u : nat -> R) (v : R -> nat) (en : enumeration R u v)
      (n : nat)
  : let (I,pr) := tearing_sequences u v en n in
    proj1_sig (tearing_sequences u v en (S n))
    = first_two_in_interval u v (fst I) (snd I) en pr.

Lemma tearing_sequences_inc_dec (u : nat -> R) (v : R -> nat) (pen : enumeration R u v)
  : forall n : nat,
    let I := proj1_sig (tearing_sequences u v pen n) in
    let SI := proj1_sig (tearing_sequences u v pen (S n)) in
    Rlt (fst I) (fst SI) /\ Rlt (snd SI) (snd I).

Lemma split_lt_succ : forall n m : nat, lt n (S m) -> lt n m \/ n = m.

Lemma increase_seq_transit (u : nat -> R) :
  (forall n : nat, Rlt (u n) (u (S n))) -> (forall n m : nat, n < m -> Rlt (u n) (u m)).

Lemma decrease_seq_transit (u : nat -> R) :
  (forall n : nat, Rlt (u (S n)) (u n)) -> (forall n m : nat, n < m -> Rlt (u m) (u n)).

Lemma tearing_sequences_ordered_forall (u : nat -> R) (v : R -> nat)
      (pen : enumeration R u v) :
  forall n m : nat, let In := proj1_sig (tearing_sequences u v pen n) in
             let Im := proj1_sig (tearing_sequences u v pen m) in
             Rlt (fst In) (snd Im).

Definition tearing_elem_fst (u : nat -> R) (v : R -> nat) (pen : enumeration R u v) (x : R)
  := exists n : nat, x = fst (proj1_sig (tearing_sequences u v pen n)).

Definition torn_number (u : nat -> R) (v : R -> nat) (pen : enumeration R u v) :
  {m : R | is_lub (tearing_elem_fst u v pen) m}.

Lemma torn_number_above_first_sequence (u : nat -> R) (v : R -> nat) (en : enumeration R u v)
  : forall n : nat, Rlt (fst (proj1_sig (tearing_sequences u v en n)))
                 (proj1_sig (torn_number u v en)).

Lemma torn_number_below_second_sequence (u : nat -> R) (v : R -> nat)
      (en : enumeration R u v) :
  forall n : nat, Rlt (proj1_sig (torn_number u v en))
               (snd (proj1_sig (tearing_sequences u v en n))).

Lemma limit_index_above_all_indices (u : nat -> R) (v : R -> nat) (en : enumeration R u v) :
  forall n : nat, v (fst (proj1_sig (tearing_sequences u v en (S n))))
           < v (proj1_sig (torn_number u v en)).

Lemma first_indices_increasing (u : nat -> R) (v : R -> nat) (H : enumeration R u v)
  : forall n : nat, n <> 0 -> v (fst (proj1_sig (tearing_sequences u v H n)))
                     < v (fst (proj1_sig (tearing_sequences u v H (S n)))).

Theorem R_uncountable : forall u : nat -> R, ~Bijective u.