The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 09/23/2014 08:05 PM, Hugo Carvalho wrote:
> 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

Thanks!  In the case I'm interested in, having that particular inductive 
hypothesis works (I can construct the necessary "Foo tl", even though it 
isn't used).  However, is it possible to keep the equality from the 
destruct, but not have it get incorporated into the inductive hypothesis 
at all?  In other words, restrict the inductive hypotheses to what it 
would have been if there was no equation E at all (in this simplified 
case, just P alone)?

-- Jonathan