Mercurial > cpdt > repo

comparison src/Intro.v @ 370:549d604c3d16

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Move exercises out of mainline book
author Adam Chlipala <adam@chlipala.net>
date Fri, 02 Mar 2012 09:58:00 -0500
parents 3322367e955d
children f7c2bf7f1324
comparison
equal deleted inserted replaced
369:4550dedad73a 370:549d604c3d16
1 (* Copyright (c) 2008-2011, Adam Chlipala 1 (* Copyright (c) 2008-2012, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
167 167
168 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. 168 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.
169 169
170 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 understandings 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. 170 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 understandings 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.
171 171
172 Most chapters end with suggested exercises. Some exercises marked with %``$\star$''%#"star"# are especially difficult or deal with especially advanced subjects that the reader may not wish to master on a first reading. 172 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.
173 *) 173 *)
174 174
175 (** ** On the Tactic Library *) 175 (** ** On the Tactic Library *)
176 176
177 (** 177 (**