Library additions.Naive

Naïve and Monomorphic Functions for Computing Powers.

Exponentiation of integers

Let us define a function Z.power : Z → nat → Z by structural recursion on the exponent n:

Require Import ZArith.
Open Scope Z_scope.

Module Z.

Fixpoint power (x:Z)(n:nat) :=
match n with
| 0%nat ⇒ 1
| S p ⇒ x × power x p
end.

Compute power 2 10.

Some basic properties of Z.power

Lemma power_S : ∀ (x:Z)(n:nat), power x (S n) = x × power x n.

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

End Z.

Exponentiation modulo m

Let m be some natural number. We can compute for any number x and exponent n the number .

Since m and x can be arbitrary large numbers, we give them the type N of binary natural number. Following our naïve approach, the exponent n is still of type nat.

Module N_mod.
#[local] Open Scope N_scope.

Section m_fixed.

  Variable m: N.

  Definition mult_mod (x y : N) := (x × y ) mod m.

  Fixpoint power (x: N) (n : nat) : N :=
    match n with
      | 0%nat ⇒ 1 mod m
      | S p ⇒ mult_mod x (power x p)
    end.
End m_fixed.
End N_mod.

Compute N_mod.power 14555553%N 5689%N 27.

= 9086410
: N

Exponentiation of matrices

Our last example is a definition of where is a matrix over any scalar type , assuming one can provide with a semi-ring structure.

Module M2.
Section Definitions.

  Variables (A: Type)
           (zero one : A)
           (plus mult : A → A → A).

  Variable rt : semi_ring_theory zero one plus mult (@eq A).
  Add Ring Aring : rt.

  Notation "0" := zero.
  Notation "1" := one.
  Notation "x + y" := (plus x y).
  Notation "x * y " := (mult x y).

  Structure t : Type := mat{c00 : A; c01 : A;
                            c10 : A; c11 : A}.

  Definition Id2 : t := mat 1 0 0 1.

  Definition M2_mult (M M':t) : t :=
    mat (c00 M × c00 M' + c01 M × c10 M')
        (c00 M × c01 M' + c01 M × c11 M')
        (c10 M × c00 M' + c11 M × c10 M')
        (c10 M × c01 M' + c11 M × c11 M').

  Infix "**" := M2_mult (at level 40, left associativity).

  Fixpoint power (M : t) (n : nat) : t :=
    match n with
      | 0%nat ⇒ Id2
      | S p ⇒ M ** (power M p)
    end.

The ring tactic, applied to inhabitants of type A, allows us to prove associativity of matrix multiplication, then a law of distributivity of power upon **

  Lemma Id2_neutral : ∀ M:t, Id2 ** M = M.

  Lemma M2_mult_assoc : ∀ M M' M'':t, M ** (M' ** M'') =
                                            (M ** M') ** M''.

  Lemma power_of_plus (M:t) :
  ∀ n p, power M (n + p) = power M n ** power M p.

End Definitions.
End M2.

Definition fibonacci (n:nat) :=
  M2.c00 N (M2.power N 0%N 1%N Nplus Nmult (M2.mat _ 1 1 1 0)%N n).