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?
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.
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?
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?
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
这是Coq的一个证据,R是不可数的.我真的不知道该怎么想,因为Prop从外面的Coq 看起来很明显.这可能是斯科勒姆悖论的一种表现,正如亚瑟·阿泽维多·德阿莫林所暗示的那样.我想说的方式是在Coq 之间R和之间的双射nat.也许出于类似的原因,无法在Coq中编写Coq解释器.
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 -> {m : R | 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.
在ZFC中,实数满足两个有用的属性:
有一个函数e : R * R -> bool,当且仅当它的两个参数相等时返回true,并且
顺序关系是反对称的:if x <= y和y <= x,然后x = y.
如果在Cauchy序列或Dedekind切割方面没有附加公理的情况下定义实数,则这两个属性在Coq中都会失败.例如,Dedekind剪切可以定义为P Q : rational -> Prop满足某些属性的一对谓词.编写一个Coq函数来判断两个切割是否相等是不可能的,因为有理数的谓词相等是不可判定的.和顺序对削减任何合理的概念将无法满足反对称因为谓词平等是不伸展:这是不是说情况forall x, P x <-> Q x暗示P = Q.
至于你的第二个问题,确实只有相当多的Coq术语类型R -> Prop.然而,ZFC也是如此:只有很多公式可用于定义实数的子集.这与Löwenheim-Skolem悖论有关,这意味着如果ZFC是一致的,它有一个可数模型 - 特别是,它只有相当多的实数.然而,无论是在ZFC还是在Coq中,都不可能定义一个列举所有实数的函数:它们可以从我们自己对理论的外部视角中计算出来,但从理论的角度来看是不可数的.