The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

    Dear Michael,

You might be interested in looking into the ssreflect plugin, which 
implements the behaviour you expected.
This is not really a bug, however: to achieve this, equation generation has 
to be interpreted differently for elim (or induction) than for case (or 
destruct):
the equation has to be generated after applying the second-order elimination 
lemma, rather than before, and its left-hand side is a new (generalized) 
variable, rather than the argument of the elimination tactic. In fact, the 
ssreflect code only uses this interpretation for eliminations that generate 
induction hypotheses; admittedly this could be better documented in the 
ssreflect manual (http://hal.inria.fr/docs/00/84/38/81/PDF/main.pdf , p. 25).

    Cheers,
Georges

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of 
michael.soegtrop AT intel.com
Sent: 24 October 2013 11:24
To: 
coq-club AT inria.fr
Subject: [Coq-Club] Strange behaviour of induction with eqn: option

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