# Library Coq.ZArith.Zpow_alt

Require Import BinInt.
Local Open Scope Z_scope.
An alternative power function for Z
This Zpower_alt is extensionnaly equal to Z.pow, 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 Z.pow on average, but can be quite slower on powers of 2.
Definition Zpower_alt n m :=
match m with
| Z0 => 1
| Zpos p => Pos.iter_op Z.mul p n
| Zneg p => 0
end.
Infix "^^" := Zpower_alt (at level 30, right associativity) : Z_scope.
Lemma Piter_mul_acc : forall f,
(forall x y:Z, ( f x )* y = f (x * y)) ->
forall p k, Pos.iter p f k = ( Pos.iter p f 1)* k.
Lemma Piter_op_square : forall p a,
Pos.iter_op Z.mul p (a * a) = ( Pos.iter_op Z.mul p a )*( Pos.iter_op Z.mul p a ).
Lemma Zpower_equiv a b : a ^^ b = a ^ b.
Lemma Zpower_alt_0_r n : n ^^0 = 1.
Lemma Zpower_alt_succ_r a b : 0<= b -> a ^^( Z.succ b ) = a * a ^^ b.
Lemma Zpower_alt_neg_r a b : b <0 -> a ^^ b = 0.
Lemma Zpower_alt_Ppow p q : ( Zpos p )^^( Zpos q ) = Zpos (p ^ q).