annotate src/Conclusion.v @ 384:eb0fa506d04c
Strengthen last theorem of Coinductive
| author |
Adam Chlipala <adam@chlipala.net> |
| date |
Sun, 08 Apr 2012 11:11:27 -0400 |
| parents |
e2c88317611f |
| children |
5986e9fd40b5 |
| rev |
line source |
|
adam@383
|
1 (* Copyright (c) 2012, Adam Chlipala
|
|
adam@383
|
2 *
|
|
adam@383
|
3 * This work is licensed under a
|
|
adam@383
|
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
|
|
adam@383
|
5 * Unported License.
|
|
adam@383
|
6 * The license text is available at:
|
|
adam@383
|
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
|
|
adam@383
|
8 *)
|
|
adam@383
|
9
|
|
adam@383
|
10 (** %\addcontentsline{toc}{chapter}{Conclusion}\chapter*{Conclusion}% *)
|
|
adam@383
|
11
|
|
adam@383
|
12 (** I have designed this book to present the key ideas needed to get started with productive use of Coq. Many people have learned to use Coq through a variety of resources, yet there is a distinct lack of agreement on structuring principles and techniques for easing the evolution of Coq developments over time. Here I have emphasized two unusual techniques: programming with dependent types, and proving with scripted proof automation. I have also tried to present other material following my own take on how to keep Coq code beautiful and scalable.
|
|
adam@383
|
13
|
|
adam@383
|
14 Part of the attraction of Coq and similar tools is that their logical foundations are small. A few pages of %\LaTeX{}%#LaTeX# code suffice to define CIC, Coq's logic, yet there do not seem to be any practical limits on which mathematical concepts may be encoded on top of this modest base. At the same time, the %\emph{%#<i>#pragmatic#</i>#%}% foundation of Coq is vast, encompassing tactics, libraries, and design patterns for programs, theorem statements, and proof scripts. I hope the preceding chapters have given a sense of just how much there is to learn before it is possible to drive Coq with the same ease with which many readers write informal proofs! The pay-off of this learning process is that many proofs, especially those with many details to check, become much easier to write than they are on paper. Further, the truth of such theorems may be established with much greater confidence, even without reading proof details.
|
|
adam@383
|
15
|
|
adam@383
|
16 As Coq has so many moving parts to catalogue mentally, I have not attempted to describe most of them here; nor have I attempted to give exhaustive descriptions of the few I devote space to. To those readers who have made it this far through the book, my advice is: read through the Coq manual, front to back, at some level of detail. Get a sense for which bits of functionality are available. Dig more into those categories that sound relevant to the developments you want to build, and keep the rest in mind in case they come in handy later.
|
|
adam@383
|
17
|
|
adam@383
|
18 In a domain as rich as this one, the learning process never ends. The Coq Club mailing list (linked from the Coq home page) is a great place to get involved in discussions of the latest improvements, or to ask questions about stumbling blocks that you encounter. (I hope that this book will save you from needing to ask some of the most common questions!) I believe the best way to learn is to get started using Coq to build some development that interests you.
|
|
adam@383
|
19
|
|
adam@383
|
20 Good luck! *)
|
