The Coq mailing list

[<hugoccomp AT gmail.com>]

A friend of mine is working his way through Software Foundations and was using
its "Case" (and "SCase", etc) tactics to annotate the proof context.
Eventually the book introduced the "eqn:" extra option to the "destruct"
tactic, and it seemed like it was a a suitable replacement for that usage of
"Case" tatics, until he tried to use the same option with "induction".

Goal forall n, n+0=n.
induction n as [|n'] eqn:Heqn.
(*The first goal, 0+0=0, goes through normally...*)
reflexivity.
(*But here we are stuck - the equality generated by eqn: blocks usage of the
inductive hypothesis. *)

Is this behavior intended?

A similar "impossible" proof state is reached if,
instead of "induction n as [|n'] eqn:Heqn.",  you start with "intro n;remember
n;induction n".
But if you're using "remember", you can "generalize dependent" the fresh term
before the induction
and then all goes through fine. I can't help but think that maybe "eqn:"
should be doing something similar behind the scenes.

Also i'm using Coq 8.4pl2 - if this is fixed on the later versions let me
know.