CODEWITHSUNDEEP
functional-programmingcoqtheorem-proving
Sai Ganesh Muthuraman
Sai Ganesh Muthuraman

Reputation: 111

Using an exponentiation function

This is the definition for exp in group theory:

Definition exp : Z -> U -> U.
Proof.
intros n a.
elim n;
 clear n.
exact e.
intro n.
 elim n; clear n.
exact a.
intros n valrec.
exact (star a valrec).
intro n; elim n; clear n.
exact (inv a).
intros n valrec.
exact (star (inv a) valrec).
Defined.

I tried to define a ((a^n)^k) this way.

Definition exp2 (n k : Z) (a : U)  := fun a => exp k (exp  n a).

But exp k (exp n a) is of type U->U but I want it to be of type U. How can I do it?

Upvotes: 0

Views: 70

Answers (1)

Vinz
Vinz

Reputation: 6047

As Gilles pointed out, the signature of your exp2 function is equivalent to

Definition exp2 (n k : Z) (a a(*won't work in Coq*) : U) :=
    exp k (exp n a).

You need to remove one of the a:

Definition exp2 (n k : Z) (a : U) := exp k (exp n a).
Definition exp2_alt (n k : Z) : fun a => exp k (exp n a).

Upvotes: 1

Related Questions