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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Export Rbase.
Require Export QArith_base.
(** Injection of rational numbers into real numbers. *)
Definition Q2R (x : Q) : R := (IZR (Qnum x) * / IZR (QDen x))%R.
Lemma IZR_nz : forall p : positive, IZR (Zpos p) <> 0%R.
Proof.
intros; apply not_O_IZR; auto with qarith.
Qed.
Hint Resolve IZR_nz Rmult_integral_contrapositive.
Lemma eqR_Qeq : forall x y : Q, Q2R x = Q2R y -> x==y.
Proof.
unfold Qeq, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden;
intros.
apply eq_IZR.
do 2 rewrite mult_IZR.
set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2);
set (X2 := IZR (Zpos x2)) in *.
set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
set (Y2 := IZR (Zpos y2)) in *.
assert ((X2 * X1 * / X2)%R = (X2 * (Y1 * / Y2))%R).
rewrite <- H; field; auto.
rewrite Rinv_r_simpl_m in H0; auto; rewrite H0; field; auto.
Qed.
Lemma Qeq_eqR : forall x y : Q, x==y -> Q2R x = Q2R y.
Proof.
unfold Qeq, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden;
intros.
set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2);
set (X2 := IZR (Zpos x2)) in *.
set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
set (Y2 := IZR (Zpos y2)) in *.
assert ((X1 * Y2)%R = (Y1 * X2)%R).
unfold X1, X2, Y1, Y2; do 2 rewrite <- mult_IZR.
apply IZR_eq; auto.
clear H.
field_simplify_eq; auto.
ring_simplify X1 Y2 (Y2 * X1)%R.
rewrite H0; ring.
Qed.
Lemma Rle_Qle : forall x y : Q, (Q2R x <= Q2R y)%R -> x<=y.
Proof.
unfold Qle, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden;
intros.
apply le_IZR.
do 2 rewrite mult_IZR.
set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2);
set (X2 := IZR (Zpos x2)) in *.
set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
set (Y2 := IZR (Zpos y2)) in *.
replace (X1 * Y2)%R with (X1 * / X2 * (X2 * Y2))%R; try (field; auto).
replace (Y1 * X2)%R with (Y1 * / Y2 * (X2 * Y2))%R; try (field; auto).
apply Rmult_le_compat_r; auto.
apply Rmult_le_pos.
unfold X2; replace 0%R with (IZR 0); auto; apply IZR_le;
auto with zarith.
unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_le;
auto with zarith.
Qed.
Lemma Qle_Rle : forall x y : Q, x<=y -> (Q2R x <= Q2R y)%R.
Proof.
unfold Qle, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden;
intros.
set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2);
set (X2 := IZR (Zpos x2)) in *.
set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
set (Y2 := IZR (Zpos y2)) in *.
assert (X1 * Y2 <= Y1 * X2)%R.
unfold X1, X2, Y1, Y2; do 2 rewrite <- mult_IZR.
apply IZR_le; auto.
clear H.
replace (X1 * / X2)%R with (X1 * Y2 * (/ X2 * / Y2))%R; try (field; auto).
replace (Y1 * / Y2)%R with (Y1 * X2 * (/ X2 * / Y2))%R; try (field; auto).
apply Rmult_le_compat_r; auto.
apply Rmult_le_pos; apply Rlt_le; apply Rinv_0_lt_compat.
unfold X2; replace 0%R with (IZR 0); auto; apply IZR_lt; red;
auto with zarith.
unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_lt; red;
auto with zarith.
Qed.
Lemma Rlt_Qlt : forall x y : Q, (Q2R x < Q2R y)%R -> x<y.
Proof.
unfold Qlt, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden;
intros.
apply lt_IZR.
do 2 rewrite mult_IZR.
set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2);
set (X2 := IZR (Zpos x2)) in *.
set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
set (Y2 := IZR (Zpos y2)) in *.
replace (X1 * Y2)%R with (X1 * / X2 * (X2 * Y2))%R; try (field; auto).
replace (Y1 * X2)%R with (Y1 * / Y2 * (X2 * Y2))%R; try (field; auto).
apply Rmult_lt_compat_r; auto.
apply Rmult_lt_0_compat.
unfold X2; replace 0%R with (IZR 0); auto; apply IZR_lt; red;
auto with zarith.
unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_lt; red;
auto with zarith.
Qed.
Lemma Qlt_Rlt : forall x y : Q, x<y -> (Q2R x < Q2R y)%R.
Proof.
unfold Qlt, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden;
intros.
set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2);
set (X2 := IZR (Zpos x2)) in *.
set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
set (Y2 := IZR (Zpos y2)) in *.
assert (X1 * Y2 < Y1 * X2)%R.
unfold X1, X2, Y1, Y2; do 2 rewrite <- mult_IZR.
apply IZR_lt; auto.
clear H.
replace (X1 * / X2)%R with (X1 * Y2 * (/ X2 * / Y2))%R; try (field; auto).
replace (Y1 * / Y2)%R with (Y1 * X2 * (/ X2 * / Y2))%R; try (field; auto).
apply Rmult_lt_compat_r; auto.
apply Rmult_lt_0_compat; apply Rinv_0_lt_compat.
unfold X2; replace 0%R with (IZR 0); auto; apply IZR_lt; red;
auto with zarith.
unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_lt; red;
auto with zarith.
Qed.
Lemma Q2R_plus : forall x y : Q, Q2R (x+y) = (Q2R x + Q2R y)%R.
Proof.
unfold Qplus, Qeq, Q2R; intros (x1, x2) (y1, y2);
unfold Qden, Qnum.
simpl_mult.
rewrite plus_IZR.
do 3 rewrite mult_IZR.
field; auto.
Qed.
Lemma Q2R_mult : forall x y : Q, Q2R (x*y) = (Q2R x * Q2R y)%R.
Proof.
unfold Qmult, Qeq, Q2R; intros (x1, x2) (y1, y2);
unfold Qden, Qnum.
simpl_mult.
do 2 rewrite mult_IZR.
field; auto.
Qed.
Lemma Q2R_opp : forall x : Q, Q2R (- x) = (- Q2R x)%R.
Proof.
unfold Qopp, Qeq, Q2R; intros (x1, x2); unfold Qden, Qnum.
rewrite Ropp_Ropp_IZR.
field; auto.
Qed.
Lemma Q2R_minus : forall x y : Q, Q2R (x-y) = (Q2R x - Q2R y)%R.
Proof.
unfold Qminus; intros; rewrite Q2R_plus; rewrite Q2R_opp; auto.
Qed.
Lemma Q2R_inv : forall x : Q, ~ x==0 -> Q2R (/x) = (/ Q2R x)%R.
Proof.
unfold Qinv, Q2R, Qeq; intros (x1, x2). case x1; unfold Qnum, Qden.
simpl; intros; elim H; trivial.
intros; field; auto.
intros;
change (IZR (Zneg x2)) with (- IZR (' x2))%R;
change (IZR (Zneg p)) with (- IZR (' p))%R;
simpl; field; (*auto 8 with real.*)
repeat split; auto; auto with real.
Qed.
Lemma Q2R_div :
forall x y : Q, ~ y==0 -> Q2R (x/y) = (Q2R x / Q2R y)%R.
Proof.
unfold Qdiv, Rdiv.
intros; rewrite Q2R_mult.
rewrite Q2R_inv; auto.
Qed.
Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl.
|
