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
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(** Properties of the power function *)
Require Import Bool ZAxioms ZMulOrder ZParity ZSgnAbs NZPow.
Module Type ZPowProp
(Import A : ZAxiomsSig')
(Import B : ZMulOrderProp A)
(Import C : ZParityProp A B)
(Import D : ZSgnAbsProp A B).
Include NZPowProp A A B.
(** Parity of power *)
Lemma even_pow : forall a b, 0<b -> even (a^b) = even a.
Proof.
intros a b Hb. apply lt_ind with (4:=Hb). solve_proper.
now nzsimpl.
clear b Hb. intros b Hb IH. nzsimpl; [|order].
rewrite even_mul, IH. now destruct (even a).
Qed.
Lemma odd_pow : forall a b, 0<b -> odd (a^b) = odd a.
Proof.
intros. now rewrite <- !negb_even, even_pow.
Qed.
(** Properties of power of negative numbers *)
Lemma pow_opp_even : forall a b, Even b -> (-a)^b == a^b.
Proof.
intros a b (c,H). rewrite H.
destruct (le_gt_cases 0 c).
rewrite 2 pow_mul_r by order'.
rewrite 2 pow_2_r.
now rewrite mul_opp_opp.
assert (2*c < 0) by (apply mul_pos_neg; order').
now rewrite !pow_neg_r.
Qed.
Lemma pow_opp_odd : forall a b, Odd b -> (-a)^b == -(a^b).
Proof.
intros a b (c,H). rewrite H.
destruct (le_gt_cases 0 c) as [LE|GT].
assert (0 <= 2*c) by (apply mul_nonneg_nonneg; order').
rewrite add_1_r, !pow_succ_r; trivial.
rewrite pow_opp_even by (now exists c).
apply mul_opp_l.
apply double_above in GT. rewrite mul_0_r in GT.
rewrite !pow_neg_r by trivial. now rewrite opp_0.
Qed.
Lemma pow_even_abs : forall a b, Even b -> a^b == (abs a)^b.
Proof.
intros. destruct (abs_eq_or_opp a) as [EQ|EQ]; rewrite EQ.
reflexivity.
symmetry. now apply pow_opp_even.
Qed.
Lemma pow_even_nonneg : forall a b, Even b -> 0 <= a^b.
Proof.
intros. rewrite pow_even_abs by trivial.
apply pow_nonneg, abs_nonneg.
Qed.
Lemma pow_odd_abs_sgn : forall a b, Odd b -> a^b == sgn a * (abs a)^b.
Proof.
intros a b H.
destruct (sgn_spec a) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ.
nzsimpl.
rewrite abs_eq; order.
rewrite <- EQ'. nzsimpl.
destruct (le_gt_cases 0 b).
apply pow_0_l.
assert (b~=0) by (contradict H; now rewrite H, <-odd_spec, odd_0).
order.
now rewrite pow_neg_r.
rewrite abs_neq by order.
rewrite pow_opp_odd; trivial.
now rewrite mul_opp_opp, mul_1_l.
Qed.
Lemma pow_odd_sgn : forall a b, 0<=b -> Odd b -> sgn (a^b) == sgn a.
Proof.
intros a b Hb H.
destruct (sgn_spec a) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ.
apply sgn_pos. apply pow_pos_nonneg; trivial.
rewrite <- EQ'. rewrite pow_0_l. apply sgn_0.
assert (b~=0) by (contradict H; now rewrite H, <-odd_spec, odd_0).
order.
apply sgn_neg.
rewrite <- (opp_involutive a). rewrite pow_opp_odd by trivial.
apply opp_neg_pos.
apply pow_pos_nonneg; trivial.
now apply opp_pos_neg.
Qed.
Lemma abs_pow : forall a b, abs (a^b) == (abs a)^b.
Proof.
intros a b.
destruct (Even_or_Odd b).
rewrite pow_even_abs by trivial.
apply abs_eq, pow_nonneg, abs_nonneg.
rewrite pow_odd_abs_sgn by trivial.
rewrite abs_mul.
destruct (lt_trichotomy 0 a) as [Ha|[Ha|Ha]].
rewrite (sgn_pos a), (abs_eq 1), mul_1_l by order'.
apply abs_eq, pow_nonneg, abs_nonneg.
rewrite <- Ha, sgn_0, abs_0, mul_0_l.
symmetry. apply pow_0_l'. intro Hb. rewrite Hb in H.
apply (Even_Odd_False 0); trivial. exists 0; now nzsimpl.
rewrite (sgn_neg a), abs_opp, (abs_eq 1), mul_1_l by order'.
apply abs_eq, pow_nonneg, abs_nonneg.
Qed.
End ZPowProp.
|
