coq --- function power definition

Question

I am interested in how would one define f to the n in Coq:

Basically, as an exercise, I would like to write this definition and then confirm that my algorithm implements this specification. Inductive definition seems appropriate here, but I was not able to make it clean as above. What would be a clean Coq implementation of the above?

Answer 1

With the pow_func function that gallais defined, you can state your specification as lemmas, such as:

Lemma pow_func0: forall (A:Type) (f: A -> A) (x: A), pow_fun f O x = f x.

and

Lemma pow_funcS: forall (n:nat) (A: Type) (f: A->A) (x:A), pow_fun f (S n) x = f (pow_fun f n x).

The proof should be trivial by unfolding the definition

Answer 2

Inductive is used to define types closed under some operations; this is not what you are looking for here. What you want to build is a recursive function iterating over n. This can be done using the Fixpoint keyword:

Fixpoint pow_func {A : Type} (f : A -> A) (n : nat) (a : A) : A :=
 match n with
  | O   => f a
  | S n => f (pow_func f n a)
end.

If you want a nicer syntax for this function, you can introduce a Notation:

Notation "f ^ n" := (pow_func f n).

However, note that this is not a well-behaved definition of a notion of power: if you compose f ^ m and f ^ n, you don't get f ^ (m + n) but rather f ^ (1 + m + n). To fix that, you should pick the base case f ^ 0 to be the neutral element for composition id rather than f itself. Which would give you:

Fixpoint pow_func' {A : Type} (f : A -> A) (n : nat) (a : A) : A :=
 match n with
  | O   => a
  | S n => f (pow_func' f n a)
end.