The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

On Mon, Nov 30, 2015 at 3:07 AM, Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Kenneth,

 

> Does anybody have any advice how to move forward so that I can get the Coq interpreter to accept my definition?

 

The below lecture notes by Benjamin Grégoire from a Coq summer school helped me a lot to get a grip on more intricate fixpoints. In your case I would think an explicit termination proof is required. See the slides “Example using Function: fact on Z”.

Jeeze, an explicit termination proof just for a function that I'm writing that is going to be used as a basis for more proofs... It might be better if I really reado this with Peano integers.

In all actuality, the need to use any other type than nat arose from the need for the log function. So maybe I should have started describing the original objective?

 

 

www.di.ens.fr/~zappa/teaching/coq/ecole11/summer/lectures/lec9.pdf

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928