-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathRationalsInReals.v
128 lines (116 loc) · 2.61 KB
/
RationalsInReals.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
Require Export Reals.
Require Export QArith.
Require Export Qreals.
Open Scope R_scope.
Lemma inverses_of_nats_approach_0:
forall eps:R, eps > 0 -> exists n:nat, (n > 0)%nat /\
/ (INR n) < eps.
Proof.
intros.
assert (exists n:Z, (n>0)%Z /\ / (IZR n) < eps).
exists (up (/ eps)); split.
assert (IZR (up (/ eps)) > 0).
apply Rgt_trans with (/ eps).
apply archimed.
auto with *.
assert ((0 < up (/ eps))%Z).
apply lt_IZR.
simpl.
assumption.
auto with *.
pattern eps at 2.
rewrite <- Rinv_involutive.
apply Rinv_lt_contravar.
apply Rmult_lt_0_compat; auto with *.
apply Rlt_trans with (/ eps); auto with *.
apply archimed.
apply archimed.
auto with *.
destruct H0 as [[ | p | p]].
destruct H0.
contradict H0; auto with *.
destruct H0.
exists (nat_of_P p).
split; auto with *.
destruct H0.
contradict H0.
red; intro.
inversion H0.
Qed.
Lemma Z_interpolation: forall x y:R, y > x+1 ->
exists n:Z, x < IZR n < y.
Proof.
intros.
exists (up x).
split.
apply archimed.
apply Rle_lt_trans with (x+1).
pose proof (archimed x).
destruct H0.
assert (x + (IZR (up x) - x) <= x + 1).
auto with real.
ring_simplify in H2.
assumption.
assumption.
Qed.
Lemma rational_interpolation: forall (x y:R) (n:positive),
x<y -> IZR (' n) > 1/(y-x) ->
exists m:Z, x < Q2R (m # n) < y.
Proof.
intros.
assert (0 < / IZR (' n)).
cut (0 < IZR (' n)); auto with real.
replace 0 with (IZR 0) by trivial.
cut ((0 < ' n)%Z); auto with *.
apply IZR_lt.
unfold Zlt.
trivial.
destruct (Z_interpolation (IZR (' n) * x)
(IZR (' n) * y)) as [m].
apply Rgt_minus in H.
assert (IZR (' n) * (y - x) > 1).
replace 1 with ((1 / (y-x)) * (y-x)); try field.
apply Rmult_gt_compat_r; trivial.
auto with real.
apply Rgt_minus in H2.
apply Rminus_gt.
match goal with H2: ?a > 0 |- ?b > 0 => replace b with a end.
trivial.
ring.
exists m.
unfold Q2R.
simpl.
replace (INR (nat_of_P n)) with (IZR (' n)) by auto with real.
replace x with ((IZR (' n) * x) / IZR (' n)).
replace y with ((IZR (' n) * y) / IZR (' n)).
destruct H2.
split.
apply Rmult_lt_compat_r; trivial.
apply Rmult_lt_compat_r; trivial.
field.
auto with *.
field.
auto with *.
Qed.
Lemma rationals_dense_in_reals: forall x y:R, x<y ->
exists q:Q, x < Q2R q < y.
Proof.
intros.
pose (d := up (/ (y - x))).
assert ((0 < d)%Z).
apply lt_IZR.
simpl.
apply Rlt_trans with (/ (y - x)).
apply Rgt_minus in H.
auto with *.
apply archimed.
assert (/ (y - x) < IZR d) by apply archimed.
destruct d as [|d|]; try discriminate H0.
destruct (rational_interpolation x y d) as [n]; trivial.
replace (1 / (y-x)) with (/(y-x)).
trivial.
field.
apply Rgt_minus in H.
auto with real.
exists (n # d); trivial.
Qed.