The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

What if induction eqn: did something instead like so:

Goal forall n, n+0=n.
intro n.
remember n as n0 eqn:E.
revert n n0 E.
induction n as [|n'].

-- Jonathan


On 09/07/2014 10:53 AM, Hugo Herbelin wrote:
> Hi,
>
> As it is implemented now, the "eqn:" modifier to induction is actually
> pointless as it impacts the induction hypotheses in a way which makes
> them useless. It is here by analogy with the "eqn:" for destruct, but
> it is a posteriori an error to make it available for induction.
>
> In any case, the primary use of the "eqn:" modifier was to remember
> the value of the term destruct is applied on. If it also helps to
> indicate which case of a case analysis proof is under consideration,
> it is somehow incidental. Maybe one day will this information be made
> available to the user without impacting the purely logical content of
> the proof...
>
> Hugo Herbelin
>
> On Fri, Sep 05, 2014 at 02:50:13PM +0200, 
> hugoccomp AT gmail.com
>  wrote:
> > 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.