coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Fixpoint decreasing parameter:help

From: Adam Koprowski <adam.koprowski AT gmail.com>
To: Groleo Marius <groleo AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Fixpoint decreasing parameter:help
Date: Wed, 13 Jan 2010 18:15:20 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=srBTSLzESZO2iZrk9uHAP2vjN206e9alPsggw7cXOycupfuvDr03cfa1XGB2+a0SWh JDIh1VpBr0fmru7psJ1Mr2tPWApCxbYUF2TF+g5iwtkv1lwgNKuORpqdkpnky28yBVpX foK3zhtfnaF12JTSn0rbjX96zsEJCQV2lG3Uc=

I'm trying to write a recursive function, that would only loop until a
given parameter, n, get equal to 1.
[...]
Can you point me please to some documents regarding this construct ?

��Since you want [n] to decrease from some positive value to 0, why not making it a natural number [nat] instead? Then writing what you intend should go smoothly and Coq will be able to establish that the function is terminating.

��Best,

��Adam

--
Adam Koprowski � [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate � �[15 rue Berlier, 75013 Paris, France]
Sent from Amsterdam, NH, Netherlands

[Coq-Club] Fixpoint decreasing parameter:help, Groleo Marius
- Re: [Coq-Club] Fixpoint decreasing parameter:help, Adam Chlipala
  - Re: [Coq-Club] Fixpoint decreasing parameter:help, Groleo Marius
- Re: [Coq-Club] Fixpoint decreasing parameter:help, Adam Koprowski
  - Re: [Coq-Club] Fixpoint decreasing parameter:help, Groleo Marius