coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Force Principle Argument Recognition

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Force Principle Argument Recognition
Date: Mon, 30 Nov 2015 08:07:20 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga02.intel.com
Ironport-phdr: 9a23:zGu8LBU86Fe8B14WNxB31qIsE6bV8LGtZVwlr6E/grcLSJyIuqrYZhOEt8tkgFKBZ4jH8fUM07OQ6PC9Hzxeqsze7zgrS99laVwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oM2OJVUWz2DiPvtbF1afk0b4joEum4xsK6I8mFPig0BjXKBo/15uPk+ZhB3m5829r9ZJ+iVUvO89pYYbCf2pN/dwcbsNRj8hKiU+4NDhnRjFVwqGoHUGGC1CmR1RRgPB8RvSX5HrsyK8uPAriweAOsijB4szVDu+9aBzDFfNiSwHPjM9uimDj817jKtWpFS6oBFw35TTeKmUMuZzeuXWetZMFjkJZdpYSyEUWtD0VIAIFedUZes=

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

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

[Coq-Club] Force Principle Argument Recognition, Kenneth Adam Miller, 11/30/2015
- RE: [Coq-Club] Force Principle Argument Recognition, Soegtrop, Michael, 11/30/2015
  - Re: [Coq-Club] Force Principle Argument Recognition, Kenneth Adam Miller, 11/30/2015
    - RE: [Coq-Club] Force Principle Argument Recognition, Soegtrop, Michael, 11/30/2015
      - Re: [Coq-Club] Force Principle Argument Recognition, Kenneth Adam Miller, 11/30/2015
        
        Re: [Coq-Club] Force Principle Argument Recognition, Emma Tosch, 11/30/2015
        
        Re: [Coq-Club] Force Principle Argument Recognition, Epiphanie, 11/30/2015