coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Kenneth Adam Miller <kennethadammiller AT gmail.com>
- To: coq-club Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Force Principle Argument Recognition
- Date: Mon, 30 Nov 2015 11:16:33 -0500
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=kennethadammiller AT gmail.com; spf=Pass smtp.mailfrom=kennethadammiller AT gmail.com; spf=None smtp.helo=postmaster AT mail-yk0-f181.google.com
- Ironport-phdr: 9a23:wUDxGRNQWTO+EifgY08l6mtUPXoX/o7sNwtQ0KIMzox0KPTzrarrMEGX3/hxlliBBdydsKIZzbqG+PqwEUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35nxh7D5oc2bSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6LoJvvRNWqTifqk+UacQTHF/azh0t4XXskzIShLK7X8BWC09lgdCS1zO6wi/VZPsuAP7sPB80W+UJ5ulY6ozXGGB4qFtRQPowA4LPjtx1WDTjsFqxPZYrRSnqgB/yoLdZYSUMP5zZIvSeNobQSxKWcMHBH8JOZ+1c4ZaV7lJBu1ftYSo4gJW9RY=
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
- [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.