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.