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.