The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Mon, 1 Aug 2011 15:42:44 +0000,
frank maltman 
<frank.maltman AT googlemail.com>
 a écrit :

> 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.
> 

Ok, you didn't understood my response; my script proved what you wished
(at least on my version of Coq), so that your formalization may be
wrong (the eternal problem of "how can I be sure I am in the theory I
want?"), but what you intended to prove was provable, so it doesn't seem
meaningless.