# 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, k < n -> ~in_holed_interval a b h u 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.