coq - 为什么在 Coq 中实数是公理化的？
问题描述
我想知道 Coq 是否将实数定义为 Cauchy 序列或 Dedekind 切割，所以我检查了 Coq.Reals.Raxioms 和......这两个都没有。实数及其运算（如Parameters 和Axioms）被公理化。为什么会这样？
此外，实数紧密依赖于子集的概念，因为它们的定义属性之一是每个上界子集都有一个最小上界。将Axiom completeness这些子集编码为Props。
我的印象是这些Props 仅形成实数的可定义子集。那么 Coq 是否只能访问可定义的实数？这个 Coq 到底是什么R？解析数字？代数数？算术数字？
如果，正如我所怀疑的那样，Coq 只有实数的可数子集（因为只有可数的多个Props），那就是实数的无穷小部分。它是否适合深入利用 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 悖论的一种表现。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当且仅当它的两个参数相等时，有一个函数返回 true，并且顺序关系是反对称的：如果
x <= y和y <= x，则x = y。
如果在没有附加公理的情况下根据柯西序列或戴德金割来定义实数，那么这两个属性在 Coq 中都将失效。例如，Dedekind 割可以定义为一对P Q : rational -> Prop满足某些属性的谓词。不可能编写一个 Coq 函数来决定两个割是否相等，因为有理数上的谓词相等是不可判定的。并且任何合理的切割排序概念都无法满足反对称，因为谓词上的相等性不是外延的：它不是forall x, P x <-> Q x暗示的情况P = Q。
至于你的第二个问题，确实只能有许多 Coq 术语 type R -> Prop。然而，ZFC 也是如此：定义实数子集的公式只有可数个。这与Löwenheim-Skolem 悖论有关，这意味着如果 ZFC 是一致的，它就有一个可数模型——特别是，它只有可数个实数。然而，在 ZFC 和 Coq 中，不可能定义一个枚举所有实数的函数：从我们自己的理论外部角度来看，它们是可数的，但从理论的角度来看是不可数的。
推荐阅读
- android - Room：使用 ID 检索用户信息
- css - DataTable中一个单元格的动态css - PrimeNG
- apache-kafka - 以 Kafka Avro 文件格式将新模式/主题添加到模式注册表
- java - 从命令行运行 Verticle 时找不到包
- java - 对 sendBroadcast(intent) 无操作
- ios - iOS Scope Bar 添加到 UISearchBar 下后不出现
- javascript - 将 js 对象发送为 html 表单
- r - 所有在 Shiny 中绘制 xray 分布的输出？
- functional-programming - Kotlin 中的元素算术运算
- node.js - 返回节点尝试捕获嵌套的异步错误