The Coq mailing list

[Laurent Théry <Laurent.Thery AT inria.fr>]

On 11/10/2012 02:54 PM, Kevin Sullivan wrote:
> 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.
You can prove it directly with two inductions, or only one induction 
using an intermediate lemme
f (ant' f x n) = ant' f (f x) n (that is proved by induction)

Hint: don' t forget to generalize your goal before doing the induction!

--
Laurent