functional-programmingcoqtheorem-proving

Proving extensional equality of two functions


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?


Solution

  • 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.