The Coq mailing list

[<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