Mercurial > cpdt > repo
comparison src/Intro.v @ 389:76e1dfcb86eb
Comment CpdtTactics.v
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Thu, 12 Apr 2012 18:41:32 -0400 |
| parents | 9e47cdd76bb5 |
| children | d40b05266306 |
comparison
equal
deleted
inserted
replaced
| 388:057a29f9c773 | 389:76e1dfcb86eb |
|---|---|
| 175 (** ** On the Tactic Library *) | 175 (** ** On the Tactic Library *) |
| 176 | 176 |
| 177 (** | 177 (** |
| 178 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. | 178 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. |
| 179 | 179 |
| 180 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>#CpdtTactics.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. | 180 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>#CpdtTactics.v#</tt>.#%}.% 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. |
| 181 *) | 181 *) |
| 182 | 182 |
| 183 (** ** Installation and Emacs Set-Up *) | 183 (** ** Installation and Emacs Set-Up *) |
| 184 | 184 |
| 185 (** | 185 (** |