The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

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.

 

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