The Coq mailing list

[Marcus Ramos <marcus.ramos AT univasf.edu.br>]

That works, thank you. However, I still don´t understand why apply didn´t do the job.

Regards,

Marcus.

2014-06-26 15:54 GMT+02:00 Gregory Malecha <gmalecha AT cs.harvard.edu>:

I believe that that is just the semantics of [apply] in Ltac. [apply] attempts to fully apply a term. You can achieve the behavior you are looking for by doing.

generalize (x _ _ hPi); clear hPi; intro hPi

On Thu, Jun 26, 2014 at 6:22 AM, Marcus Ramos <marcus.ramos AT univasf.edu.br> wrote:

Hi Vincent,

That was me, thanks for forwarding the question. As I had not seen your message before, I made another post with the same contents a few minutes ago. Sorry for the duplicate.

Marcus.

2014-06-26 12:00 GMT+02:00 Vincent Siles <vincent.siles AT ens-lyon.org>:

Hi club,
an interesting question was asked on StackOverflow yesterday, and I
have to say I don't understand why this simple apply fails. Consider
the script:

Parameter P: nat -> Prop.
Parameter Q: nat -> Prop.
Hypothesis x : forall i, P i -> (forall k, Q k).

Lemma y:
  forall i, P i -> (* Whatever *) P i.
Proof.
  intros i hPi.
  apply x in hPi.

It fails with: Error: Unable to find an instance for the variable k.

Why does Coq asks for the instantiation of k ?

Best,
V.

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/