Let's do the exercises in the first chapter of "Software Foundations" (by Benjamin Pierce and a whole bunch of other people) and then get together and discuss it.
You'll need to do a fair amount of system administration before you get started:
. downloading the book . installing Coq . installing emacs . installing the Proof General plugin for emacs
Also strongly recommended is to download a copy of Adam Chilpala's "Certified Programming with Dependent Types"; I would skim through the first two chapters before starting with Software Foundations, because Chilpala gives an overview of how Coq is put together and what Coq can do that makes the beginning of Software Foundations a lot less mysterious.
. Download Software Foundations (henceforth "SF") from http://www.cis.upenn.edu/~bcpierce/sf/ (I'm not aware of a paper edition). Untarring it gives you a directory of .html files (browsable) and .v files, which are the literate Coq source files for the book. In order to do the exercises, you actually modify the .v files.
The chapters in SF aren't numbered and vary in length, but the first real chapter (the one we're doing for this meeting) is the one titled "Basics: Functional Programming in Coq".
. Install Coq from http://coq.inria.fr/download (current version is 8.4pl3).
You can interact with Coq using coqtop on the command line, or through Proof General in an emacs buffer. Because most things you do with Coq are many lines long, coqtop isn't very helpful unless you want to do something really simple.
. Install emacs (if you don't already have it; from http://www.gnu.org/software/emacs/). You'll want version 23.3 or later (current version is 24.3) for compatibility with Proof General.
If you haven't used emacs before, I'm afraid this may be a bit of a culture shock. emacs probably has modes that emulate almost any text editor you might be familiar with, but I'm afraid I don't know much about them.
. Install Proof General from http://proofgeneral.inf.ed.ac.uk/download (current version is 4.2). Note that you have to edit your ~/emacs.d file to make emacs able to find Proof General, so follow all the installation instructions!
I've found the Proof General documentation to be rather unapproachable, but so far there's really only one command I've needed. To get Proof General to process a Coq source buffer, position your cursor in the buffer at the point up to which you'd like Proof General to run Coq, and type CTRL-C CTRL-ENTER.
. Chilpala's "Certified Programming with Dependent Types" is available in both paper and PDF editions (the PDF is free!) from http://adam.chlipala.net/cpdt/ .