The Coq mailing list

[Sosuke MORIGUCHI <chiguri.s AT gmail.com>]

Hi Colm,

I have got the same question, but this is just usual, and not a bug.

"eapply" just waits instantiation of some variables, and instantiated terms
MUST be describable in the context of application of "eapply".

Otherwise, we can prove the following theorem.

Goal (exists a : A, P a) -> { x : A | P a }.

when we use following variables.

Variables (A : Type) (P : A->Prop).

This shows that, we can make a program (which is predicative)
from a predicate (which is impredicative).

Best regards,

Sosuke Moriguchi.

2013/5/11 <bhandalc AT tcd.ie>

Hi  people,

Just noticed some unusual behaviour of eapply. It's not a big deal, very easy
to work around, but just thought I'd flag it. I'm using Coq version 8.3pl5.
Here is the code:

(*Just a simple Lemma for use in the test lemma*)
Lemma simple : forall (x y : nat),
  x < y -> y <> 0. intros. destruct y.
  inversion H. unfold not. intro.
  inversion H0. Qed.

(*This works OK*)
Lemma testGood : forall y : nat,
  (exists x : nat, x < y) -> y <> 0.
  intros. inversion H. eapply simple.
  apply H0. Qed.

(*This breaks with the error message: Error: Impossible to unify "?25" with
"x".*)
Lemma testBug : forall y : nat,
  (exists x : nat, x < y) -> y <> 0.
  intros. eapply simple. inversion H.
  apply H0.

It seems as though eapply doesn't like when you instantiate existentials in a
hypothesis after the application- they must have existsed beforehand. The
workaround is simple: Just instantiate before eapply. But I believe the
behaviour is of interest nonetheless.

All the best,

Colm