Library additions.Compatibility

Compatibility with StdLib exponentiation functions

Function for computing powers already exist in 's standard library. We provide equivalence theorems with functions defined in our module Pow.

From additions Require Import Monoid_def Monoid_instances
Pow.
From Coq Require Import Lia ArithRing.

really logarithmic versions of N.pow, Pos.pow and Z.pow

We propose three functions that are extensionnaly equivalent to functions of the standard library. These functions are defined in the module; we just rename them for readability's sake.

Definition N_pow (a n: N) :=Pow.N_bpow a n.

Definition Pos_pow (a n : positive) := Pow.Pos_bpow a n.

Definition Z_pow (x y : Z) :=
match y with
| 0%Z ⇒ 1%Z
| Z.pos p ⇒ Pow.N_bpow x (Npos p)
| Z.neg _ ⇒ 0%Z
end.

Equivalence between StdLib definitions and ours

Section Equivalence.
Variable (A: Type)
         (op : Mult_op A)
         (one : A).

Context (M : Monoid op one).
Open Scope M_scope.

Check fun x y:A ⇒ x × y.

Ltac monoid_rw :=
    rewrite (@one_left A op one M) ||
    rewrite (@one_right A op one M)||
    rewrite (@op_assoc A op one M).

  Ltac monoid_simpl := repeat monoid_rw.

Ltac power_simpl := repeat (monoid_rw || rewrite <- power_of_plus).

Let pos_iter_M x := Pos.iter (op x).

During an execution of the binary exponentiation algorithm through the function binary_power_mult, the "accumulator" acc is always a power of . Thus, even if the considered monoid is not abelian, the accumulator commutes with any other power of .

Let is_power_of (x acc:A) := ∃ i , acc = x ^ i.

Lemma Pos_iter_op_ok_0 :
  ∀ p x acc, is_power_of x acc →
                  pos_iter_M x acc p = binary_power_mult x acc p .

Lemma Pos_iter_op_ok:
  ∀ p x,
    pos_iter_M x one p = binary_power_mult x one p .

Lemma Pos_iter_ok: ∀ p x, N_bpow x (Npos p) = pos_iter_M x one p.

End Equivalence.

Lemma Pos_pow_power : ∀ n a : positive ,
                        (a ^ n )%positive = power a (Pos.to_nat n).

Lemma Npos_power_compat : ∀ (n:nat)(a:positive),
                            Npos (power a n) = power (Npos a) n.

Lemma N_pow_power : ∀ n a , (a ^ n )%N = power a (N.to_nat n).

Lemma N_pow_compat : ∀ n (a:N), (a ^ n )%N = N_pow a n.

Lemma Pos_pow_compat : ∀ n (a:positive), (a ^ n )%positive = Pos_pow a n.

Lemma nat_power_ok : ∀ a b:nat, (a ^ b)%nat = (a ^ b)%M.

  Lemma Pos2Nat_morph : ∀ (n:nat)(a : positive),
     Pos.to_nat (a ^ n)%M = Pos.to_nat a ^ n.

Lemma Z_pow_compat_pos : ∀ (p:positive) (x:Z),
        Z.pow_pos x p = N_bpow x (Npos p).

Lemma Z_pow_compat : ∀ x y: Z, Z_pow x y = (x ^ y)%Z.

Tests

Let us chose a big exponent, and a computation that does not create big numbers. So, the following computation time will be proportional to the number of recursive calls, hence to the number of multiplications

Time consuming !
Time Compute (1 ^ 56666667)%Z.

Finished transaction in 3.604 secs (3.587u,0.007s)

Finished transaction in 0. secs (0.u,0.s) (successful)

Adapting lemmas from Standard Library

Standard library already contains many lemmas about N.pow, Pos.pow and Z.pow. By using our extensional equivalence properties, one can easily prove the same properties for our implementation of the same functions.

We just give a simple example of this adaptation.

Section Adaptation.

Lemma N_size_gt : ∀ n : N, (n < N_pow 2 (N.size n))%N.

End Adaptation.

Comments on Stdlib's exponentiation

Print Z.pow.

Print Z.pow_pos.

Eval simpl in fun (x:nat) ⇒ Pos.iter S x 12%positive.