Here are some resources for programmers who want to get started with Coq:
- Coq is best used as an interactive theorem prover. When you’re learning,
you’ll want to be able to jump back and forth between the steps in your proof
scripts, comment them out etc. To be able to do that, I recommend that you use
CoqIDE instead of your usual editor and the REPL (
coqtop). CoqIDE is not the best editor out there, but it supports proof navigation and it’s easy to set up. In case your usual editor is Emacs, you can use Proof General as well. - The best tutorial out there is the book Software Foundations by Benjamin C. Pierce et al. It’s the best because it has such a good set of exercises. To start learning Coq, start working through those exercises.
- I’ve found Adam Chlipala’s Certified Programming with Dependent Types useful as well. CPDT places more emphasis on using powerful proof automation than SF. My gut feeling is that SF teaches you what’s going on and CPDT teaches you how to do things in practice.
- Another interesting text for beginners is Ilya Sergey’s Programs and Proofs. Instead of plain Coq, it uses Ssreflect, an extension of Coq that was developed for implementing large mathematical proofs. I’ve used Ssreflect only a bit but it looks powerful.
- Finally, you’ll want to keep the Coq reference manual, esp. the tactics chapter, and the standard library docs at hand.
I’ve also read parts of the Coq’Art book, but I didn’t get much out of it, so I wouldn’t recommend that.