← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to contrib/fourier/Fourier_util.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
contrib/fourier/Fourier_util.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(* $Id: Fourier_util.v 10710 2008-03-23 09:24:09Z herbelin $ *)
 
10
 
 
11
Require Export Rbase.
 
12
Comments "Lemmas used by the tactic Fourier".
 
13
 
 
14
Open Scope R_scope.
 
15
 
 
16
Lemma Rfourier_lt : forall x1 y1 a:R, x1 < y1 -> 0 < a -> a * x1 < a * y1.
 
17
intros; apply Rmult_lt_compat_l; assumption.
 
18
Qed.
 
19
 
 
20
Lemma Rfourier_le : forall x1 y1 a:R, x1 <= y1 -> 0 < a -> a * x1 <= a * y1.
 
21
red in |- *.
 
22
intros.
 
23
case H; auto with real.
 
24
Qed.
 
25
 
 
26
Lemma Rfourier_lt_lt :
 
27
 forall x1 y1 x2 y2 a:R,
 
28
   x1 < y1 -> x2 < y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2.
 
29
intros x1 y1 x2 y2 a H H0 H1; try assumption.
 
30
apply Rplus_lt_compat.
 
31
try exact H.
 
32
apply Rfourier_lt.
 
33
try exact H0.
 
34
try exact H1.
 
35
Qed.
 
36
 
 
37
Lemma Rfourier_lt_le :
 
38
 forall x1 y1 x2 y2 a:R,
 
39
   x1 < y1 -> x2 <= y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2.
 
40
intros x1 y1 x2 y2 a H H0 H1; try assumption.
 
41
case H0; intros.
 
42
apply Rplus_lt_compat.
 
43
try exact H.
 
44
apply Rfourier_lt; auto with real.
 
45
rewrite H2.
 
46
rewrite (Rplus_comm y1 (a * y2)).
 
47
rewrite (Rplus_comm x1 (a * y2)).
 
48
apply Rplus_lt_compat_l.
 
49
try exact H.
 
50
Qed.
 
51
 
 
52
Lemma Rfourier_le_lt :
 
53
 forall x1 y1 x2 y2 a:R,
 
54
   x1 <= y1 -> x2 < y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2.
 
55
intros x1 y1 x2 y2 a H H0 H1; try assumption.
 
56
case H; intros.
 
57
apply Rfourier_lt_le; auto with real.
 
58
rewrite H2.
 
59
apply Rplus_lt_compat_l.
 
60
apply Rfourier_lt; auto with real.
 
61
Qed.
 
62
 
 
63
Lemma Rfourier_le_le :
 
64
 forall x1 y1 x2 y2 a:R,
 
65
   x1 <= y1 -> x2 <= y2 -> 0 < a -> x1 + a * x2 <= y1 + a * y2.
 
66
intros x1 y1 x2 y2 a H H0 H1; try assumption.
 
67
case H0; intros.
 
68
red in |- *.
 
69
left; try assumption.
 
70
apply Rfourier_le_lt; auto with real.
 
71
rewrite H2.
 
72
case H; intros.
 
73
red in |- *.
 
74
left; try assumption.
 
75
rewrite (Rplus_comm x1 (a * y2)).
 
76
rewrite (Rplus_comm y1 (a * y2)).
 
77
apply Rplus_lt_compat_l.
 
78
try exact H3.
 
79
rewrite H3.
 
80
red in |- *.
 
81
right; try assumption.
 
82
auto with real.
 
83
Qed.
 
84
 
 
85
Lemma Rlt_zero_pos_plus1 : forall x:R, 0 < x -> 0 < 1 + x.
 
86
intros x H; try assumption.
 
87
rewrite Rplus_comm.
 
88
apply Rle_lt_0_plus_1.
 
89
red in |- *; auto with real.
 
90
Qed.
 
91
 
 
92
Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y.
 
93
intros x y H H0; try assumption.
 
94
replace 0 with (x * 0).
 
95
apply Rmult_lt_compat_l; auto with real.
 
96
ring.
 
97
Qed.
 
98
 
 
99
Lemma Rlt_zero_1 : 0 < 1.
 
100
exact Rlt_0_1.
 
101
Qed.
 
102
 
 
103
Lemma Rle_zero_pos_plus1 : forall x:R, 0 <= x -> 0 <= 1 + x.
 
104
intros x H; try assumption.
 
105
case H; intros.
 
106
red in |- *.
 
107
left; try assumption.
 
108
apply Rlt_zero_pos_plus1; auto with real.
 
109
rewrite <- H0.
 
110
replace (1 + 0) with 1.
 
111
red in |- *; left.
 
112
exact Rlt_zero_1.
 
113
ring.
 
114
Qed.
 
115
 
 
116
Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y.
 
117
intros x y H H0; try assumption.
 
118
case H; intros.
 
119
red in |- *; left.
 
120
apply Rlt_mult_inv_pos; auto with real.
 
121
rewrite <- H1.
 
122
red in |- *; right; ring.
 
123
Qed.
 
124
 
 
125
Lemma Rle_zero_1 : 0 <= 1.
 
126
red in |- *; left.
 
127
exact Rlt_zero_1.
 
128
Qed.
 
129
 
 
130
Lemma Rle_not_lt : forall n d:R, 0 <= n * / d -> ~ 0 < - n * / d.
 
131
intros n d H; red in |- *; intros H0; try exact H0.
 
132
generalize (Rgt_not_le 0 (n * / d)).
 
133
intros H1; elim H1; try assumption.
 
134
replace (n * / d) with (- - (n * / d)).
 
135
replace 0 with (- -0).
 
136
replace (- (n * / d)) with (- n * / d).
 
137
replace (-0) with 0.
 
138
red in |- *.
 
139
apply Ropp_gt_lt_contravar.
 
140
red in |- *.
 
141
exact H0.
 
142
ring.
 
143
ring.
 
144
ring.
 
145
ring.
 
146
Qed.
 
147
 
 
148
Lemma Rnot_lt0 : forall x:R, ~ 0 < 0 * x.
 
149
intros x; try assumption.
 
150
replace (0 * x) with 0.
 
151
apply Rlt_irrefl.
 
152
ring.
 
153
Qed.
 
154
 
 
155
Lemma Rlt_not_le_frac_opp : forall n d:R, 0 < n * / d -> ~ 0 <= - n * / d.
 
156
intros n d H; try assumption.
 
157
apply Rgt_not_le.
 
158
replace 0 with (-0).
 
159
replace (- n * / d) with (- (n * / d)).
 
160
apply Ropp_lt_gt_contravar.
 
161
try exact H.
 
162
ring.
 
163
ring.
 
164
Qed.
 
165
 
 
166
Lemma Rnot_lt_lt : forall x y:R, ~ 0 < y - x -> ~ x < y.
 
167
unfold not in |- *; intros.
 
168
apply H.
 
169
apply Rplus_lt_reg_r with x.
 
170
replace (x + 0) with x.
 
171
replace (x + (y - x)) with y.
 
172
try exact H0.
 
173
ring.
 
174
ring.
 
175
Qed.
 
176
 
 
177
Lemma Rnot_le_le : forall x y:R, ~ 0 <= y - x -> ~ x <= y.
 
178
unfold not in |- *; intros.
 
179
apply H.
 
180
case H0; intros.
 
181
left.
 
182
apply Rplus_lt_reg_r with x.
 
183
replace (x + 0) with x.
 
184
replace (x + (y - x)) with y.
 
185
try exact H1.
 
186
ring.
 
187
ring.
 
188
right.
 
189
rewrite H1; ring.
 
190
Qed.
 
191
 
 
192
Lemma Rfourier_gt_to_lt : forall x y:R, y > x -> x < y.
 
193
unfold Rgt in |- *; intros; assumption.
 
194
Qed.
 
195
 
 
196
Lemma Rfourier_ge_to_le : forall x y:R, y >= x -> x <= y.
 
197
intros x y; exact (Rge_le y x).
 
198
Qed.
 
199
 
 
200
Lemma Rfourier_eqLR_to_le : forall x y:R, x = y -> x <= y.
 
201
exact Req_le.
 
202
Qed.
 
203
 
 
204
Lemma Rfourier_eqRL_to_le : forall x y:R, y = x -> x <= y.
 
205
exact Req_le_sym.
 
206
Qed.
 
207
 
 
208
Lemma Rfourier_not_ge_lt : forall x y:R, (x >= y -> False) -> x < y.
 
209
exact Rnot_ge_lt.
 
210
Qed.
 
211
 
 
212
Lemma Rfourier_not_gt_le : forall x y:R, (x > y -> False) -> x <= y.
 
213
exact Rnot_gt_le.
 
214
Qed.
 
215
 
 
216
Lemma Rfourier_not_le_gt : forall x y:R, (x <= y -> False) -> x > y.
 
217
exact Rnot_le_lt.
 
218
Qed.
 
219
 
 
220
Lemma Rfourier_not_lt_ge : forall x y:R, (x < y -> False) -> x >= y.
 
221
exact Rnot_lt_ge.
 
222
Qed.