The Coq mailing list

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

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

Dear Kenneth,

 

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?

 

It is definitely possible to solve the software foundations course exercises on nat/binnum conversion without use of a log function. One thing you learn quickly with Coq is to obey Einstein’s saying “Everything should be made as simple as possible, but not simpler”. Otherwise you will spend a lot of time convincing Coq that your solution is correct. If you need some help or pointers, please drop me a private mail. I think the authors don’t like it too much if their exercises can be solved by google.

 

I don't want to solve them with google, I do want to understand them. I'm just looking for pointers in how to move forward. To be able to use Coq, I need to be able to understand how to get it to see that the function will terminate, not how to solve the problem itself.

Sent you an email.

 

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