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
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(** Power Function *)
Require Import NZAxioms NZMulOrder.
(** Interface of a power function, then its specification on naturals *)
Module Type Pow (Import T:Typ).
Parameters Inline pow : t -> t -> t.
End Pow.
Module Type PowNotation (T:Typ)(Import NZ:Pow T).
Infix "^" := pow.
End PowNotation.
Module Type Pow' (T:Typ) := Pow T <+ PowNotation T.
Module Type NZPowSpec (Import NZ : NZOrdAxiomsSig')(Import P : Pow' NZ).
Declare Instance pow_wd : Proper (eq==>eq==>eq) pow.
Axiom pow_0_r : forall a, a^0 == 1.
Axiom pow_succ_r : forall a b, 0<=b -> a^(succ b) == a * a^b.
End NZPowSpec.
Module Type NZPow (NZ:NZOrdAxiomsSig) := Pow NZ <+ NZPowSpec NZ.
Module Type NZPow' (NZ:NZOrdAxiomsSig) := Pow' NZ <+ NZPowSpec NZ.
(** Derived properties of power *)
Module NZPowProp
(Import NZ : NZOrdAxiomsSig')
(Import NZP : NZMulOrderProp NZ)
(Import NZP' : NZPow' NZ).
Hint Rewrite pow_0_r pow_succ_r : nz.
Lemma lt_0_2 : 0 < 2.
Proof.
apply lt_succ_r, le_0_1.
Qed.
Ltac order' := generalize lt_0_1 lt_0_2; order.
(** Power and basic constants *)
Lemma pow_0_l : forall a, 0<a -> 0^a == 0.
Proof.
intros a Ha.
destruct (lt_exists_pred _ _ Ha) as (a' & EQ & Ha').
rewrite EQ. now nzsimpl.
Qed.
Lemma pow_1_r : forall a, a^1 == a.
Proof.
intros. now nzsimpl.
Qed.
Lemma pow_1_l : forall a, 0<=a -> 1^a == 1.
Proof.
apply le_ind; intros. solve_predicate_wd.
now nzsimpl.
now nzsimpl.
Qed.
Hint Rewrite pow_1_l : nz.
Lemma pow_2_r : forall a, a^2 == a*a.
Proof.
intros. nzsimpl; order'.
Qed.
(** Power and addition, multiplication *)
Lemma pow_add_r : forall a b c, 0<=b -> 0<=c ->
a^(b+c) == a^b * a^c.
Proof.
intros a b c Hb. apply le_ind with (4:=Hb). solve_predicate_wd.
now nzsimpl.
clear b Hb. intros b Hb IH Hc.
nzsimpl; trivial.
rewrite IH; trivial. apply mul_assoc.
now apply add_nonneg_nonneg.
Qed.
Lemma pow_mul_l : forall a b c, 0<=c ->
(a*b)^c == a^c * b^c.
Proof.
intros a b c Hc. apply le_ind with (4:=Hc). solve_predicate_wd.
now nzsimpl.
clear c Hc. intros c Hc IH.
nzsimpl; trivial.
rewrite IH; trivial. apply mul_shuffle1.
Qed.
Lemma pow_mul_r : forall a b c, 0<=b -> 0<=c ->
a^(b*c) == (a^b)^c.
Proof.
intros a b c Hb. apply le_ind with (4:=Hb). solve_predicate_wd.
intros. now nzsimpl.
clear b Hb. intros b Hb IH Hc.
nzsimpl; trivial.
rewrite pow_add_r, IH, pow_mul_l; trivial. apply mul_comm.
now apply mul_nonneg_nonneg.
Qed.
(** Positivity *)
Lemma pow_nonneg_nonneg : forall a b, 0<=a -> 0<=b -> 0<=a^b.
Proof.
intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd.
nzsimpl; order'.
clear b Hb. intros b Hb IH.
nzsimpl; trivial. now apply mul_nonneg_nonneg.
Qed.
Lemma pow_pos_nonneg : forall a b, 0<a -> 0<=b -> 0<a^b.
Proof.
intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd.
nzsimpl; order'.
clear b Hb. intros b Hb IH.
nzsimpl; trivial. now apply mul_pos_pos.
Qed.
(** Monotonicity *)
Lemma pow_lt_mono_l : forall a b c, 0<c -> 0<=a<b -> a^c < b^c.
Proof.
intros a b c Hc. apply lt_ind with (4:=Hc). solve_predicate_wd.
intros (Ha,H). nzsimpl; trivial; order.
clear c Hc. intros c Hc IH (Ha,H).
nzsimpl; try order.
apply mul_lt_mono_nonneg; trivial.
apply pow_nonneg_nonneg; try order.
apply IH. now split.
Qed.
Lemma pow_le_mono_l : forall a b c, 0<=c -> 0<=a<=b -> a^c <= b^c.
Proof.
intros a b c Hc (Ha,H).
apply lt_eq_cases in Hc; destruct Hc as [Hc|Hc]; [|rewrite <- Hc].
apply lt_eq_cases in H. destruct H as [H|H]; [|now rewrite <- H].
apply lt_le_incl, pow_lt_mono_l; now try split.
now nzsimpl.
Qed.
Lemma pow_gt_1 : forall a b, 1<a -> 0<b -> 1<a^b.
Proof.
intros a b Ha Hb. rewrite <- (pow_1_l b) by order.
apply pow_lt_mono_l; try split; order'.
Qed.
Lemma pow_lt_mono_r : forall a b c, 1<a -> 0<=b<c -> a^b < a^c.
Proof.
intros a b c Ha (Hb,H).
assert (H' : b<=c) by order.
destruct (le_exists_sub _ _ H') as (d & EQ & Hd).
rewrite EQ, pow_add_r; trivial. rewrite <- (mul_1_l (a^b)) at 1.
apply mul_lt_mono_pos_r.
apply pow_pos_nonneg; order'.
apply pow_gt_1; trivial.
apply lt_eq_cases in Hd; destruct Hd as [LT|EQ']; trivial.
rewrite <- EQ' in *. rewrite add_0_l in EQ. order.
Qed.
(** NB: since 0^0 > 0^1, the following result isn't valid with a=0 *)
Lemma pow_le_mono_r : forall a b c, 0<a -> 0<=b<=c -> a^b <= a^c.
Proof.
intros a b c Ha (Hb,H).
apply le_succ_l in Ha.
apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha].
apply lt_eq_cases in H; destruct H as [H|H]; [|now rewrite <- H].
apply lt_le_incl, pow_lt_mono_r; now try split.
nzsimpl; order.
Qed.
Lemma pow_le_mono : forall a b c d, 0<a<=c -> 0<=b<=d ->
a^b <= c^d.
Proof.
intros. transitivity (a^d).
apply pow_le_mono_r; intuition order.
apply pow_le_mono_l; intuition order.
Qed.
Lemma pow_lt_mono : forall a b c d, 0<a<c -> 0<b<d ->
a^b < c^d.
Proof.
intros a b c d (Ha,Hac) (Hb,Hbd).
apply le_succ_l in Ha.
apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha].
transitivity (a^d).
apply pow_lt_mono_r; intuition order.
apply pow_lt_mono_l; try split; order'.
nzsimpl; try order. apply pow_gt_1; order.
Qed.
(** Injectivity *)
Lemma pow_inj_l : forall a b c, 0<=a -> 0<=b -> 0<c ->
a^c == b^c -> a == b.
Proof.
intros a b c Ha Hb Hc EQ.
destruct (lt_trichotomy a b) as [LT|[EQ'|GT]]; trivial.
assert (a^c < b^c) by (apply pow_lt_mono_l; try split; trivial).
order.
assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial).
order.
Qed.
Lemma pow_inj_r : forall a b c, 1<a -> 0<=b -> 0<=c ->
a^b == a^c -> b == c.
Proof.
intros a b c Ha Hb Hc EQ.
destruct (lt_trichotomy b c) as [LT|[EQ'|GT]]; trivial.
assert (a^b < a^c) by (apply pow_lt_mono_r; try split; trivial).
order.
assert (a^c < a^b) by (apply pow_lt_mono_r; try split; trivial).
order.
Qed.
(** Monotonicity results, both ways *)
Lemma pow_lt_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c ->
(a<b <-> a^c < b^c).
Proof.
intros a b c Ha Hb Hc.
split; intro LT.
apply pow_lt_mono_l; try split; trivial.
destruct (le_gt_cases b a) as [LE|GT]; trivial.
assert (b^c <= a^c) by (apply pow_le_mono_l; try split; order).
order.
Qed.
Lemma pow_le_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c ->
(a<=b <-> a^c <= b^c).
Proof.
intros a b c Ha Hb Hc.
split; intro LE.
apply pow_le_mono_l; try split; trivial. order.
destruct (le_gt_cases a b) as [LE'|GT]; trivial.
assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial).
order.
Qed.
Lemma pow_lt_mono_r_iff : forall a b c, 1<a -> 0<=b -> 0<=c ->
(b<c <-> a^b < a^c).
Proof.
intros a b c Ha Hb Hc.
split; intro LT.
apply pow_lt_mono_r; try split; trivial.
destruct (le_gt_cases c b) as [LE|GT]; trivial.
assert (a^c <= a^b) by (apply pow_le_mono_r; try split; order').
order.
Qed.
Lemma pow_le_mono_r_iff : forall a b c, 1<a -> 0<=b -> 0<=c ->
(b<=c <-> a^b <= a^c).
Proof.
intros a b c Ha Hb Hc.
split; intro LE.
apply pow_le_mono_r; try split; trivial. order'.
destruct (le_gt_cases b c) as [LE'|GT]; trivial.
assert (a^c < a^b) by (apply pow_lt_mono_r; try split; order').
order.
Qed.
(** For any a>1, the a^x function is above the identity function *)
Lemma pow_gt_lin_r : forall a b, 1<a -> 0<=b -> b < a^b.
Proof.
intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd.
nzsimpl. order'.
clear b Hb. intros b Hb IH. nzsimpl; trivial.
rewrite <- !le_succ_l in *.
transitivity (2*(S b)).
nzsimpl. rewrite <- 2 succ_le_mono.
rewrite <- (add_0_l b) at 1. apply add_le_mono; order.
apply mul_le_mono_nonneg; trivial.
order'.
now apply lt_le_incl, lt_succ_r.
Qed.
(** Someday, we should say something about the full Newton formula.
In the meantime, we can at least provide some inequalities about
(a+b)^c.
*)
Lemma pow_add_lower : forall a b c, 0<=a -> 0<=b -> 0<c ->
a^c + b^c <= (a+b)^c.
Proof.
intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_predicate_wd.
nzsimpl; order.
clear c Hc. intros c Hc IH.
assert (0<=c) by order'.
nzsimpl; trivial.
transitivity ((a+b)*(a^c + b^c)).
rewrite mul_add_distr_r, !mul_add_distr_l.
apply add_le_mono.
rewrite <- add_0_r at 1. apply add_le_mono_l.
apply mul_nonneg_nonneg; trivial.
apply pow_nonneg_nonneg; trivial.
rewrite <- add_0_l at 1. apply add_le_mono_r.
apply mul_nonneg_nonneg; trivial.
apply pow_nonneg_nonneg; trivial.
apply mul_le_mono_nonneg_l; trivial.
now apply add_nonneg_nonneg.
Qed.
(** This upper bound can also be seen as a convexity proof for x^c :
image of (a+b)/2 is below the middle of the images of a and b
*)
Lemma pow_add_upper : forall a b c, 0<=a -> 0<=b -> 0<c ->
(a+b)^c <= 2^(pred c) * (a^c + b^c).
Proof.
assert (aux : forall a b c, 0<=a<=b -> 0<c ->
(a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)).
(* begin *)
intros a b c (Ha,H) Hc.
rewrite !mul_add_distr_l, !mul_add_distr_r. nzsimpl.
rewrite <- !add_assoc. apply add_le_mono_l.
rewrite !add_assoc. apply add_le_mono_r.
destruct (le_exists_sub _ _ H) as (d & EQ & Hd).
rewrite EQ.
rewrite 2 mul_add_distr_r.
rewrite !add_assoc. apply add_le_mono_r.
rewrite add_comm. apply add_le_mono_l.
apply mul_le_mono_nonneg_l; trivial.
apply pow_le_mono_l; try split; order.
(* end *)
intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_predicate_wd.
nzsimpl; order.
clear c Hc. intros c Hc IH.
assert (0<=c) by order.
nzsimpl; trivial.
transitivity ((a+b)*(2^(pred c) * (a^c + b^c))).
apply mul_le_mono_nonneg_l; trivial.
now apply add_nonneg_nonneg.
rewrite mul_assoc. rewrite (mul_comm (a+b)).
assert (EQ : S (P c) == c) by (apply lt_succ_pred with 0; order').
assert (LE : 0 <= P c) by (now rewrite succ_le_mono, EQ, le_succ_l).
assert (EQ' : 2^c == 2^(P c) * 2) by (rewrite <- EQ at 1; nzsimpl; order).
rewrite EQ', <- !mul_assoc.
apply mul_le_mono_nonneg_l.
apply pow_nonneg_nonneg; order'.
destruct (le_gt_cases a b).
apply aux; try split; order'.
rewrite (add_comm a), (add_comm (a^c)), (add_comm (a*a^c)).
apply aux; try split; order'.
Qed.
End NZPowProp.
|
