Library additions.Pow

Exponentiation in a Monoid

In this section, we give two polymorphic functions for computing : the naive ( linear) one and the aforementionned binary method, that takes less than multiplications.

Both functions require an instance of EMonoid. Their code use the multiplication of the monoid, and sometimes its unity. Correctness proofs require the "axioms" of monoid structure.

Set Implicit Arguments.

Require Export ZArith Div2.
Require Export Recdef.
Require Import Relations Morphisms.

Require Import Monoid_def.
Require Import Arith Lia.

Open Scope M_scope.

Two functions for computing powers

The module defines two functions for exponentiation on any Emonoid on carrier .

The function power has type A → nat → A; it is linear with respect to the exponent. Its simplicity and the fact that the exponent has type nat make it adequate for being the reference for any other definition, and for easily proving laws like .
The function Pos_bpow has type A → positive → A and is logarithmic with respect to its exponent. This function should be used for effective computations. Its variant N_bpow allows the exponent to be .

The "naive" reference function

Generalizable Variables A E_op E_one E_eq.

Fixpoint power `{M: @EMonoid A E_op E_one E_eq}
         (x:A)(n:nat) :=
  match n with 0%nat ⇒ E_one
             | S p ⇒ x × x ^ p
  end
where "x ^ n" := (power x n) : M_scope.

Lemma power_eq1 `{M: @EMonoid A E_op E_one E_eq}(x:A) :
  x ^ 0 = E_one.

Lemma power_eq2 `{M: @EMonoid A E_op E_one E_eq}(x:A) (n:nat) :
x ^ (S n ) = x × x ^ n.

Lemma power_eq3 `{M: @EMonoid A E_op E_one E_eq}(x:A) :
x ^ 1 == x.

The binary exponentiation function (exponents in positive)

The auxiliary function below computes , where the "accumulator" acc is intented to be an already computed power of x:

Fixpoint binary_power_mult `{M: @EMonoid A E_op E_one E_eq}
         (x a:A)(p:positive) : A
  :=
  match p with
    | xH ⇒ a × x
    | xO q ⇒ binary_power_mult (x × x) a q
    | xI q ⇒ binary_power_mult (x × x) (a × x) q
  end.

The following function decomposes the exponent p into , then calls binary_power_mult with and .

Fixpoint Pos_bpow `{M: @EMonoid A E_op E_one E_eq}
         (x:A)(p:positive) :=
match p with
  | xH ⇒ x
  | xO q ⇒ Pos_bpow (x × x) q
  | xI q ⇒ binary_power_mult (x × x) x q
end.

*** It is straightforward to adapt Pos_bpow for accepting exponents of type N :

Definition N_bpow `{M: @EMonoid A E_op E_one E_eq} x (n:N) :=
  match n with
  | 0%N ⇒ E_one
  | Npos p ⇒ Pos_bpow x p
  end.

Infix "^b" := N_bpow (at level 30, right associativity) : M_scope.

Properties of the power function

Taking power as a reference, it remains to prove two kinds of properties

Mathematical properties of exponentiation, i.e the function power,
proving correctness of functions Pos_bpow and N_bpow

First, let us consider some Emonoid and define some useful notations and tactics:

Section M_given.

  Variables (A:Type) (E_one:A) .
  Context (E_op : Mult_op A) (E_eq : Equiv A)
          (M:EMonoid E_op E_one E_eq).

#[global] Instance Eop_proper : Proper (equiv ==> equiv ==> equiv) E_op.

Ltac monoid_rw :=
    rewrite Eone_left ||
    rewrite Eone_right ||
    rewrite Eop_assoc.

Ltac monoid_simpl := repeat monoid_rw.

#[global] Instance power_proper :
  Proper (equiv ==> eq ==> equiv) power.

Lemma power_of_plus :
  ∀ x n p, x ^ (n + p ) == x ^ n × x ^ p.

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

Lemma power_commute x n p:
  x ^ n × x ^ p == x ^ p × x ^ n.

Lemma power_commute_with_x x n:
  x × x ^ n == x ^ n × x.

Lemma power_of_power x n p:
  (x ^ n ) ^ p == x ^ (p × n ).

Lemma power_of_power_comm x n p : (x ^ n ) ^ p == (x ^ p ) ^ n.

Lemma sqr_eqn : ∀ x, x ^ 2 == x × x.

Ltac factorize := repeat (
                rewrite <- power_commute_with_x ||
                rewrite <- power_of_plus ||
                rewrite <- sqr_eqn ||
                rewrite <- power_eq2 ||
                rewrite power_of_power).

Lemma power_of_square x n : (x × x ) ^ n == x ^ n × x ^ n.

Correctness of the binary algorithm

Correctness of the "concrete" functions Pos_bpow and N_bpow with respect to the more abstract function power is expressed by extensional equalities, taking into account the conversion between various representations of natural numbers.

Lemma binary_power_mult_ok :
  ∀ p a x, binary_power_mult x a p == a × x ^ Pos.to_nat p.

Lemma Pos_bpow_ok :
  ∀ p x, Pos_bpow x p == x ^ Pos.to_nat p.

#[global] Instance Pos_bpow_proper :
  Proper (equiv ==> eq ==> equiv) Pos_bpow.

Lemma N_bpow_ok :
  ∀ n x, x ^b n == x ^ N.to_nat n.

Lemma N_bpow_ok_R :
  ∀ n x, x ^b (N.of_nat n ) == x ^ n.

Lemma Pos_bpow_ok_R :
  ∀ p x, p ≠ 0 →
              Pos_bpow x (Pos.of_nat p) == x ^ p.

Lemma N_bpow_commute : ∀ x n p,
                        x ^b n × x ^b p ==
                        x ^b p × x ^b n.

Lemma Pos_bpow_of_plus : ∀ x n p, Pos_bpow x (n + p)%positive ==
                                       Pos_bpow x n × Pos_bpow x p.

Lemma Pos_bpow_of_bpow : ∀ (x:A) n p,
    Pos_bpow (Pos_bpow x n) p == Pos_bpow x (p × n)%positive.

Remark

If we normalize exponentiation functions with a given exponent, we notice that the obtained functions do not execute the same computations, but it is hard to visualize why the binary method is more efficient than the naive one.

Eval simpl in fun (x:A) ⇒ x ^b 17.

Eval simpl in fun x ⇒ x ^ 17.

Definition pow_17 (x:A) :=
  let x2 := x × x in
  let x4 := x2 × x2 in
  let x8 := x4 × x4 in
  let x16 := x8 × x8 in
  x16 × x.

Eval cbv zeta beta delta [pow_17] in pow_17.

= fun x : A => x * x * (x * x) * (x * x * (x * x)) * (x * x * (x * x) * (x * x * (x * x))) * x : A -> A

In order to compare the real computations needed to raise some to its -th power, we need to make more explicit how intermediate values are used during some computation. This is described in the module (see ).

Properties of Abelian Monoids

Some equalities hold in the restricted context of abelian (a.k.a. commutative) monoids.

Section Power_of_op.
Context {AM:Abelian_EMonoid M}.

Theorem power_of_mult :
   ∀ n x y, (x × y ) ^ n == x ^ n × y ^ n.

End Power_of_op.

End M_given.

Infix "^" := power : M_scope.

Ltac monoid_simpl M := generalize (Eop_proper M); intro;
  repeat ( rewrite (Eone_left ) ||
    rewrite (Eone_right ) ||
    rewrite (Eop_assoc )).

  Ltac power_simpl M := generalize (Eop_proper M); intro;
  repeat ( rewrite Eone_left || rewrite Eone_right || rewrite Eop_assoc
     || rewrite power_of_plus).