The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

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.

I think I have a case of this, but it is slightly different.  The eqn: is modifying a destruct prior to the induction (case_eq ; intros works similarly), but the induction hypotheses are still messed up as a result.  Here's a simplified example:

Variable P : Prop.

Inductive foo : Type :=
| Foo (l : list nat) : foo.

Goal foo -> P.
intro f.
destruct f as [l] eqn:E.
induction l as [|hl tl].
Focus 2.

This gives:

1 subgoal
f : foo
hl : nat
tl : list nat
E : f = Foo (hl :: tl)
IHtl : f = Foo tl -> P
______________________________________(1/1)
P

Note that the IHtl induction hypothesis can't be used, as Foo(hl::tl) does not equal Foo tl.  Somehow, I need an equality relating f with Foo (hl::tl), but I don't want that equality to creep into the inductive hypothesis unless it stays the same.

Does anyone know a way around this?  I have tried various that end up with the same result.

-- Jonathan