The Coq mailing list

[<michael.soegtrop AT intel.com>]

Dear Coq users,

I don't understand the behaviour of induction when the eqn: option is used.
Here is a short example demonstrating the behaviour:

Lemma minimal_strange : forall n:nat, n = n.
Proof.
  intros.
  induction n as [|p] eqn:?.
  reflexivity.

After this I end up with:

1 subgoals
n : nat
p : nat
Heqn0 : n = S p
IHp : n = p -> p = p
______________________________________(1/1)
S p = S p

What I don't understand is why Coq adds the n=p condition to the induction
hypothesis. Obviously this cannot be fullfilled since n = S p. This makes the
induction hypothesis unusable.

Is this a bug in Coq or do i miss something here? I see similiar beaviour in
all cases I tried. With destruct eqn: seems to work fine, though.

Best regards,

Michael

P.S.: I am using version:
The Coq Proof Assistant, version 8.4pl2 (April 2013)
Architecture win32 running Win32 operating system