← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Numbers/NatInt/NZMulOrder.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:
theories/Numbers/NatInt/NZMulOrder.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
(*                      Evgeny Makarov, INRIA, 2007                     *)
 
9
(************************************************************************)
 
10
 
 
11
(*i $Id: NZMulOrder.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
 
12
 
 
13
Require Import NZAxioms.
 
14
Require Import NZAddOrder.
 
15
 
 
16
Module NZMulOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig).
 
17
Module Export NZAddOrderPropMod := NZAddOrderPropFunct NZOrdAxiomsMod.
 
18
Open Local Scope NatIntScope.
 
19
 
 
20
Theorem NZmul_lt_pred :
 
21
  forall p q n m : NZ, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
 
22
Proof.
 
23
intros p q n m H. rewrite <- H. do 2 rewrite NZmul_succ_l.
 
24
rewrite <- (NZadd_assoc (p * n) n m).
 
25
rewrite <- (NZadd_assoc (p * m) m n).
 
26
rewrite (NZadd_comm n m). now rewrite <- NZadd_lt_mono_r.
 
27
Qed.
 
28
 
 
29
Theorem NZmul_lt_mono_pos_l : forall p n m : NZ, 0 < p -> (n < m <-> p * n < p * m).
 
30
Proof.
 
31
NZord_induct p.
 
32
intros n m H; false_hyp H NZlt_irrefl.
 
33
intros p H IH n m H1. do 2 rewrite NZmul_succ_l.
 
34
le_elim H. assert (LR : forall n m : NZ, n < m -> p * n + n < p * m + m).
 
35
intros n1 m1 H2. apply NZadd_lt_mono; [now apply -> IH | assumption].
 
36
split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3.
 
37
apply <- NZle_ngt in H3. le_elim H3.
 
38
apply NZlt_asymm in H2. apply H2. now apply LR.
 
39
rewrite H3 in H2; false_hyp H2 NZlt_irrefl.
 
40
rewrite <- H; do 2 rewrite NZmul_0_l; now do 2 rewrite NZadd_0_l.
 
41
intros p H1 _ n m H2. apply NZlt_asymm in H1. false_hyp H2 H1.
 
42
Qed.
 
43
 
 
44
Theorem NZmul_lt_mono_pos_r : forall p n m : NZ, 0 < p -> (n < m <-> n * p < m * p).
 
45
Proof.
 
46
intros p n m.
 
47
rewrite (NZmul_comm n p); rewrite (NZmul_comm m p). now apply NZmul_lt_mono_pos_l.
 
48
Qed.
 
49
 
 
50
Theorem NZmul_lt_mono_neg_l : forall p n m : NZ, p < 0 -> (n < m <-> p * m < p * n).
 
51
Proof.
 
52
NZord_induct p.
 
53
intros n m H; false_hyp H NZlt_irrefl.
 
54
intros p H1 _ n m H2. apply NZlt_succ_l in H2. apply <- NZnle_gt in H2. false_hyp H1 H2.
 
55
intros p H IH n m H1. apply <- NZle_succ_l in H.
 
56
le_elim H. assert (LR : forall n m : NZ, n < m -> p * m < p * n).
 
57
intros n1 m1 H2. apply (NZle_lt_add_lt n1 m1).
 
58
now apply NZlt_le_incl. do 2 rewrite <- NZmul_succ_l. now apply -> IH.
 
59
split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3.
 
60
apply <- NZle_ngt in H3. le_elim H3.
 
61
apply NZlt_asymm in H2. apply H2. now apply LR.
 
62
rewrite H3 in H2; false_hyp H2 NZlt_irrefl.
 
63
rewrite (NZmul_lt_pred p (S p)) by reflexivity.
 
64
rewrite H; do 2 rewrite NZmul_0_l; now do 2 rewrite NZadd_0_l.
 
65
Qed.
 
66
 
 
67
Theorem NZmul_lt_mono_neg_r : forall p n m : NZ, p < 0 -> (n < m <-> m * p < n * p).
 
68
Proof.
 
69
intros p n m.
 
70
rewrite (NZmul_comm n p); rewrite (NZmul_comm m p). now apply NZmul_lt_mono_neg_l.
 
71
Qed.
 
72
 
 
73
Theorem NZmul_le_mono_nonneg_l : forall n m p : NZ, 0 <= p -> n <= m -> p * n <= p * m.
 
74
Proof.
 
75
intros n m p H1 H2. le_elim H1.
 
76
le_elim H2. apply NZlt_le_incl. now apply -> NZmul_lt_mono_pos_l.
 
77
apply NZeq_le_incl; now rewrite H2.
 
78
apply NZeq_le_incl; rewrite <- H1; now do 2 rewrite NZmul_0_l.
 
79
Qed.
 
80
 
 
81
Theorem NZmul_le_mono_nonpos_l : forall n m p : NZ, p <= 0 -> n <= m -> p * m <= p * n.
 
82
Proof.
 
83
intros n m p H1 H2. le_elim H1.
 
84
le_elim H2. apply NZlt_le_incl. now apply -> NZmul_lt_mono_neg_l.
 
85
apply NZeq_le_incl; now rewrite H2.
 
86
apply NZeq_le_incl; rewrite H1; now do 2 rewrite NZmul_0_l.
 
87
Qed.
 
88
 
 
89
Theorem NZmul_le_mono_nonneg_r : forall n m p : NZ, 0 <= p -> n <= m -> n * p <= m * p.
 
90
Proof.
 
91
intros n m p H1 H2; rewrite (NZmul_comm n p); rewrite (NZmul_comm m p);
 
92
now apply NZmul_le_mono_nonneg_l.
 
93
Qed.
 
94
 
 
95
Theorem NZmul_le_mono_nonpos_r : forall n m p : NZ, p <= 0 -> n <= m -> m * p <= n * p.
 
96
Proof.
 
97
intros n m p H1 H2; rewrite (NZmul_comm n p); rewrite (NZmul_comm m p);
 
98
now apply NZmul_le_mono_nonpos_l.
 
99
Qed.
 
100
 
 
101
Theorem NZmul_cancel_l : forall n m p : NZ, p ~= 0 -> (p * n == p * m <-> n == m).
 
102
Proof.
 
103
intros n m p H; split; intro H1.
 
104
destruct (NZlt_trichotomy p 0) as [H2 | [H2 | H2]].
 
105
apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3].
 
106
assert (H4 : p * m < p * n); [now apply -> NZmul_lt_mono_neg_l |].
 
107
rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
 
108
assert (H4 : p * n < p * m); [now apply -> NZmul_lt_mono_neg_l |].
 
109
rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
 
110
false_hyp H2 H.
 
111
apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3].
 
112
assert (H4 : p * n < p * m) by (now apply -> NZmul_lt_mono_pos_l).
 
113
rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
 
114
assert (H4 : p * m < p * n) by (now apply -> NZmul_lt_mono_pos_l).
 
115
rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
 
116
now rewrite H1.
 
117
Qed.
 
118
 
 
119
Theorem NZmul_cancel_r : forall n m p : NZ, p ~= 0 -> (n * p == m * p <-> n == m).
 
120
Proof.
 
121
intros n m p. rewrite (NZmul_comm n p), (NZmul_comm m p); apply NZmul_cancel_l.
 
122
Qed.
 
123
 
 
124
Theorem NZmul_id_l : forall n m : NZ, m ~= 0 -> (n * m == m <-> n == 1).
 
125
Proof.
 
126
intros n m H.
 
127
stepl (n * m == 1 * m) by now rewrite NZmul_1_l. now apply NZmul_cancel_r.
 
128
Qed.
 
129
 
 
130
Theorem NZmul_id_r : forall n m : NZ, n ~= 0 -> (n * m == n <-> m == 1).
 
131
Proof.
 
132
intros n m; rewrite NZmul_comm; apply NZmul_id_l.
 
133
Qed.
 
134
 
 
135
Theorem NZmul_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m).
 
136
Proof.
 
137
intros n m p H; do 2 rewrite NZlt_eq_cases.
 
138
rewrite (NZmul_lt_mono_pos_l p n m) by assumption.
 
139
now rewrite -> (NZmul_cancel_l n m p) by
 
140
(intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl).
 
141
Qed.
 
142
 
 
143
Theorem NZmul_le_mono_pos_r : forall n m p : NZ, 0 < p -> (n <= m <-> n * p <= m * p).
 
144
Proof.
 
145
intros n m p. rewrite (NZmul_comm n p); rewrite (NZmul_comm m p);
 
146
apply NZmul_le_mono_pos_l.
 
147
Qed.
 
148
 
 
149
Theorem NZmul_le_mono_neg_l : forall n m p : NZ, p < 0 -> (n <= m <-> p * m <= p * n).
 
150
Proof.
 
151
intros n m p H; do 2 rewrite NZlt_eq_cases.
 
152
rewrite (NZmul_lt_mono_neg_l p n m); [| assumption].
 
153
rewrite -> (NZmul_cancel_l m n p) by (intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl).
 
154
now setoid_replace (n == m) with (m == n) using relation iff by (split; now intro).
 
155
Qed.
 
156
 
 
157
Theorem NZmul_le_mono_neg_r : forall n m p : NZ, p < 0 -> (n <= m <-> m * p <= n * p).
 
158
Proof.
 
159
intros n m p. rewrite (NZmul_comm n p); rewrite (NZmul_comm m p);
 
160
apply NZmul_le_mono_neg_l.
 
161
Qed.
 
162
 
 
163
Theorem NZmul_lt_mono_nonneg :
 
164
  forall n m p q : NZ, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q.
 
165
Proof.
 
166
intros n m p q H1 H2 H3 H4.
 
167
apply NZle_lt_trans with (m * p).
 
168
apply NZmul_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl].
 
169
apply -> NZmul_lt_mono_pos_l; [assumption | now apply NZle_lt_trans with n].
 
170
Qed.
 
171
 
 
172
(* There are still many variants of the theorem above. One can assume 0 < n
 
173
or 0 < p or n <= m or p <= q. *)
 
174
 
 
175
Theorem NZmul_le_mono_nonneg :
 
176
  forall n m p q : NZ, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q.
 
177
Proof.
 
178
intros n m p q H1 H2 H3 H4.
 
179
le_elim H2; le_elim H4.
 
180
apply NZlt_le_incl; now apply NZmul_lt_mono_nonneg.
 
181
rewrite <- H4; apply NZmul_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl].
 
182
rewrite <- H2; apply NZmul_le_mono_nonneg_l; [assumption | now apply NZlt_le_incl].
 
183
rewrite H2; rewrite H4; now apply NZeq_le_incl.
 
184
Qed.
 
185
 
 
186
Theorem NZmul_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n * m.
 
187
Proof.
 
188
intros n m H1 H2.
 
189
rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_pos_r.
 
190
Qed.
 
191
 
 
192
Theorem NZmul_neg_neg : forall n m : NZ, n < 0 -> m < 0 -> 0 < n * m.
 
193
Proof.
 
194
intros n m H1 H2.
 
195
rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_neg_r.
 
196
Qed.
 
197
 
 
198
Theorem NZmul_pos_neg : forall n m : NZ, 0 < n -> m < 0 -> n * m < 0.
 
199
Proof.
 
200
intros n m H1 H2.
 
201
rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_neg_r.
 
202
Qed.
 
203
 
 
204
Theorem NZmul_neg_pos : forall n m : NZ, n < 0 -> 0 < m -> n * m < 0.
 
205
Proof.
 
206
intros; rewrite NZmul_comm; now apply NZmul_pos_neg.
 
207
Qed.
 
208
 
 
209
Theorem NZlt_1_mul_pos : forall n m : NZ, 1 < n -> 0 < m -> 1 < n * m.
 
210
Proof.
 
211
intros n m H1 H2. apply -> (NZmul_lt_mono_pos_r m) in H1.
 
212
rewrite NZmul_1_l in H1. now apply NZlt_1_l with m.
 
213
assumption.
 
214
Qed.
 
215
 
 
216
Theorem NZeq_mul_0 : forall n m : NZ, n * m == 0 <-> n == 0 \/ m == 0.
 
217
Proof.
 
218
intros n m; split.
 
219
intro H; destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]];
 
220
destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]];
 
221
try (now right); try (now left).
 
222
elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZmul_neg_neg |].
 
223
elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZmul_neg_pos |].
 
224
elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZmul_pos_neg |].
 
225
elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZmul_pos_pos |].
 
226
intros [H | H]. now rewrite H, NZmul_0_l. now rewrite H, NZmul_0_r.
 
227
Qed.
 
228
 
 
229
Theorem NZneq_mul_0 : forall n m : NZ, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
 
230
Proof.
 
231
intros n m; split; intro H.
 
232
intro H1; apply -> NZeq_mul_0 in H1. tauto.
 
233
split; intro H1; rewrite H1 in H;
 
234
(rewrite NZmul_0_l in H || rewrite NZmul_0_r in H); now apply H.
 
235
Qed.
 
236
 
 
237
Theorem NZeq_square_0 : forall n : NZ, n * n == 0 <-> n == 0.
 
238
Proof.
 
239
intro n; rewrite NZeq_mul_0; tauto.
 
240
Qed.
 
241
 
 
242
Theorem NZeq_mul_0_l : forall n m : NZ, n * m == 0 -> m ~= 0 -> n == 0.
 
243
Proof.
 
244
intros n m H1 H2. apply -> NZeq_mul_0 in H1. destruct H1 as [H1 | H1].
 
245
assumption. false_hyp H1 H2.
 
246
Qed.
 
247
 
 
248
Theorem NZeq_mul_0_r : forall n m : NZ, n * m == 0 -> n ~= 0 -> m == 0.
 
249
Proof.
 
250
intros n m H1 H2; apply -> NZeq_mul_0 in H1. destruct H1 as [H1 | H1].
 
251
false_hyp H1 H2. assumption.
 
252
Qed.
 
253
 
 
254
Theorem NZlt_0_mul : forall n m : NZ, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0).
 
255
Proof.
 
256
intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]].
 
257
destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]];
 
258
[| rewrite H1 in H; rewrite NZmul_0_l in H; false_hyp H NZlt_irrefl |];
 
259
(destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]];
 
260
[| rewrite H2 in H; rewrite NZmul_0_r in H; false_hyp H NZlt_irrefl |]);
 
261
try (left; now split); try (right; now split).
 
262
assert (H3 : n * m < 0) by now apply NZmul_neg_pos.
 
263
elimtype False; now apply (NZlt_asymm (n * m) 0).
 
264
assert (H3 : n * m < 0) by now apply NZmul_pos_neg.
 
265
elimtype False; now apply (NZlt_asymm (n * m) 0).
 
266
now apply NZmul_pos_pos. now apply NZmul_neg_neg.
 
267
Qed.
 
268
 
 
269
Theorem NZsquare_lt_mono_nonneg : forall n m : NZ, 0 <= n -> n < m -> n * n < m * m.
 
270
Proof.
 
271
intros n m H1 H2. now apply NZmul_lt_mono_nonneg.
 
272
Qed.
 
273
 
 
274
Theorem NZsquare_le_mono_nonneg : forall n m : NZ, 0 <= n -> n <= m -> n * n <= m * m.
 
275
Proof.
 
276
intros n m H1 H2. now apply NZmul_le_mono_nonneg.
 
277
Qed.
 
278
 
 
279
(* The converse theorems require nonnegativity (or nonpositivity) of the
 
280
other variable *)
 
281
 
 
282
Theorem NZsquare_lt_simpl_nonneg : forall n m : NZ, 0 <= m -> n * n < m * m -> n < m.
 
283
Proof.
 
284
intros n m H1 H2. destruct (NZlt_ge_cases n 0).
 
285
now apply NZlt_le_trans with 0.
 
286
destruct (NZlt_ge_cases n m).
 
287
assumption. assert (F : m * m <= n * n) by now apply NZsquare_le_mono_nonneg.
 
288
apply -> NZle_ngt in F. false_hyp H2 F.
 
289
Qed.
 
290
 
 
291
Theorem NZsquare_le_simpl_nonneg : forall n m : NZ, 0 <= m -> n * n <= m * m -> n <= m.
 
292
Proof.
 
293
intros n m H1 H2. destruct (NZlt_ge_cases n 0).
 
294
apply NZlt_le_incl; now apply NZlt_le_trans with 0.
 
295
destruct (NZle_gt_cases n m).
 
296
assumption. assert (F : m * m < n * n) by now apply NZsquare_lt_mono_nonneg.
 
297
apply -> NZlt_nge in F. false_hyp H2 F.
 
298
Qed.
 
299
 
 
300
Theorem NZmul_2_mono_l : forall n m : NZ, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
 
301
Proof.
 
302
intros n m H. apply <- NZle_succ_l in H.
 
303
apply -> (NZmul_le_mono_pos_l (S n) m (1 + 1)) in H.
 
304
repeat rewrite NZmul_add_distr_r in *; repeat rewrite NZmul_1_l in *.
 
305
repeat rewrite NZadd_succ_r in *. repeat rewrite NZadd_succ_l in *. rewrite NZadd_0_l.
 
306
now apply -> NZle_succ_l.
 
307
apply NZadd_pos_pos; now apply NZlt_succ_diag_r.
 
308
Qed.
 
309
 
 
310
End NZMulOrderPropFunct.