Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   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 BinInt.
Local Open Scope Z_scope.
An alternative power function for Z
This Zpower_alt is extensionally 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.


forall f : Z -> Z,
(forall x y : Z, f x * y = f (x * y)) ->
forall (p : positive) (k : Z),
Pos.iter f k p = Pos.iter f 1 p * k


forall f : Z -> Z,
(forall x y : Z, f x * y = f (x * y)) ->
forall (p : positive) (k : Z),
Pos.iter f k p = Pos.iter f 1 p * k

 
f:Z -> Z
Hf:forall x y : Z, f x * y = f (x * y)
forall (p : positive) (k : Z),
Pos.iter f k p = Pos.iter f 1 p * k

 
f:Z -> Z
Hf:forall x y : Z, f x * y = f (x * y)
p:positive
IHp:forall k0 : Z, Pos.iter f k0 p = Pos.iter f 1 p * k0
k:Z
f (Pos.iter f (Pos.iter f k p) p) =
f (Pos.iter f (Pos.iter f 1 p) p) * k
f:Z -> Z
Hf:forall x y : Z, f x * y = f (x * y)
p:positive
IHp:forall k0 : Z, Pos.iter f k0 p = Pos.iter f 1 p * k0
k:Z
Pos.iter f (Pos.iter f k p) p =
Pos.iter f (Pos.iter f 1 p) p * k
f:Z -> Z
Hf:forall x y : Z, f x * y = f (x * y)
k:Z
f k = f 1 * k

 
f:Z -> Z
Hf:forall x y : Z, f x * y = f (x * y)
p:positive
IHp:forall k0 : Z, Pos.iter f k0 p = Pos.iter f 1 p * k0
k:Z
f (Pos.iter f (Pos.iter f k p) p) =
f (Pos.iter f (Pos.iter f 1 p) p) * k
 
f:Z -> Z
Hf:forall x y : Z, f x * y = f (x * y)
p:positive
g:=Pos.iter f 1 p:Z
IHp:forall k0 : Z, Pos.iter f k0 p = g * k0
k:Z
f (Pos.iter f (Pos.iter f k p) p) =
f (Pos.iter f g p) * k
 now rewrite !IHp, Hf, Z.mul_assoc.
 
f:Z -> Z
Hf:forall x y : Z, f x * y = f (x * y)
p:positive
IHp:forall k0 : Z, Pos.iter f k0 p = Pos.iter f 1 p * k0
k:Z
Pos.iter f (Pos.iter f k p) p =
Pos.iter f (Pos.iter f 1 p) p * k
 
f:Z -> Z
Hf:forall x y : Z, f x * y = f (x * y)
p:positive
g:=Pos.iter f 1 p:Z
IHp:forall k0 : Z, Pos.iter f k0 p = g * k0
k:Z
Pos.iter f (Pos.iter f k p) p = Pos.iter f g p * k
 now rewrite !IHp, Z.mul_assoc.
 
f:Z -> Z
Hf:forall x y : Z, f x * y = f (x * y)
k:Z
f k = f 1 * k
 now rewrite Hf, Z.mul_1_l.
Qed.


forall (p : positive) (a : Z),
Pos.iter_op Z.mul p (a * a) =
Pos.iter_op Z.mul p a * Pos.iter_op Z.mul p a


forall (p : positive) (a : Z),
Pos.iter_op Z.mul p (a * a) =
Pos.iter_op Z.mul p a * Pos.iter_op Z.mul p a

 
p:positive
IHp:forall a0 : Z,
Pos.iter_op Z.mul p (a0 * a0) =
Pos.iter_op Z.mul p a0 * Pos.iter_op Z.mul p a0
a:Z
a * a * Pos.iter_op Z.mul p (a * a * (a * a)) =
a * Pos.iter_op Z.mul p (a * a) *
(a * Pos.iter_op Z.mul p (a * a))
 now rewrite IHp, Z.mul_shuffle1.
Qed.


a, b:Z
a ^^ b = a ^ b


a, b:Z
a ^^ b = a ^ b

 
a:Z
p:positive
a ^^ Z.pos p = a ^ Z.pos p

 
a:Z
p:positive
Pos.iter_op Z.mul p a = Pos.iter (Z.mul a) 1 p

 
p:positive
forall a : Z,
Pos.iter_op Z.mul p a = Pos.iter (Z.mul a) 1 p

 
p:positive
IHp:forall a0 : Z, Pos.iter_op Z.mul p a0 = Pos.iter (Z.mul a0) 1 p
a:Z
a * Pos.iter_op Z.mul p (a * a) =
a * Pos.iter (Z.mul a) (Pos.iter (Z.mul a) 1 p) p
p:positive
IHp:forall a0 : Z, Pos.iter_op Z.mul p a0 = Pos.iter (Z.mul a0) 1 p
a:Z
Pos.iter_op Z.mul p (a * a) =
Pos.iter (Z.mul a) (Pos.iter (Z.mul a) 1 p) p
a:Z
a = a * 1

 
p:positive
IHp:forall a0 : Z, Pos.iter_op Z.mul p a0 = Pos.iter (Z.mul a0) 1 p
a:Z
a * Pos.iter_op Z.mul p (a * a) =
a * Pos.iter (Z.mul a) (Pos.iter (Z.mul a) 1 p) p
 
p:positive
IHp:forall a0 : Z, Pos.iter_op Z.mul p a0 = Pos.iter (Z.mul a0) 1 p
a:Z
Pos.iter_op Z.mul p (a * a) =
Pos.iter (Z.mul a) (Pos.iter (Z.mul a) 1 p) p

   
p:positive
IHp:forall a0 : Z, Pos.iter_op Z.mul p a0 = Pos.iter (Z.mul a0) 1 p
a:Z
Pos.iter_op Z.mul p (a * a) =
Pos.iter (Z.mul a) 1 p * Pos.iter (Z.mul a) 1 p
p:positive
IHp:forall a0 : Z, Pos.iter_op Z.mul p a0 = Pos.iter (Z.mul a0) 1 p
a:Z
forall x y : Z, a * x * y = a * (x * y)

   
p:positive
IHp:forall a0 : Z, Pos.iter_op Z.mul p a0 = Pos.iter (Z.mul a0) 1 p
a:Z
forall x y : Z, a * x * y = a * (x * y)

   
p:positive
IHp:forall a0 : Z, Pos.iter_op Z.mul p a0 = Pos.iter (Z.mul a0) 1 p
a, x, y:Z
a * x * y = a * (x * y)
 symmetry; apply Z.mul_assoc.
 
p:positive
IHp:forall a0 : Z, Pos.iter_op Z.mul p a0 = Pos.iter (Z.mul a0) 1 p
a:Z
Pos.iter_op Z.mul p (a * a) =
Pos.iter (Z.mul a) (Pos.iter (Z.mul a) 1 p) p
 
p:positive
IHp:forall a0 : Z, Pos.iter_op Z.mul p a0 = Pos.iter (Z.mul a0) 1 p
a:Z
Pos.iter_op Z.mul p (a * a) =
Pos.iter (Z.mul a) 1 p * Pos.iter (Z.mul a) 1 p
p:positive
IHp:forall a0 : Z, Pos.iter_op Z.mul p a0 = Pos.iter (Z.mul a0) 1 p
a:Z
forall x y : Z, a * x * y = a * (x * y)

   
p:positive
IHp:forall a0 : Z, Pos.iter_op Z.mul p a0 = Pos.iter (Z.mul a0) 1 p
a:Z
forall x y : Z, a * x * y = a * (x * y)

   
p:positive
IHp:forall a0 : Z, Pos.iter_op Z.mul p a0 = Pos.iter (Z.mul a0) 1 p
a, x, y:Z
a * x * y = a * (x * y)
 symmetry; apply Z.mul_assoc.
 
a:Z
a = a * 1
 now Z.nzsimpl.
Qed.


n:Z
n ^^ 0 = 1


n:Z
n ^^ 0 = 1
 reflexivity. Qed.


a, b:Z
0 <= b -> a ^^ Z.succ b = a * a ^^ b


a, b:Z
0 <= b -> a ^^ Z.succ b = a * a ^^ b

 
a:Z
Hb:0 <= 0
a = a * 1
a:Z
b:positive
Hb:0 <= Z.pos b
Pos.iter_op Z.mul (b + 1) a =
a * Pos.iter_op Z.mul b a
a:Z
b:positive
Hb:0 <= Z.neg b
a ^^ Z.pos_sub 1 b = a * 0

 
a:Z
Hb:0 <= 0
a = a * 1
 now Z.nzsimpl.
 
a:Z
b:positive
Hb:0 <= Z.pos b
Pos.iter_op Z.mul (b + 1) a =
a * Pos.iter_op Z.mul b a
 now rewrite Pos.add_1_r, Pos.iter_op_succ by apply Z.mul_assoc.
 
a:Z
b:positive
Hb:0 <= Z.neg b
a ^^ Z.pos_sub 1 b = a * 0
 now elim Hb.
Qed.


a, b:Z
b < 0 -> a ^^ b = 0


a, b:Z
b < 0 -> a ^^ b = 0

 now destruct b.
Qed.


p, q:positive
Z.pos p ^^ Z.pos q = Z.pos (p ^ q)


p, q:positive
Z.pos p ^^ Z.pos q = Z.pos (p ^ q)

 now rewrite Zpower_equiv, Pos2Z.inj_pow.
Qed.