Library Stdlib.Reals.Runcountable

From Stdlib.Reals Require Import Rdefinitions.
From Stdlib.Reals Require Import Raxioms.
From Stdlib Require Import Rfunctions.
From Stdlib.Reals Require Import RIneq.
From Stdlib Require Import FinFun.
From Stdlib.Logic Require Import 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_dec_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.