Applying hypothesis with unknown variables

Using Coq
1

I’m trying to prove the following lemma about functions on natural numbers

  Lemma nat_funcs : 
    forall (f : nat -> nat -> nat) (P : (nat -> nat) -> Prop), 
      (forall n, P (fun m => (f n m))) -> P (fun m => f (m + 1) m).

When I proceed and introduce variables to the context, I end up with a hypothesis:

H : forall n, P (fun m => (f n m))

and my goal is:

 P (fun m => f (m + 1) m)

I would like to apply H and instantiate n with m + 1 but the problem is, m is out of scope, is there a way I can do that?

I tried eapply and rapply but this doesn’t work either.

2

This lemma is false.

Consider what happens when P g is the proposition that g is a constant function.
Then when f x y = x, we have forall n, (fun m => f n m) = (fun m => n) which is a constant function, while (fun m => f (m + 1) m) = (fun m => m + 1) which is not a constant function.

1 Like