The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Your induction hypothesis is too specific; you are appealing to  
induction too late in the proof. Try doing the induction before the  
intros.

Edsko

On 12 Mar 2009, at 15:26, Dimitris Vekris wrote:

> Could you give me a hint cause i'm stuck?
>
> Lemma lemma1 (ord : nat)(sl : list ST)(l : nat) :
>                  find ord sl (S l) = S (find ord sl l).
> Proof.
> intros.
> induction sl; simpl.
> reflexivity.
> destruct (compare_nat (order a) ord).
> Admitted.
>
> Thanks for your help!
>
> > CC: 
> coq-club AT pauillac.inria.fr
> > From: 
> devriese AT cs.tcd.ie
> > To: 
> dvekris AT hotmail.com
> > Subject: Re: [Coq-Club] Problems with tail-recursion.
> > Date: Thu, 12 Mar 2009 15:11:03 +0000
> >
> > What's difficult about them? I tried lemma1 and lemma2, and they go
> > through easily enough. Where do you get stuck?
> >
> > (BTW, compare_nat is eq_nat_dec from the Arith library).
> >
> > Edsko
>
> What can you do with the new Windows Live? Find out