coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problems with tail-recursion.

From: Adam Chlipala <adamc AT hcoop.net>
To: Cedric Auger <Cedric.Auger AT lri.fr>
Cc: Edsko de Vries <devriese AT cs.tcd.ie>, dimitrisg7 <dvekris AT hotmail.com>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Problems with tail-recursion.
Date: Thu, 12 Mar 2009 11:55:24 -0400
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Cedric Auger wrote:

Edsko de Vries a e'crit :

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

A more constructive answer ;)

I don't agree that writing someone's proof for him is a constructive answer, despite my own guilt for doing it commonly on this list. :P I liked Edsko's approach better, and I think it is more likely to help the original poster learn how to use Coq effectively.

[Coq-Club] Problems with tail-recursion., dimitrisg7
- Re: [Coq-Club] Problems with tail-recursion., Edsko de Vries
  - RE: [Coq-Club] Problems with tail-recursion., Dimitris Vekris
    - Re: [Coq-Club] Problems with tail-recursion., Edsko de Vries
  - Re: [Coq-Club] Problems with tail-recursion., Cedric Auger
    - Re: [Coq-Club] Problems with tail-recursion., Adam Chlipala