Why are the real numbers axiomatized in Coq?

I was wondering whether Coq defined the real numbers as Cauchy sequences or Dedekind cuts, so I checked Coq.Reals.Raxioms and... none of these two. The real numbers are axiomatized, along with their operations (as Parameters and Axioms). Why is it so?

Parameter

Axiom

Also, the real numbers tightly rely on the notion of subset, since one of their defining properties is that is every upper bounded subset has a least upper bound. The Axiom completeness encodes those subsets as Props.

Axiom completeness

Prop

I have the impression that these Props only form the definable subsets of the reals. So does Coq only have access to definable real numbers? What exactly is this Coq's R? Analytical numbers? Algebraic numbers? Arithmetical numbers?

Prop

R

If, as I suspect, Coq only has a countable subset of the reals (because there are only countably many Props), that makes an infinitesimal part of the reals. Is it fit for theories that deeply exploit the structure of the ZFC real numbers, such as fractals, chaos theory or the Lebesgue measure?

Prop

EDIT

Here is a naive construction of the reals by Dedekind cuts.

Require Import Coq.QArith.QArith_base.

(* An interval of rationals, unbounded below, bounded above.
Its upper limit is the definition of a real number. *)
Definition DedekindCut (part : Q -> Prop) : Prop :=
(forall x y : Q, x < y / part(y) -> part(x))
/ (exists q : Q, forall x : Q, part(x) -> x < q).

(* Square root of 2 *)
Definition sqrt_2 (x : Q) : Prop := x*x < 2#1 / x < 0.

Lemma square_increasing : forall x y : Q, 0 <= x -> 0 <= y -> x <= y -> x*x <= y*y.
Proof.
intros x y H H0 H1. apply (Qle_trans (x*x) (y*x) (y*y)).
apply (Qmult_le_compat_r x y x); assumption. rewrite -> (Qmult_comm y x).
apply (Qmult_le_compat_r x y y); assumption.
Qed.

Lemma sqrt_increasing : forall x y : Q, 0 <= x -> 0 <= y -> x*x < y*y -> x < y.
Proof.
intros x y H H0 H1. destruct (Q_dec y x) as [[eq|eq0]|eq1].
- exfalso. apply Qlt_le_weak in eq. apply square_increasing in eq. apply Qle_not_lt in eq.
contradiction. assumption. assumption.
- assumption.
- exfalso. rewrite -> eq1 in H1. apply Qlt_irrefl in H1. contradiction.
Qed.

Lemma sqrt_2_is_dc : DedekindCut sqrt_2.
Proof.
split.
- intros x y [H H0]. destruct (Qlt_le_dec y 0). right.
apply (Qlt_trans x y 0); assumption. destruct (Qlt_le_dec x 0). right. assumption.
left. destruct H0. apply (Qle_lt_trans (x*x) (y*y) (2#1)).
apply square_increasing. assumption. assumption. apply Qlt_le_weak. assumption.
assumption. exfalso. apply Qle_not_lt in q. contradiction.
- exists (2#1). intros. destruct (Qlt_le_dec x 0). apply (Qlt_trans x 0 (2#1)). assumption.
reflexivity. destruct H. apply (Qlt_trans (x*x) (2#1) ((2#1) * (2#1))) in H.
apply sqrt_increasing. assumption. discriminate. assumption. split. apply (Qlt_trans x 0 (2#1)).
assumption. reflexivity.
Qed.

(* The order on Dedekind cuts : any point of the lower one is a limit
of the higher one. *)
Definition DCleq (l h : Q -> Prop) : Prop :=
DedekindCut(l) / DedekindCut(h)
/ (forall x eta : Q, l x -> exists y : Q, h y / y < x / x - y < eta).

(* The equality on Dedekind cuts : anti-symmetry of the order *)
Definition DCeq (d e : Q -> Prop) : Prop :=
DedekindCut(d) / DedekindCut(e) / DCleq d e / DCleq e d.

(* The addition of Dedekind cuts *)
Definition dc_add (x y : Q -> Prop) (a : Q) : Prop :=
exists u v : Q, x u / y v / a <= u + v.


EDIT

And here is a proof in Coq that R is uncountable. I don't really know what to think of it, since Props are obviously countable from outside Coq. This is probably a manifestation of Skolem's paradox, as Arthur Azevedo De Amorim suggests. The way I would put it is that the bijection between R and nat cannot be written in Coq. Maybe for similar reasons to the impossibility of writing a Coq interpreter in Coq.

R

Prop

R

nat

Require Import Coq.Reals.Rdefinitions.
Require Import Coq.Reals.Raxioms.
Require Import Rfunctions.
Require Import Coq.Reals.RIneq.

(* Well-order for decidable nat -> Prop. They have minimums. *)

Fixpoint smallest_prop_elem (P : nat -> Prop) (fuel start : nat)
(dec : forall k : nat, P k + ~P k) : nat :=
match fuel with
| O => start
| S fuel' => if dec start then start else smallest_prop_elem P fuel' (S start) dec
end.

Lemma below_smallest_not :
forall (P : nat -> Prop) (fuel n l : nat) (dec : forall k : nat, P k + ~P k),
l <= n -> n < smallest_prop_elem P fuel l dec -> ~P n.
Proof.
induction fuel.
- intros n l dec H H0 H1. simpl in H0. apply le_not_lt in H. contradiction.
- intros n l dec H H0. simpl in H0. destruct (dec l).
+ exfalso. apply le_not_lt in H. contradiction.
+ apply le_lt_or_eq in H. destruct H. apply (IHfuel n (S l) dec). assumption.
assumption. subst. assumption.
Qed.

Lemma smallest_below_fuel :
forall (P : nat -> Prop) (fuel l : nat) (dec : forall k : nat, P k + ~P k),
smallest_prop_elem P fuel l dec <= fuel + l.
Proof.
induction fuel.
- intros. reflexivity.
- intros. simpl. destruct (dec l). assert (forall k : nat, l <= S (k + l)).
induction k. simpl. apply le_S. apply le_n. apply (le_trans l (S (k+l)) (S (S k + l))).
apply IHk. apply le_n_S. simpl. apply le_S. apply le_n.
apply H. specialize (IHfuel (S l) dec). rewrite -> Nat.add_succ_r in IHfuel. assumption.
Qed.

Lemma smallest_found :
forall (P : nat -> Prop) (dec : forall k : nat, P k + ~P k) (fuel l : nat),
smallest_prop_elem P fuel l dec < fuel+l -> P (smallest_prop_elem P fuel l dec).
Proof.
induction fuel.
- intros. simpl in H. apply lt_irrefl in H. contradiction.
- intros. simpl. simpl in H. destruct (dec l). assumption. apply IHfuel.
rewrite -> Nat.add_succ_r. assumption.
Qed.

(* Tired to search in the library... *)
Lemma le_or_lt : forall m n : nat, n <= m -> n < m / n = m.
Proof.
induction m.
- intros. inversion H. right. reflexivity.
- intros. destruct n. left. apply le_n_S. apply le_0_n. apply le_pred in H. simpl in H.
destruct (IHm n H). left. apply le_n_S. assumption. subst. right. reflexivity.
Qed.

Lemma smallest_sat (P : nat -> Prop) (n : nat) (dec : forall k : nat, P k + ~P k) :
P n -> P (smallest_prop_elem P n 0 dec).
Proof.
intros. pose proof (smallest_below_fuel P n 0 dec). rewrite -> Nat.add_0_r in H0.
apply le_or_lt in H0 as [H0|H1]. apply (smallest_found P). rewrite -> Nat.add_0_r. assumption.
rewrite -> H1. assumption.
Qed.



(* Now the proof that R is uncountable. *)

(* We define the enumerations of the real numbers, to prove that they don't exist. *)
Definition R_enum (u : nat -> R) (v : R -> nat) : Prop :=
(forall x : R, u (v x) = x) / (forall n : nat, v (u n) = n).

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

(* Here we use axiom total_order_T *)
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.
Proof.
destruct (total_order_T a (u n)) as [[l|e]|hi].
- destruct (total_order_T b (u n)) as [[lb|eb]|hb].
+ right. intro H. destruct H. destruct H0. apply Rlt_asym in H0. contradiction.
+ subst. right. intro H. destruct H. destruct H0.
pose proof (Rlt_asym (u n) (u n) H0). contradiction.
+ destruct (Req_EM_T h (u n)). subst. right. intro H. destruct H. destruct H0.
exact (H1 eq_refl). left. split. assumption. split. assumption. intro H. subst.
exact (n0 eq_refl).
- subst. right. intro H. destruct H. pose proof (Rlt_asym (u n) (u n) H). contradiction.
- right. intro H. destruct H. apply Rlt_asym in H. contradiction.
Qed.

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.
Proof.
intros.
assert (twoNotZero: INR 2 <> 0%R).
apply not_0_INR. intro abs. inversion abs.
assert (twoAboveZero : (0 < / INR 2)%R).
apply Rinv_0_lt_compat. apply lt_0_INR. apply le_n_S. apply le_S. apply le_n.
assert (double : forall x : R, Rplus x x = ((INR 2) * x)%R).
intro x. rewrite -> S_O_plus_INR. rewrite -> Rmult_plus_distr_r.
rewrite -> Rmult_1_l. reflexivity.
split.
- assert (a + a < a + b)%R. apply (Rplus_lt_compat_l a a b). assumption.
rewrite -> double in H0. apply (Rmult_lt_compat_l (/ (INR 2))) in H0.
rewrite <- Rmult_assoc in H0. rewrite -> Rinv_l in H0. simpl in H0.
rewrite -> Rmult_1_l in H0. rewrite -> Rmult_comm in H0. assumption.
assumption. assumption.
- assert (b + a < b + b)%R. apply (Rplus_lt_compat_l b a b). assumption.
rewrite -> Rplus_comm in H0. rewrite -> double in H0.
apply (Rmult_lt_compat_l (/ (INR 2))) in H0.
rewrite <- Rmult_assoc in H0. rewrite -> Rinv_l in H0. simpl in H0.
rewrite -> Rmult_1_l in H0. rewrite -> Rmult_comm in H0. assumption.
assumption. assumption.
Qed.

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.
Proof.
intros. unfold point_in_holed_interval in p.
pose proof (middle_in_interval a b H). destruct H0.
destruct (Req_EM_T h ((a + b) / INR 2)).
- (* middle hole, p is quarter *) subst.
pose proof (middle_in_interval a ((a + b) / INR 2) H0). destruct H2.
split. assumption. split. apply (Rlt_trans p ((a + b) / INR 2)%R). assumption.
assumption. apply Rlt_not_eq. assumption.
- split. assumption. split. assumption. intro abs. subst. contradiction.
Qed.

(* An enumeration of R reaches any open interval of R,
extract the first two real numbers in it. *)
Definition first_in_holed_interval (u : nat -> R) (v : R -> nat) (a b h : R) : nat :=
smallest_prop_elem (in_holed_interval a b h u)
(v (point_in_holed_interval a b h))
0 (in_holed_interval_dec a b h u).

Lemma first_in_holed_interval_works (u : nat -> R) (v : R -> nat) (a b h : R) :
R_enum u v -> Rlt a b ->
let c := first_in_holed_interval u v a b h in
in_holed_interval a b h u c
/ forall x:R, Rlt a x -> Rlt x b -> x <> h -> x <> u c -> c < v x.
Proof.
intros. split.
- apply (smallest_sat (in_holed_interval a b h u)
(v (point_in_holed_interval a b h))
(in_holed_interval_dec a b h u)).
unfold in_holed_interval. destruct H. rewrite -> H.
apply point_in_holed_interval_works. assumption.
- intros. destruct (c ?= v x) eqn:order.
+ exfalso. apply Nat.compare_eq_iff in order. rewrite -> order in H4.
destruct H. rewrite -> H in H4. exact (H4 eq_refl).
+ apply Nat.compare_lt_iff in order. assumption.
+ exfalso. apply Nat.compare_gt_iff in order.
unfold first_in_holed_interval in c.
pose proof (below_smallest_not (in_holed_interval a b h u)
(v (point_in_holed_interval a b h))
(v x)
0 (in_holed_interval_dec a b h u)
(le_0_n (v x)) order).
destruct H. assert (in_holed_interval a b h u (v x)).
split. rewrite -> H. assumption. rewrite -> H. split; assumption.
contradiction.
Qed.

Lemma split_couple_eq : forall a b c d : R, (a,b) = (c,d) -> a = c / b = d.
Proof.
intros. injection H. intros. split. subst. reflexivity. subst. reflexivity.
Qed.

Definition first_two_in_interval (u : nat -> R) (v : R -> nat) (a b : R) : prod R R :=
let first_index : nat := first_in_holed_interval u v a b b in
let second_index := first_in_holed_interval u v a b (u first_index) 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 first_two_in_interval_works (u : nat -> R) (v : R -> nat) (a b : R)
: R_enum u v -> Rlt a b
-> let (c,d) := first_two_in_interval u v a b 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).
Proof.
intros. destruct (first_two_in_interval u v a b) eqn:ft.
unfold first_two_in_interval in ft.
destruct (Rle_dec (u (first_in_holed_interval u v a b b))
(u (first_in_holed_interval u v a b
(u (first_in_holed_interval u v a b b))))).
- apply split_couple_eq in ft as [ft ft0]. rewrite -> ft in r1.
pose proof (first_in_holed_interval_works u v a b b H H0). destruct H1.
destruct H1. rewrite -> ft in H1. rewrite -> ft in H3. split. apply H1.
destruct H3. split. apply H3. rewrite -> ft in ft0.
pose proof (first_in_holed_interval_works u v a b r H H0). destruct H5.
destruct H5. rewrite -> ft0 in H5. split. assumption. rewrite -> ft0 in H7.
destruct H7. split. assumption. rewrite -> ft0 in r1. destruct r1. split.
assumption. intros. assert (first_in_holed_interval u v a b b = v r).
rewrite <- ft. destruct H. rewrite -> H14. reflexivity.
rewrite <- H14. apply H2. assumption. assumption. intro abs. subst.
apply Rlt_irrefl in H11. contradiction. rewrite -> ft. assumption.
exfalso. rewrite -> H9 in H8. exact (H8 eq_refl).
- (* ugly copy paste *)
apply split_couple_eq in ft as [ft ft0]. apply Rnot_le_lt in n.
rewrite -> ft in n. rewrite -> ft0 in ft.
pose proof (first_in_holed_interval_works u v a b b H H0). destruct H1.
destruct H1. rewrite -> ft0 in H1. rewrite -> ft0 in H3.
pose proof (first_in_holed_interval_works u v a b r0 H H0). destruct H4.
destruct H4. rewrite -> ft in H4. rewrite -> ft in H6.
split. assumption. destruct H6. split. assumption. split. assumption.
destruct H3. split. assumption. rewrite -> ft0 in n. split. assumption.
intros. assert (first_in_holed_interval u v a b r0 = v r).
rewrite <- ft. destruct H. rewrite -> H13. reflexivity.
rewrite <- H13. apply H5. assumption. assumption. intro abs. rewrite -> abs in H12.
exact (H12 eq_refl). rewrite -> ft. assumption.
Qed.

(* If u,v is an enumeration of R, these sequences tear the segment [0,1].
The first sequence is increasing, the second decreasing. The first is below the second.
Therefore the first sequence has a limit, a least upper bound b, that u cannot reach,
which contradicts u (v b) = b. *)
Fixpoint tearing_sequences (u : nat -> R) (v : R -> nat) (n : nat) : prod R R :=
match n with
| 0 => (INR 0, INR 1)
| S p => let (a,b) := tearing_sequences u v p in
first_two_in_interval u v a b
end.

Lemma tearing_sequences_ordered (u : nat -> R) (v : R -> nat) :
R_enum u v -> forall n : nat, let (a,b) := tearing_sequences u v n in Rlt a b.
Proof.
induction n.
- apply Rlt_0_1.
- destruct (tearing_sequences u v n) eqn:tear. destruct (tearing_sequences u v (S n)) eqn:tearS.
simpl in tearS. rewrite -> tear in tearS.
pose proof (first_two_in_interval_works u v r r0 H IHn). rewrite -> tearS in H0.
apply H0.
Qed.

(* The first tearing sequence in increasing, the second decreasing *)
Lemma tearing_sequences_inc_dec (u : nat -> R) (v : R -> nat) :
R_enum u v ->
forall n : nat, Rlt (fst (tearing_sequences u v n)) (fst (tearing_sequences u v (S n)))
/ Rlt (snd (tearing_sequences u v (S n))) (snd (tearing_sequences u v n)).
Proof.
intros. destruct (tearing_sequences u v (S n)) eqn:tear. simpl. simpl in tear.
destruct (tearing_sequences u v n) eqn:tearP. simpl.
pose proof (tearing_sequences_ordered u v H n). rewrite -> tearP in H0.
pose proof (first_two_in_interval_works u v r1 r2 H H0). rewrite -> tear in H1.
destruct H1 as [H1 [H2 [H3 [H4 H5]]]]. destruct H. split; assumption.
Qed.

Lemma split_lt_succ : forall n m : nat, lt n (S m) -> lt n m / n = m.
Proof.
intros n m. generalize dependent n. induction m.
- intros. destruct n. right. reflexivity. exfalso. inversion H. inversion H1.
- intros. destruct n. left. unfold lt. apply le_n_S. apply le_0_n.
apply lt_pred in H. simpl in H. specialize (IHm n H). destruct IHm. left. apply lt_n_S. assumption.
subst. right. reflexivity.
Qed.

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)).
Proof.
intros. induction m.
- intros. inversion H0.
- intros. destruct (split_lt_succ n m H0).
+ apply (Rlt_trans (u n) (u m)). apply IHm. assumption. apply H.
+ subst. apply H.
Qed.

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)).
Proof.
intros. induction m.
- intros. inversion H0.
- intros. destruct (split_lt_succ n m H0).
+ apply (Rlt_trans (u (S m)) (u m)). apply H. apply IHm. assumption.
+ subst. apply H.
Qed.

(* Either increase the first sequence, or decrease the second sequence,
until n = m and conclude by tearing_sequences_ordered *)
Lemma tearing_sequences_ordered_forall (u : nat -> R) (v : R -> nat) :
R_enum u v -> forall n m : nat, Rlt (fst (tearing_sequences u v n))
(snd (tearing_sequences u v m)).
Proof.
intros. destruct (n ?= m) eqn:order.
- apply Nat.compare_eq_iff in order. subst.
pose proof (tearing_sequences_ordered u v H m). destruct (tearing_sequences u v m). assumption.
- apply Nat.compare_lt_iff in order. (* increase first sequence *)
apply (Rlt_trans (fst (tearing_sequences u v n)) (fst (tearing_sequences u v m))).
remember (fun n => fst (tearing_sequences u v n)) as fseq.
pose proof (increase_seq_transit fseq). assert ((forall n : nat, (fseq n < fseq (S n))%R)).
intro n0. rewrite -> Heqfseq. apply tearing_sequences_inc_dec. assumption.
specialize (H0 H1). rewrite -> Heqfseq in H0. apply H0. assumption.
pose proof (tearing_sequences_ordered u v H m). destruct (tearing_sequences u v m). assumption.
- apply Nat.compare_gt_iff in order. (* decrease second sequence *)
apply (Rlt_trans (fst (tearing_sequences u v n)) (snd (tearing_sequences u v n))).
pose proof (tearing_sequences_ordered u v H n). destruct (tearing_sequences u v n). assumption.
remember (fun n => snd (tearing_sequences u v n)) as sseq.
pose proof (decrease_seq_transit sseq). assert ((forall n : nat, (sseq (S n) < sseq n)%R)).
intro n0. rewrite -> Heqsseq. apply tearing_sequences_inc_dec. assumption.
specialize (H0 H1). rewrite -> Heqsseq in H0. apply H0. assumption.
Qed.

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

(* The limit of the first tearing sequence cannot be reached by u *)
Definition torn_number (u : nat -> R) (v : R -> nat) :
R_enum u v -> is_lub (tearing_elem_fst u v) m.
Proof.
intros. assert (bound (tearing_elem_fst u v)).
exists (INR 1). intros x H0. destruct H0 as [n H0]. subst. left.
apply (tearing_sequences_ordered_forall u v H n 0).
apply (completeness (tearing_elem_fst u v) H0).
exists (INR 0). exists 0. reflexivity.
Defined.

Lemma torn_number_above_first_sequence (u : nat -> R) (v : R -> nat) (en : R_enum u v) :
forall n : nat, Rlt (fst (tearing_sequences u v n))
(proj1_sig (torn_number u v en)).
Proof.
intros. destruct (torn_number u v en) as [torn i]. simpl.
destruct (Rlt_le_dec (fst (tearing_sequences u v n)) torn). assumption. exfalso.
destruct i. (* Apply the first sequence once to make the inequality strict *)
assert (Rlt torn (fst (tearing_sequences u v (S n)))).
apply (Rle_lt_trans torn (fst (tearing_sequences u v n))). assumption.
apply tearing_sequences_inc_dec. assumption.
clear r. specialize (H (fst (tearing_sequences u v (S n)))).
assert (tearing_elem_fst u v (fst (tearing_sequences u v (S n)))).
exists (S n). reflexivity.
specialize (H H2). assert (Rlt torn torn).
apply (Rlt_le_trans torn (fst (tearing_sequences u v (S n)))); assumption.
apply Rlt_irrefl in H3. contradiction.
Qed.

(* The torn number is between both tearing sequences, so it could have been chosen
at each step. *)
Lemma torn_number_below_second_sequence (u : nat -> R) (v : R -> nat) (en : R_enum u v) :
forall n : nat, Rlt (proj1_sig (torn_number u v en))
(snd (tearing_sequences u v n)).
Proof.
intros. destruct (torn_number u v en) as [torn i]. simpl.
destruct (Rlt_le_dec torn (snd (tearing_sequences u v n)))
as [l|h].
- assumption.
- exfalso. (* Apply the second sequence once to make the inequality strict *)
assert (Rlt (snd (tearing_sequences u v (S n))) torn).
apply (Rlt_le_trans (snd (tearing_sequences u v (S n))) (snd (tearing_sequences u v n)) torn).
apply (tearing_sequences_inc_dec u v en n). assumption.
clear h. (* Then prove snd (tearing_sequences u v (S n)) is an upper bound of the first
sequence. It will yield the contradiction torn < torn. *)
assert (is_upper_bound (tearing_elem_fst u v) (snd (tearing_sequences u v (S n)))).
intros x H0. destruct H0. subst. left. apply tearing_sequences_ordered_forall. assumption.
destruct i. apply H2 in H0.
pose proof (Rle_lt_trans torn (snd (tearing_sequences u v (S n))) torn H0 H).
apply Rlt_irrefl in H3. contradiction.
Qed.

(* Here is the contradiction : the torn number's index is above a sequence that tends to infinity *)
Lemma limit_index_above_all_indices (u : nat -> R) (v : R -> nat) (en : R_enum u v) :
forall n : nat, v (fst (tearing_sequences u v (S n))) < v (proj1_sig (torn_number u v en)).
Proof.
intros. simpl. destruct (tearing_sequences u v n) eqn:tear.
(* The torn number was not chosen, so its index is above *)
pose proof (tearing_sequences_ordered u v en n). rewrite -> tear in H.
pose proof (first_two_in_interval_works u v r r0 en H).
destruct (first_two_in_interval u v r r0) eqn:ft. simpl.
assert (tearing_sequences u v (S n) = (r1, r2)).
simpl. rewrite -> tear. assumption.
apply H0.
- pose proof (torn_number_above_first_sequence u v en n). rewrite -> tear in H2. assumption.
- pose proof (torn_number_below_second_sequence u v en n). rewrite -> tear in H2. assumption.
- pose proof (torn_number_above_first_sequence u v en (S n)). rewrite -> H1 in H2. simpl in H2.
intro H5. subst. apply Rlt_irrefl in H2. contradiction.
- pose proof (torn_number_below_second_sequence u v en (S n)). rewrite -> H1 in H2. simpl in H2.
intro H5. subst. apply Rlt_irrefl in H2. contradiction.
Qed.

(* The indices increase because each time the minimum index is chosen *)
Lemma first_indices_increasing (u : nat -> R) (v : R -> nat) :
R_enum u v -> forall n : nat, n <> 0 -> v (fst (tearing_sequences u v n))
< v (fst (tearing_sequences u v (S n))).
Proof.
intros. destruct n. contradiction. simpl.
pose proof (tearing_sequences_ordered u v H n).
destruct (tearing_sequences u v n) eqn:tear.
pose proof (first_two_in_interval_works u v r r0 H H1).
destruct (first_two_in_interval u v r r0) eqn:ft. simpl.
destruct H2 as [fth [fth0 [fth1 [fth2 [fth3 fth4]]]]].
pose proof (first_two_in_interval_works u v r1 r2 H fth3).
destruct (first_two_in_interval u v r1 r2) eqn:ft2. simpl.
destruct H2 as [H2 [H3 [H4 [H5 [H6 H7]]]]]. destruct H.
apply fth4.
- apply (Rlt_trans r r1); assumption.
- apply (Rlt_trans r3 r2); assumption.
- intro abs. subst. apply Rlt_irrefl in H2. contradiction.
- intro abs. subst. apply Rlt_irrefl in H3. contradiction.
Qed.

Theorem r_uncountable : forall (u : nat -> R) (v : R -> nat), ~R_enum u v.
Proof.
intros u v H.
assert (forall n : nat, n + v (fst (tearing_sequences u v 1))
<= v (fst (tearing_sequences u v (S n)))).
induction n. simpl. apply le_refl.
apply (le_trans (S n + v (fst (tearing_sequences u v 1)))
(S (v (fst (tearing_sequences u v (S n)))))).
simpl. apply le_n_S. assumption.
apply first_indices_increasing. assumption. discriminate.
assert (v (proj1_sig (torn_number u v H)) + v (fst (tearing_sequences u v 1))
< v (proj1_sig (torn_number u v H))).
pose proof (limit_index_above_all_indices u v H (v (proj1_sig (torn_number u v H)))).
specialize (H0 (v (proj1_sig (torn_number u v H)))).
apply (le_lt_trans (v (proj1_sig (torn_number u v H)) + v (fst (tearing_sequences u v 1)))
(v (fst (tearing_sequences u v (S (v (proj1_sig (torn_number u v H)))))))).
assumption. assumption.
assert (forall n m : nat, ~(n + m < n)).
induction n. intros. intro H2. inversion H2. intro m. intro H2. simpl in H2.
apply lt_pred in H2. simpl in H2. apply IHn in H2. contradiction.
apply H2 in H1. contradiction.
Qed.


2 Answers
2

In ZFC, the real numbers satisfy two useful properties:

there is a function e : R * R -> bool that returns true if and only if its two arguments are equal, and

e : R * R -> bool

the order relation is antisymmetric: if x <= y and y <= x, then x = y.

x <= y

y <= x

x = y

Both of these properties would fail in Coq if the real numbers were defined without additional axioms in terms of Cauchy sequences or Dedekind cuts. For example, a Dedekind cut can be defined as a pair of predicates P Q : rational -> Prop that satisfy certain properties. It is impossible to write a Coq function that decides whether two cuts are equal, because equality of predicates on rationals is undecidable. And any reasonable notion of ordering on cuts would fail to satisfy antisymmetry because equality on predicates is not extensional: it is not the case that forall x, P x <-> Q x implies P = Q.

P Q : rational -> Prop

forall x, P x <-> Q x

P = Q

As for your second question, it is true that there can be only countably many Coq terms of type R -> Prop. However, the same is true of ZFC: there are only countably many formulas for defining subsets of the real numbers. This is connected to the Löwenheim-Skolem paradox, which implies that if ZFC is consistent it has a countable model -- which, in particular, would have only countably many real numbers. Both in ZFC and in Coq, however, it is impossible to define a function that enumerates all real numbers: they are countable from our own external perspective on the theory, but uncountable from the theory's point of view.

R -> Prop

Qeq

Qle

Qeq

1#2 <> 2#4

R

Axiom total_order_T

Axiom total_order_P : forall r1 r2:R, (r1 < r2) / (r1 = r2) / (r1 > r2)

=

forall P, P + ~ P

Many think that the current definition of Real numbers in Coq is far from optimal and we are just waiting for someone to produce a better alternative. The choice of axioms introduces many complications [including consistency problems in the past], and a formulation in terms of cuts plus excluded middle would be great to have.

If I am not mistaken the proof of the four color theorem includes such a formalization; also, constructive developments such as CoRN should work as it is usually the case that most theorems of classical analysis can be recovered from their intuitionistic version plus + EM.

located

Prop

Rlt_linear

located

Prop

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.