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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Require Import ZArith_base ZArithRing Zcomplements Zdiv Znumtheory.
Require Export Zpower.
Local Open Scope Z_scope.
(** Properties of the power function over [Z] *)
(** Nota: the usual properties of [Z.pow] are now already provided
by [BinInt.Z]. Only remain here some compatibility elements,
as well as more specific results about power and modulo and/or
primality. *)
Lemma Zpower_pos_1_r x : Z.pow_pos x 1 = x.
Proof (Z.pow_1_r x).
Lemma Zpower_pos_1_l p : Z.pow_pos 1 p = 1.
Proof. now apply (Z.pow_1_l (Zpos p)). Qed.
Lemma Zpower_pos_0_l p : Z.pow_pos 0 p = 0.
Proof. now apply (Z.pow_0_l (Zpos p)). Qed.
Lemma Zpower_pos_pos x p : 0 < x -> 0 < Z.pow_pos x p.
Proof. intros. now apply (Z.pow_pos_nonneg x (Zpos p)). Qed.
Notation Zpower_1_r := Z.pow_1_r (only parsing).
Notation Zpower_1_l := Z.pow_1_l (only parsing).
Notation Zpower_0_l := Z.pow_0_l' (only parsing).
Notation Zpower_0_r := Z.pow_0_r (only parsing).
Notation Zpower_2 := Z.pow_2_r (only parsing).
Notation Zpower_gt_0 := Z.pow_pos_nonneg (only parsing).
Notation Zpower_ge_0 := Z.pow_nonneg (only parsing).
Notation Zpower_Zabs := Z.abs_pow (only parsing).
Notation Zpower_Zsucc := Z.pow_succ_r (only parsing).
Notation Zpower_mult := Z.pow_mul_r (only parsing).
Notation Zpower_le_monotone2 := Z.pow_le_mono_r (only parsing).
Theorem Zpower_le_monotone a b c :
0 < a -> 0 <= b <= c -> a^b <= a^c.
Proof. intros. now apply Z.pow_le_mono_r. Qed.
Theorem Zpower_lt_monotone a b c :
1 < a -> 0 <= b < c -> a^b < a^c.
Proof. intros. apply Z.pow_lt_mono_r; auto with zarith. Qed.
Theorem Zpower_gt_1 x y : 1 < x -> 0 < y -> 1 < x^y.
Proof. apply Z.pow_gt_1. Qed.
Theorem Zmult_power p q r : 0 <= r -> (p*q)^r = p^r * q^r.
Proof. intros. apply Z.pow_mul_l. Qed.
Hint Resolve Z.pow_nonneg Z.pow_pos_nonneg : zarith.
Theorem Zpower_le_monotone3 a b c :
0 <= c -> 0 <= a <= b -> a^c <= b^c.
Proof. intros. now apply Z.pow_le_mono_l. Qed.
Lemma Zpower_le_monotone_inv a b c :
1 < a -> 0 < b -> a^b <= a^c -> b <= c.
Proof.
intros Ha Hb H. apply (Z.pow_le_mono_r_iff a); trivial.
apply Z.lt_le_incl; apply (Z.pow_gt_1 a); trivial.
apply Z.lt_le_trans with (a^b); trivial. now apply Z.pow_gt_1.
Qed.
Notation Zpower_nat_Zpower := Zpower_nat_Zpower (only parsing).
Theorem Zpower2_lt_lin n : 0 <= n -> n < 2^n.
Proof. intros. now apply Z.pow_gt_lin_r. Qed.
Theorem Zpower2_le_lin n : 0 <= n -> n <= 2^n.
Proof. intros. apply Z.lt_le_incl. now apply Z.pow_gt_lin_r. Qed.
Lemma Zpower2_Psize n p :
Zpos p < 2^(Z.of_nat n) <-> (Pos.size_nat p <= n)%nat.
Proof.
revert p; induction n.
destruct p; now split.
assert (Hn := Nat2Z.is_nonneg n).
destruct p; simpl Pos.size_nat.
- specialize IHn with p.
rewrite Pos2Z.inj_xI, Nat2Z.inj_succ, Z.pow_succ_r; omega.
- specialize IHn with p.
rewrite Pos2Z.inj_xO, Nat2Z.inj_succ, Z.pow_succ_r; omega.
- split; auto with zarith.
intros _. apply Z.pow_gt_1. easy.
now rewrite Nat2Z.inj_succ, Z.lt_succ_r.
Qed.
(** * Z.pow and modulo *)
Theorem Zpower_mod p q n :
0 < n -> (p^q) mod n = ((p mod n)^q) mod n.
Proof.
intros Hn; destruct (Z.le_gt_cases 0 q) as [H1|H1].
- pattern q; apply natlike_ind; trivial.
clear q H1. intros q Hq Rec. rewrite !Z.pow_succ_r; trivial.
rewrite Z.mul_mod_idemp_l; auto with zarith.
rewrite Z.mul_mod, Rec, <- Z.mul_mod; auto with zarith.
- rewrite !Z.pow_neg_r; auto with zarith.
Qed.
(** A direct way to compute Z.pow modulo **)
Fixpoint Zpow_mod_pos (a: Z)(m: positive)(n : Z) : Z :=
match m with
| xH => a mod n
| xO m' =>
let z := Zpow_mod_pos a m' n in
match z with
| 0 => 0
| _ => (z * z) mod n
end
| xI m' =>
let z := Zpow_mod_pos a m' n in
match z with
| 0 => 0
| _ => (z * z * a) mod n
end
end.
Definition Zpow_mod a m n :=
match m with
| 0 => 1 mod n
| Zpos p => Zpow_mod_pos a p n
| Zneg p => 0
end.
Theorem Zpow_mod_pos_correct a m n :
n <> 0 -> Zpow_mod_pos a m n = (Z.pow_pos a m) mod n.
Proof.
intros Hn. induction m.
- rewrite Pos.xI_succ_xO at 2. rewrite <- Pos.add_1_r, <- Pos.add_diag.
rewrite 2 Zpower_pos_is_exp, Zpower_pos_1_r.
rewrite Z.mul_mod, (Z.mul_mod (Z.pow_pos a m)) by trivial.
rewrite <- IHm, <- Z.mul_mod by trivial.
simpl. now destruct (Zpow_mod_pos a m n).
- rewrite <- Pos.add_diag at 2.
rewrite Zpower_pos_is_exp.
rewrite Z.mul_mod by trivial.
rewrite <- IHm.
simpl. now destruct (Zpow_mod_pos a m n).
- now rewrite Zpower_pos_1_r.
Qed.
Theorem Zpow_mod_correct a m n :
n <> 0 -> Zpow_mod a m n = (a ^ m) mod n.
Proof.
intros Hn. destruct m; simpl; trivial.
- apply Zpow_mod_pos_correct; auto with zarith.
Qed.
(* Complements about power and number theory. *)
Lemma Zpower_divide p q : 0 < q -> (p | p ^ q).
Proof.
exists (p^(q - 1)).
rewrite Z.mul_comm, <- Z.pow_succ_r; f_equal; auto with zarith.
Qed.
Theorem rel_prime_Zpower_r i p q :
0 <= i -> rel_prime p q -> rel_prime p (q^i).
Proof.
intros Hi Hpq; pattern i; apply natlike_ind; auto with zarith.
simpl. apply rel_prime_sym, rel_prime_1.
clear i Hi. intros i Hi Rec; rewrite Z.pow_succ_r; auto.
apply rel_prime_mult; auto.
Qed.
Theorem rel_prime_Zpower i j p q :
0 <= i -> 0 <= j -> rel_prime p q -> rel_prime (p^i) (q^j).
Proof.
intros Hi Hj H. apply rel_prime_Zpower_r; trivial.
apply rel_prime_sym. apply rel_prime_Zpower_r; trivial.
now apply rel_prime_sym.
Qed.
Theorem prime_power_prime p q n :
0 <= n -> prime p -> prime q -> (p | q^n) -> p = q.
Proof.
intros Hn Hp Hq; pattern n; apply natlike_ind; auto; clear n Hn.
- simpl; intros.
assert (2<=p) by (apply prime_ge_2; auto).
assert (p<=1) by (apply Z.divide_pos_le; auto with zarith).
omega.
- intros n Hn Rec.
rewrite Z.pow_succ_r by trivial. intros.
assert (2<=p) by (apply prime_ge_2; auto).
assert (2<=q) by (apply prime_ge_2; auto).
destruct prime_mult with (2 := H); auto.
apply prime_div_prime; auto.
Qed.
Theorem Zdivide_power_2 x p n :
0 <= n -> 0 <= x -> prime p -> (x | p^n) -> exists m, x = p^m.
Proof.
intros Hn Hx; revert p n Hn. generalize Hx.
pattern x; apply Z_lt_induction; auto.
clear x Hx; intros x IH Hx p n Hn Hp H.
Z.le_elim Hx; subst.
apply Z.le_succ_l in Hx; simpl in Hx.
Z.le_elim Hx; subst.
(* x > 1 *)
case (prime_dec x); intros Hpr.
exists 1; rewrite Z.pow_1_r; apply prime_power_prime with n; auto.
case not_prime_divide with (2 := Hpr); auto.
intros p1 ((Hp1, Hpq1),(q1,->)).
assert (Hq1 : 0 < q1) by (apply Z.mul_lt_mono_pos_r with p1; auto with zarith).
destruct (IH p1) with p n as (r1,Hr1); auto with zarith.
transitivity (q1 * p1); trivial. exists q1; auto with zarith.
destruct (IH q1) with p n as (r2,Hr2); auto with zarith.
split; auto with zarith.
rewrite <- (Z.mul_1_r q1) at 1.
apply Z.mul_lt_mono_pos_l; auto with zarith.
transitivity (q1 * p1); trivial. exists p1; auto with zarith.
exists (r2 + r1); subst.
symmetry. apply Z.pow_add_r.
generalize Hq1; case r2; now auto with zarith.
generalize Hp1; case r1; now auto with zarith.
(* x = 1 *)
exists 0; rewrite Z.pow_0_r; auto.
(* x = 0 *)
exists n; destruct H; rewrite Z.mul_0_r in H; auto.
Qed.
(** * Z.square: a direct definition of [z^2] *)
Notation Psquare := Pos.square (compat "8.7").
Notation Zsquare := Z.square (compat "8.7").
Notation Psquare_correct := Pos.square_spec (only parsing).
Notation Zsquare_correct := Z.square_spec (only parsing).
|
