I came up with two equivalent definitions of a function applyN which applies a given function f to an argument x n times:
Variable A : Type.
Fixpoint applyN1 (n : nat) (f : A -> A) (x : A) :=
match n with
| 0 => x
| S n0 => applyN1 n0 f (f x)
end.
Fixpoint applyN2 (n : nat) (f : A -> A) (x : A) :=
match n with
| 0 => x
| S n0 => f (applyN2 n0 f x)
end.
I'd like to prove that these functions are extensionally equal in Coq:
Theorem applyEq : forall n f x, applyN1 n f x = applyN2 n f x.
Proof.
intros.
induction n.
reflexivity. (* base case *)
simpl.
rewrite <- IHn.
and I get stuck here. I can't really think of a lemma that would be helpful and easier to prove. How do you go about proving equalities of direct-style and accumulator-based recursive functions without an explicit accumulator?
I was able to prove it using first a lemma
Lemma applyN1_lr : forall k f x, f (applyN1 k f x) = applyN1 k f (f x).
proven by induction, then using induction again for applyEq.
Note that something I encountered while proving my applyN1_lr (and which might have blocked you in your proof attempts) is that you need to have a general induction hypothesis of the form forall x : A, …. Indeed, you want to apply this hypothesis with f x rather than x, and so doing the induction on a fixed x will lead you nowhere. To do this you can either completely avoid introducing x, or use the tactics revert x or generalize x to get the more general goal with which induction succeeds.