The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 06/26/2014 06:00 AM, Vincent Siles wrote:
> 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.
First, note that "eapply x in hPi" does work.

Then, note that it works by creating an existential variable (evar) in 
the place of k.  So, apply did not work because it refuses to create 
evars.  I almost always use eapply (and the other e... tactics), but 
then the result is having to live with many evars - which can make 
proving future subgoals much more difficult.

-- Jonathan