The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

Your example is equivalent to:

Lemma minimal_strange : forall n:nat, n = n.

Proof.

  intros.

  remember n as m eqn : Heqn0.

  induction m as [|p].

  reflexivity.

That feature is useful when you're doing induction on a term that's not a variable, as in for example "induction (S n)", or "induction (n + m)". In these cases, if you don't remember the term, your goal might become unprovable.

On Thu, Oct 24, 2013 at 11:23 AM, <michael.soegtrop AT intel.com> wrote:

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