Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] Force Principle Argument Recognition

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Force Principle Argument Recognition


Chronological Thread 
  • 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 15:58:29 +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 mga01.intel.com
  • Ironport-phdr: 9a23:ymfGYRUjIZ2ny4AMgMPvOi1QIATV8LGtZVwlr6E/grcLSJyIuqrYZhOGt8tkgFKBZ4jH8fUM07OQ6PC9HzxQqszc+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8CVM1UD3mf1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GPZTCy1jOGQo7uXqswPCRE2B/DFUBm4Ri19DBxXPxBD8RJb49CXg4LlTwi6faIfNSr07RS6l9+MjbR7jiC4KM3RxpGTWgcx5gaYduxWsqABlxJb8YYeJOf44daTYK4BJDVFdV9pcAnQSSri3aJECWrIM

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




Archive powered by MHonArc 2.6.18.

Top of Page