CODEWITHSUNDEEP
functional-programmingcoqtheorem-proving
shooqie
shooqie

Reputation: 1022

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?

Upvotes: 1

Views: 120

Answers (2)

Meven Lennon-Bertrand
Meven Lennon-Bertrand

Reputation: 1296

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.

Upvotes: 2

kyo dralliam
kyo dralliam

Reputation: 1217

You could prove an auxilliary lemma, for instance

Lemma apply1rec n : forall k f x, k <= S n -> f (applyN1 k f x) = applyN1 k f (f x).

(The only external lemma I needed to prove that one is le_S_n : forall n m, S n <= S m -> n <= m from Coq.PeanoNat)

And the proof is then easy to finish

Theorem applyEq : forall n f x, applyN1 n f x = applyN2 n f x.
Proof.
  intros n ? ? ; induction n as [|n IHn].
  - reflexivity.  (* base case *)
  - simpl.
    rewrite <- IHn, (apply1rec n n).
    * reflexivity.
    * apply Nat.le_succ_diag_r.
Qed.

Upvotes: 2

Related Questions