## 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. |