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
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
Require Export Rbase.
Comments "Lemmas used by the tactic Fourier".
Lemma Rfourier_lt:
(x1, y1, a : R) (Rlt x1 y1) -> (Rlt R0 a) -> (Rlt (Rmult a x1) (Rmult a y1)).
Intros x1 y1 a H H0; Try Assumption.
Apply Rlt_monotony; Auto with real.
Qed.
Lemma Rfourier_le:
(x1, y1, a : R) (Rle x1 y1) -> (Rlt R0 a) -> (Rle (Rmult a x1) (Rmult a y1)).
Red.
Intros.
Case H; Auto with real.
Qed.
Lemma Rfourier_lt_lt:
(x1, y1, x2, y2, a : R)
(Rlt x1 y1) ->
(Rlt x2 y2) ->
(Rlt R0 a) -> (Rlt (Rplus x1 (Rmult a x2)) (Rplus y1 (Rmult a y2))).
Intros x1 y1 x2 y2 a H H0 H1; Try Assumption.
Apply Rplus_lt.
Try Exact H.
Apply Rfourier_lt.
Try Exact H0.
Try Exact H1.
Qed.
Lemma Rfourier_lt_le:
(x1, y1, x2, y2, a : R)
(Rlt x1 y1) ->
(Rle x2 y2) ->
(Rlt R0 a) -> (Rlt (Rplus x1 (Rmult a x2)) (Rplus y1 (Rmult a y2))).
Intros x1 y1 x2 y2 a H H0 H1; Try Assumption.
Case H0; Intros.
Apply Rplus_lt.
Try Exact H.
Apply Rfourier_lt; Auto with real.
Rewrite H2.
Rewrite (Rplus_sym y1 (Rmult a y2)).
Rewrite (Rplus_sym x1 (Rmult a y2)).
Apply Rlt_compatibility.
Try Exact H.
Qed.
Lemma Rfourier_le_lt:
(x1, y1, x2, y2, a : R)
(Rle x1 y1) ->
(Rlt x2 y2) ->
(Rlt R0 a) -> (Rlt (Rplus x1 (Rmult a x2)) (Rplus y1 (Rmult a y2))).
Intros x1 y1 x2 y2 a H H0 H1; Try Assumption.
Case H; Intros.
Apply Rfourier_lt_le; Auto with real.
Rewrite H2.
Apply Rlt_compatibility.
Apply Rfourier_lt; Auto with real.
Qed.
Lemma Rfourier_le_le:
(x1, y1, x2, y2, a : R)
(Rle x1 y1) ->
(Rle x2 y2) ->
(Rlt R0 a) -> (Rle (Rplus x1 (Rmult a x2)) (Rplus y1 (Rmult a y2))).
Intros x1 y1 x2 y2 a H H0 H1; Try Assumption.
Case H0; Intros.
Red.
Left; Try Assumption.
Apply Rfourier_le_lt; Auto with real.
Rewrite H2.
Case H; Intros.
Red.
Left; Try Assumption.
Rewrite (Rplus_sym x1 (Rmult a y2)).
Rewrite (Rplus_sym y1 (Rmult a y2)).
Apply Rlt_compatibility.
Try Exact H3.
Rewrite H3.
Red.
Right; Try Assumption.
Auto with real.
Qed.
Lemma Rlt_zero_pos_plus1: (x : R) (Rlt R0 x) -> (Rlt R0 (Rplus R1 x)).
Intros x H; Try Assumption.
Rewrite Rplus_sym.
Apply Rlt_r_plus_R1.
Red; Auto with real.
Qed.
Lemma Rlt_mult_inv_pos:
(x, y : R) (Rlt R0 x) -> (Rlt R0 y) -> (Rlt R0 (Rmult x (Rinv y))).
Intros x y H H0; Try Assumption.
Replace R0 with (Rmult x R0).
Apply Rlt_monotony; Auto with real.
Ring.
Qed.
Lemma Rlt_zero_1: (Rlt R0 R1).
Exact Rlt_R0_R1.
Qed.
Lemma Rle_zero_pos_plus1: (x : R) (Rle R0 x) -> (Rle R0 (Rplus R1 x)).
Intros x H; Try Assumption.
Case H; Intros.
Red.
Left; Try Assumption.
Apply Rlt_zero_pos_plus1; Auto with real.
Rewrite <- H0.
Replace (Rplus R1 R0) with R1.
Red; Left.
Exact Rlt_zero_1.
Ring.
Qed.
Lemma Rle_mult_inv_pos:
(x, y : R) (Rle R0 x) -> (Rlt R0 y) -> (Rle R0 (Rmult x (Rinv y))).
Intros x y H H0; Try Assumption.
Case H; Intros.
Red; Left.
Apply Rlt_mult_inv_pos; Auto with real.
Rewrite <- H1.
Red; Right; Ring.
Qed.
Lemma Rle_zero_1: (Rle R0 R1).
Red; Left.
Exact Rlt_zero_1.
Qed.
Lemma Rle_not_lt:
(n, d : R) (Rle R0 (Rmult n (Rinv d))) -> ~ (Rlt R0 (Rmult (Ropp n) (Rinv d))).
Intros n d H; Red; Intros H0; Try Exact H0.
Generalize (Rle_not R0 (Rmult n (Rinv d))).
Intros H1; Elim H1; Try Assumption.
Replace (Rmult n (Rinv d)) with (Ropp (Ropp (Rmult n (Rinv d)))).
Replace R0 with (Ropp (Ropp R0)).
Replace (Ropp (Rmult n (Rinv d))) with (Rmult (Ropp n) (Rinv d)).
Replace (Ropp R0) with R0.
Red.
Try Exact H0.
Apply Rgt_Ropp.
Replace (Ropp (Rmult n (Rinv d))) with (Rmult (Ropp n) (Rinv d)).
Replace (Ropp R0) with R0.
Red.
Try Exact H0.
Ring.
Ring.
Ring.
Ring.
Ring.
Ring.
Qed.
Lemma Rnot_lt0: (x : R) ~ (Rlt R0 (Rmult R0 x)).
Intros x; Try Assumption.
Replace (Rmult R0 x) with R0.
Apply Rlt_antirefl.
Ring.
Qed.
Lemma Rlt_not_le:
(n, d : R) (Rlt R0 (Rmult n (Rinv d))) -> ~ (Rle R0 (Rmult (Ropp n) (Rinv d))).
Intros n d H; Try Assumption.
Apply Rle_not.
Replace R0 with (Ropp R0).
Replace (Rmult (Ropp n) (Rinv d)) with (Ropp (Rmult n (Rinv d))).
Apply Rlt_Ropp.
Try Exact H.
Ring.
Ring.
Qed.
Lemma Rnot_lt_lt: (x, y : R) ~ (Rlt R0 (Rminus y x)) -> ~ (Rlt x y).
Unfold not; Intros.
Apply H.
Apply Rlt_anti_compatibility with x.
Replace (Rplus x R0) with x.
Replace (Rplus x (Rminus y x)) with y.
Try Exact H0.
Ring.
Ring.
Qed.
Lemma Rnot_le_le: (x, y : R) ~ (Rle R0 (Rminus y x)) -> ~ (Rle x y).
Unfold not; Intros.
Apply H.
Case H0; Intros.
Left.
Apply Rlt_anti_compatibility with x.
Replace (Rplus x R0) with x.
Replace (Rplus x (Rminus y x)) with y.
Try Exact H1.
Ring.
Ring.
Right.
Rewrite H1; Ring.
Qed.
Lemma Rfourier_gt_to_lt: (x, y : R) (Rgt y x) -> (Rlt x y).
Unfold Rgt; Auto with *.
Qed.
Lemma Rfourier_ge_to_le: (x, y : R) (Rge y x) -> (Rle x y).
Unfold Rge Rle; Intuition.
Qed.
Lemma Rfourier_eqLR_to_le: (x, y : R) x == y -> (Rle x y).
Intros.
Rewrite H; Red.
Right; Auto with *.
Qed.
Lemma Rfourier_eqRL_to_le: (x, y : R) y == x -> (Rle x y).
Intros.
Rewrite H; Red.
Right; Auto with *.
Qed.
Lemma Rfourier_not_ge_lt: (x, y : R) ((Rge x y) -> False) -> (Rlt x y).
Intros.
Unfold Rge in H.
Elim (total_order x y); Intros.
Try Exact H0.
Intuition.
Qed.
Lemma Rfourier_not_gt_le: (x, y : R) ((Rgt x y) -> False) -> (Rle x y).
Intros.
Red.
Elim (total_order x y); Intros.
Intuition.
Intuition.
Qed.
Lemma Rfourier_not_le_gt: (x, y : R) ((Rle x y) -> False) -> (Rgt x y).
Unfold Rle.
Intros.
Red.
Elim (total_order x y); Intros.
Intuition.
Intuition.
Qed.
Lemma Rfourier_not_lt_ge: (x, y : R) ((Rlt x y) -> False) -> (Rge x y).
Intros.
Red.
Elim (total_order x y); Intros.
Intuition.
Intuition.
Qed.
|
