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
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \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.
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 in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *;
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 in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *;
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 in |- *; do 2 rewrite <- mult_IZR.
apply IZR_eq; auto.
clear H.
field_simplify_eq; auto.
ring_simplify X1 Y2 (Y2 * X1)%R.
rewrite H0 in |- *; ring.
Qed.
Lemma Rle_Qle : forall x y : Q, (Q2R x <= Q2R y)%R -> x<=y.
Proof.
unfold Qle, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *;
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 in |- *; replace 0%R with (IZR 0); auto; apply IZR_le;
auto with zarith.
unfold Y2 in |- *; 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 in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *;
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 in |- *; 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 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *;
auto with zarith.
unfold Y2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *;
auto with zarith.
Qed.
Lemma Rlt_Qlt : forall x y : Q, (Q2R x < Q2R y)%R -> x<y.
Proof.
unfold Qlt, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *;
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 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *;
auto with zarith.
unfold Y2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *;
auto with zarith.
Qed.
Lemma Qlt_Rlt : forall x y : Q, x<y -> (Q2R x < Q2R y)%R.
Proof.
unfold Qlt, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *;
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 in |- *; 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 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *;
auto with zarith.
unfold Y2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *;
auto with zarith.
Qed.
Lemma Q2R_plus : forall x y : Q, Q2R (x+y) = (Q2R x + Q2R y)%R.
Proof.
unfold Qplus, Qeq, Q2R in |- *; intros (x1, x2) (y1, y2);
unfold Qden, Qnum in |- *.
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 in |- *; intros (x1, x2) (y1, y2);
unfold Qden, Qnum in |- *.
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 in |- *; intros (x1, x2); unfold Qden, Qnum in |- *.
rewrite Ropp_Ropp_IZR.
field; auto.
Qed.
Lemma Q2R_minus : forall x y : Q, Q2R (x-y) = (Q2R x - Q2R y)%R.
unfold Qminus in |- *; 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 in |- *; intros (x1, x2); unfold Qden, Qnum in |- *.
case x1.
simpl in |- *; intros; elim H; trivial.
intros; field; auto.
intros;
change (IZR (Zneg x2)) with (- IZR (' x2))%R in |- *;
change (IZR (Zneg p)) with (- IZR (' p))%R in |- *;
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 in |- *.
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.
Section LegacyQField.
(** In the past, the field tactic was not able to deal with setoid datatypes,
so translating from Q to R and applying field on reals was a workaround.
See now Qfield for a direct field tactic on Q. *)
Ltac QField := apply eqR_Qeq; autorewrite with q2r_simpl; try field; auto.
(** Examples of use: *)
Let ex1 : forall x y z : Q, (x+y)*z == (x*z)+(y*z).
intros; QField.
Qed.
Let ex2 : forall x y : Q, ~ y==0 -> (x/y)*y == x.
intros; QField.
intro; apply H; apply eqR_Qeq.
rewrite H0; unfold Q2R in |- *; simpl in |- *; field; auto with real.
Qed.
End LegacyQField.
|
