Mercurial > cpdt > repo

comparison src/Intro.v @ 311:4cb3ba8604bc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass through first half of StackMachine, along with some reorganization of the build process
author Adam Chlipala <adam@chlipala.net>
date Mon, 29 Aug 2011 15:31:06 -0400
parents d2cb78f54454
children 495153a41819
comparison
equal deleted inserted replaced
310:cf67b7d6ceac 311:4cb3ba8604bc
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (** %\fi 10 (** %\chapter{Introduction}% *)
11
12 \usepackage{makeidx,hyperref}
13
14 \title{Certified Programming with Dependent Types}
15 \author{Adam Chlipala}
16
17 \makeindex
18
19 \begin{document}
20
21 \maketitle
22
23 \thispagestyle{empty}
24 \mbox{}\vfill
25 \begin{center}% *)
26
27 (**
28
29 Copyright Adam Chlipala 2008-2011.
30
31 This work is licensed under a
32 Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
33 Unported License.
34 The license text is available at:
35 %\begin{center} \url{http://creativecommons.org/licenses/by-nc-nd/3.0/} \end{center}%
36 #<a href="http://creativecommons.org/licenses/by-nc-nd/3.0/">http://creativecommons.org/licenses/by-nc-nd/3.0/</a>#
37
38 *)
39
40 (** %\vfill\mbox{}
41 \end{center}
42
43 \phantomsection
44 \tableofcontents
45
46 \chapter{Introduction}% *)
47 11
48 12
49 (** * Whence This Book? *) 13 (** * Whence This Book? *)
50 14
51 (** 15 (**
209 (** ** On the Tactic Library *) 173 (** ** On the Tactic Library *)
210 174
211 (** 175 (**
212 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 %\emph{%#<i>#tactics#</i>#%}%, 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. 176 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 %\emph{%#<i>#tactics#</i>#%}%, 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.
213 177
214 Some readers have asked about the pragmatics of using this tactic library in their own developments. My position there is that this tactic library was designed with the specific examples of the book in mind; I do not recommend using it in other settings. Part III should impart the necessary skills to reimplement these tactics and beyond. One generally deals with undecidable problems in interactive theorem proving, so there can be no tactic that solves all goals, though the %\index{Tactics!crush@\texttt{crush}}%[crush] tactic that we will meet soon may sometimes feel like that! There are still very useful tricks found in the implementations of [crush] and its cousins, so it may be useful to examine the commented source file %\texttt{%#<tt>#Tactics.v#</tt>.#%}.~\footnote{It's not actually commented yet. \texttt{;-)}}% I implement a new tactic library for each new project, since each project involves a different mix of undecidable theories where a different set of heuristics turns out to work well; and that is what I recommend others do, too. 178 Some readers have asked about the pragmatics of using this tactic library in their own developments. My position there is that this tactic library was designed with the specific examples of the book in mind; I do not recommend using it in other settings. Part III should impart the necessary skills to reimplement these tactics and beyond. One generally deals with undecidable problems in interactive theorem proving, so there can be no tactic that solves all goals, though the %\index{tactics!crush}%[crush] tactic that we will meet soon may sometimes feel like that! There are still very useful tricks found in the implementations of [crush] and its cousins, so it may be useful to examine the commented source file %\texttt{%#<tt>#Tactics.v#</tt>.#%}.~\footnote{It's not actually commented yet. \texttt{;-)}}% I implement a new tactic library for each new project, since each project involves a different mix of undecidable theories where a different set of heuristics turns out to work well; and that is what I recommend others do, too.
215 *) 179 *)
216 180
217 (** ** Installation and Emacs Set-Up *) 181 (** ** Installation and Emacs Set-Up *)
218 182
219 (** 183 (**