The Coq mailing list

["Kevin Sullivan" <sullivan.kevinj AT gmail.com>]

My students presented two solutions to the simple problem of applying a
function f n times to an argument x (iterated composition). The first says
apply f to the result of applying f n-1 times to x; the second,  apply f n-1
times to the result of applying f to x. I challenged one student to prove that
the programs are equivalent. This ought to be pretty easy based on the
associativity of composition. Your best solution?

Fixpoint ant {X: Type} (f: X->X) (x: X) (n: nat) : X :=
match n with
| O => x
| S n' => f (ant f x n')
end.

Fixpoint ant' {X: Type} (f: X->X) (x: X) (n: nat) : X :=
match n with
| O => x
| S n' => ant' f (f x) n'
end.

Theorem equiv: forall (X: Type) (f: X->X) (x: X) (n: nat),
(ant f x n) = (ant' f x n).
Proof.  admit.