Mercurial > cpdt > repo

comparison src/Intro.v @ 489:a95af5a59990

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Exercises online
author Adam Chlipala <adam@chlipala.net>
date Tue, 08 Jan 2013 15:48:32 -0500
parents 8bfb27cf0121
children da576746c3ba
comparison
equal deleted inserted replaced
488:31258618ef73 489:a95af5a59990
171 171
172 Readers with no prior Coq experience can ignore the preceding discussion! I hope that my heavy reliance on proof automation early on will seem like the most natural way to go, such that you may wonder why others are spending so much time entering sequences of proof steps manually. 172 Readers with no prior Coq experience can ignore the preceding discussion! I hope that my heavy reliance on proof automation early on will seem like the most natural way to go, such that you may wonder why others are spending so much time entering sequences of proof steps manually.
173 173
174 Coq is a very complex system, with many different commands driven more by pragmatic concerns than by any overarching aesthetic principle. When I use some construct for the first time, I try to give a one-sentence intuition for what it accomplishes, but I leave the details to the Coq reference manual%~\cite{CoqManual}%. I expect that readers interested in complete understanding will be consulting that manual frequently; in that sense, this book is not meant to be completely standalone. I often use constructs in code snippets without first introducing them at all, but explanations should always follow in the prose paragraphs immediately after the offending snippets. 174 Coq is a very complex system, with many different commands driven more by pragmatic concerns than by any overarching aesthetic principle. When I use some construct for the first time, I try to give a one-sentence intuition for what it accomplishes, but I leave the details to the Coq reference manual%~\cite{CoqManual}%. I expect that readers interested in complete understanding will be consulting that manual frequently; in that sense, this book is not meant to be completely standalone. I often use constructs in code snippets without first introducing them at all, but explanations should always follow in the prose paragraphs immediately after the offending snippets.
175 175
176 Previous versions of the book included some suggested exercises at the ends of chapters. Since then, I have decided to remove the exercises and focus on the main book exposition. Especially in the domain of interactive theorem proving, keeping exercises at the proper difficulty level is a lot of work, I have learned! My advice to readers is to learn to use Coq by getting started applying it in their own real projects, rather than focusing on artificial exercises. 176 Previous versions of the book included some suggested exercises at the ends of chapters. Since then, I have decided to remove the exercises and focus on the main book exposition. A database of exercises proposed by various readers of the book is #<a href="http://adam.chlipala.net/cpdt/ex/">#available on the Web#</a>#%\footnote{\url{http://adam.chlipala.net/cpdt/ex/}}%. I do want to suggest, though, that the best way to learn Coq is to get started applying it in a real project, rather than focusing on artificial exercises. *)
177 *)
178 177
179 (** ** On the Tactic Library *) 178 (** ** On the Tactic Library *)
180 179
181 (** 180 (**
182 To make it possible to start from fancy proof automation, rather than working up to it, I have included with the book source a library of _tactics_, or programs that find proofs, since the built-in Coq tactics do not support a high enough level of automation. I use these tactics even from the first chapter with code examples. 181 To make it possible to start from fancy proof automation, rather than working up to it, I have included with the book source a library of _tactics_, or programs that find proofs, since the built-in Coq tactics do not support a high enough level of automation. I use these tactics even from the first chapter with code examples.