coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 |
- [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
- Re: [Coq-Club] Force Principle Argument Recognition, Emma Tosch, 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, Soegtrop, Michael, 11/30/2015
Archive powered by MHonArc 2.6.18.