为什么 Coq 中的实数公理化？
Why are the real numbers axiomatized in Coq?
我想知道 Coq 是将实数定义为 Cauchy 序列还是 Dedekind 割，所以我检查了 Coq.Reals.Raxioms 和... none 这两个。实数及其运算（如 Parameters 和 Axioms）被公理化。为什么会这样？
此外，实数严格依赖子集的概念，因为它们的定义属性之一是每个上界子集都有一个最小上界。 Axiom completeness 将这些子集编码为 Props.
我的印象是这些 Prop 仅构成实数的可定义子集。那么 Coq 只能访问 definable real numbers 吗？这个 Coq 的 R 到底是什么？分析数字？代数数？算术数？
如果像我怀疑的那样，Coq 只有实数的可数子集（因为只有可数的 Prop ），那就是实数的无穷小部分。它是否适合深入利用 ZFC 实数结构的理论，例如分形、混沌理论或勒贝格测度？
编辑
这是 Dedekind 削减对实数的朴素构造。
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.
编辑
这是 Coq 中的一个证明 R 是不可数的。我真的不知道该怎么想，因为 Props 显然可以从 Coq 外部计算。正如 Arthur Azevedo De Amorim 所暗示的，这可能是 Skolem's paradox 的表现。我要表达的方式是 R 和 nat 之间的双射不能用 Coq 编写。也许出于与不可能在 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 当且仅当它的两个参数相等时 returns 为真，并且
顺序关系是反对称的：如果x <= y和y <= x，则x = y。
如果根据柯西序列或 Dedekind 切割定义实数而没有附加公理，则这两个属性在 Coq 中都将失效。例如，Dedekind 切割可以定义为满足特定属性的一对谓词 P Q : rational -> Prop。不可能编写一个 Coq 函数来决定两个切割是否相等，因为有理数上的谓词相等是不可判定的。并且任何合理的切割排序概念都无法满足反对称，因为谓词上的相等性不是外延的：forall x, P x <-> Q x 并不意味着 P = Q.
关于你的第二个问题，R -> Prop 类型的 Coq 项确实只能有可数个。然而，ZFC 也是如此：定义实数子集的公式只有可数个。这与 Löwenheim-Skolem paradox 相关联，这意味着如果 ZFC 是一致的，它有一个可数模型——特别是，它只有可数个实数。然而，在 ZFC 和 Coq 中，都不可能定义一个枚举所有实数的函数：从我们自己的外部理论角度来看，它们是可数的，但从理论的角度来看是不可数的。
许多人认为 Coq 中实数的当前定义远非最佳，我们只是在等待有人提出更好的替代方案。公理的选择引入了许多复杂性[包括过去的一致性问题]，并且根据切割加排中的公式会很棒。
如果我没记错的话，四色定理的证明就包含这样的形式化；此外，像 CoRN 这样的建设性发展应该会起作用，因为通常情况下，大多数经典分析定理都可以从其直觉版本加上 + EM 中恢复。
我想知道 Coq 是将实数定义为 Cauchy 序列还是 Dedekind 割，所以我检查了 Coq.Reals.Raxioms 和... none 这两个。实数及其运算（如 Parameters 和 Axioms）被公理化。为什么会这样？
此外，实数严格依赖子集的概念，因为它们的定义属性之一是每个上界子集都有一个最小上界。 Axiom completeness 将这些子集编码为 Props.
我的印象是这些 Prop 仅构成实数的可定义子集。那么 Coq 只能访问 definable real numbers 吗？这个 Coq 的 R 到底是什么？分析数字？代数数？算术数？
如果像我怀疑的那样，Coq 只有实数的可数子集（因为只有可数的 Prop ），那就是实数的无穷小部分。它是否适合深入利用 ZFC 实数结构的理论，例如分形、混沌理论或勒贝格测度？
编辑
这是 Dedekind 削减对实数的朴素构造。
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.
编辑
这是 Coq 中的一个证明 R 是不可数的。我真的不知道该怎么想，因为 Props 显然可以从 Coq 外部计算。正如 Arthur Azevedo De Amorim 所暗示的，这可能是 Skolem's paradox 的表现。我要表达的方式是 R 和 nat 之间的双射不能用 Coq 编写。也许出于与不可能在 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当且仅当它的两个参数相等时 returns 为真，并且顺序关系是反对称的：如果
x <= y和y <= x，则x = y。
如果根据柯西序列或 Dedekind 切割定义实数而没有附加公理，则这两个属性在 Coq 中都将失效。例如，Dedekind 切割可以定义为满足特定属性的一对谓词 P Q : rational -> Prop。不可能编写一个 Coq 函数来决定两个切割是否相等，因为有理数上的谓词相等是不可判定的。并且任何合理的切割排序概念都无法满足反对称，因为谓词上的相等性不是外延的：forall x, P x <-> Q x 并不意味着 P = Q.
关于你的第二个问题，R -> Prop 类型的 Coq 项确实只能有可数个。然而，ZFC 也是如此：定义实数子集的公式只有可数个。这与 Löwenheim-Skolem paradox 相关联，这意味着如果 ZFC 是一致的，它有一个可数模型——特别是，它只有可数个实数。然而，在 ZFC 和 Coq 中，都不可能定义一个枚举所有实数的函数：从我们自己的外部理论角度来看，它们是可数的，但从理论的角度来看是不可数的。
许多人认为 Coq 中实数的当前定义远非最佳，我们只是在等待有人提出更好的替代方案。公理的选择引入了许多复杂性[包括过去的一致性问题]，并且根据切割加排中的公式会很棒。
如果我没记错的话，四色定理的证明就包含这样的形式化；此外，像 CoRN 这样的建设性发展应该会起作用，因为通常情况下，大多数经典分析定理都可以从其直觉版本加上 + EM 中恢复。