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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: Fourier_util.v,v 1.2.2.1 2004/07/16 19:30:17 herbelin Exp $ *)
Require Export Rbase.
Comments "Lemmas used by the tactic Fourier".
Open Scope R_scope.
Lemma Rfourier_lt:
(x1, y1, a : R) (Rlt x1 y1) -> (Rlt R0 a) -> (Rlt (Rmult a x1) (Rmult a y1)).
Intros; Apply Rlt_monotony; Assumption.
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.
Apply Rgt_Ropp.
Red.
Exact H0.
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; Intros; Assumption.
Qed.
Lemma Rfourier_ge_to_le: (x, y : R) (Rge y x) -> (Rle x y).
Intros x y; Exact (Rge_le y x).
Qed.
Lemma Rfourier_eqLR_to_le: (x, y : R) x == y -> (Rle x y).
Exact eq_Rle.
Qed.
Lemma Rfourier_eqRL_to_le: (x, y : R) y == x -> (Rle x y).
Exact eq_Rle_sym.
Qed.
Lemma Rfourier_not_ge_lt: (x, y : R) ((Rge x y) -> False) -> (Rlt x y).
Exact not_Rge.
Qed.
Lemma Rfourier_not_gt_le: (x, y : R) ((Rgt x y) -> False) -> (Rle x y).
Exact Rgt_not_le.
Qed.
Lemma Rfourier_not_le_gt: (x, y : R) ((Rle x y) -> False) -> (Rgt x y).
Exact not_Rle.
Qed.
Lemma Rfourier_not_lt_ge: (x, y : R) ((Rlt x y) -> False) -> (Rge x y).
Exact Rlt_not_ge.
Qed.
|
