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
|
(************************************************************************)
(* 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 *)
(************************************************************************)
Require Import BinInt BinNat Ring_theory.
Local Open Scope Z_scope.
(** [Zpower_pos z n] is the n-th power of [z] when [n] is an binary
integer (type [positive]) and [z] a signed integer (type [Z]) *)
Definition Zpower_pos (z:Z) (n:positive) :=
iter_pos n Z (fun x:Z => z * x) 1.
Definition Zpower (x y:Z) :=
match y with
| Zpos p => Zpower_pos x p
| Z0 => 1
| Zneg p => 0
end.
Infix "^" := Zpower : Z_scope.
Lemma Zpower_0_r : forall n, n^0 = 1.
Proof. reflexivity. Qed.
Lemma Zpower_succ_r : forall a b, 0<=b -> a^(Zsucc b) = a * a^b.
Proof.
intros a [|b|b] Hb; [ | |now elim Hb]; simpl.
reflexivity.
unfold Zpower_pos. now rewrite Pplus_comm, iter_pos_plus.
Qed.
Lemma Zpower_neg_r : forall a b, b<0 -> a^b = 0.
Proof.
now destruct b.
Qed.
Lemma Zpower_theory : power_theory 1 Zmult (eq (A:=Z)) Z_of_N Zpower.
Proof.
constructor. intros.
destruct n;simpl;trivial.
unfold Zpower_pos.
rewrite <- (Zmult_1_r (pow_pos _ _ _)). generalize 1.
induction p; simpl; intros; rewrite ?IHp, ?Zmult_assoc; trivial.
Qed.
Lemma Zpower_Ppow : forall p q, (Zpos p)^(Zpos q) = Zpos (p^q).
Proof.
intros. unfold Ppow, Zpower, Zpower_pos.
symmetry. now apply iter_pos_swap_gen.
Qed.
Lemma Zpower_Npow : forall n m,
(Z_of_N n)^(Z_of_N m) = Z_of_N (n^m).
Proof.
intros [|n] [|m]; simpl; trivial.
unfold Zpower_pos. generalize 1. induction m; simpl; trivial.
apply Zpower_Ppow.
Qed.
(** An alternative Zpower *)
(** This Zpower_alt is extensionnaly equal to Zpower in ZArith,
but not convertible with it. The number of
multiplications is logarithmic instead of linear, but
these multiplications are bigger. Experimentally, it seems
that Zpower_alt is slightly quicker than Zpower on average,
but can be quite slower on powers of 2.
*)
Definition Zpower_alt n m :=
match m with
| Z0 => 1
| Zpos p => Piter_op Zmult p n
| Zneg p => 0
end.
Infix "^^" := Zpower_alt (at level 30, right associativity) : Z_scope.
Lemma iter_pos_mult_acc : forall f,
(forall x y:Z, (f x)*y = f (x*y)) ->
forall p k, iter_pos p _ f k = (iter_pos p _ f 1)*k.
Proof.
intros f Hf.
induction p; simpl; intros.
rewrite IHp. rewrite Hf. f_equal. rewrite (IHp (iter_pos _ _ _ _)).
rewrite <- Zmult_assoc. f_equal. auto.
rewrite IHp. rewrite (IHp (iter_pos _ _ _ _)).
rewrite <- Zmult_assoc. f_equal. auto.
rewrite Hf. f_equal. now rewrite Zmult_1_l.
Qed.
Lemma Piter_op_square : forall p a,
Piter_op Zmult p (a*a) = (Piter_op Zmult p a)*(Piter_op Zmult p a).
Proof.
induction p; simpl; intros; trivial.
rewrite IHp. rewrite <- !Zmult_assoc. f_equal.
rewrite Zmult_comm, <- Zmult_assoc.
f_equal. apply Zmult_comm.
Qed.
Lemma Zpower_equiv : forall a b, a^^b = a^b.
Proof.
intros a [|p|p]; trivial.
unfold Zpower_alt, Zpower, Zpower_pos.
revert a.
induction p; simpl; intros.
f_equal.
rewrite iter_pos_mult_acc.
now rewrite Piter_op_square, IHp.
intros. symmetry; apply Zmult_assoc.
rewrite iter_pos_mult_acc.
now rewrite Piter_op_square, IHp.
intros. symmetry; apply Zmult_assoc.
now rewrite Zmult_1_r.
Qed.
Lemma Zpower_alt_0_r : forall n, n^^0 = 1.
Proof. reflexivity. Qed.
Lemma Zpower_alt_succ_r : forall a b, 0<=b -> a^^(Zsucc b) = a * a^^b.
Proof.
intros a [|b|b] Hb; [ | |now elim Hb]; simpl.
now rewrite Zmult_1_r.
rewrite <- Pplus_one_succ_r. apply Piter_op_succ. apply Zmult_assoc.
Qed.
Lemma Zpower_alt_neg_r : forall a b, b<0 -> a^^b = 0.
Proof.
now destruct b.
Qed.
Lemma Zpower_alt_Ppow : forall p q, (Zpos p)^^(Zpos q) = Zpos (p^q).
Proof.
intros. now rewrite Zpower_equiv, Zpower_Ppow.
Qed.
|
