The Coq mailing list

[Hugo Carvalho <hugoccomp AT gmail.com>]

My guess is that "generalize dependent f" between "destruct f as [l] eqn:E" and "induction l as [|hl tl]" ought to do the trick.

The example, again:

Variable P : Prop.

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

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

This gives:

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

2014-09-23 18:38 GMT-03:00 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