The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

On Mon, 1 Aug 2011 16:14:15 +0200
AUGER Cedric 
<Cedric.Auger AT lri.fr>
 wrote:

> Le Mon, 01 Aug 2011 08:58:39 -0400,
> Adam Chlipala 
>Â <adam AT chlipala.net>
>  a écrit :
> 
> > frank maltman wrote:
> > > However, I'm now stuck proving the first case that does terminate:
> > >
> > 
> > I don't think your question is really about Coq.  This proof strategy 
> > fails on paper, too.
> > 
> 
> Hmm, that annoying if you consider this script:
> 

Thanks, both of you.

I guess I am convinced I have an informal proof (there's one in the book,
for a start) but at the same time, I'm likely convinced too easily. In
this situation, I'm never sure if my approach is wrong or if I just don't
know how to instruct coq properly. Seems as though it's the latter in this
case.