CIS 500: Coq Resources

Running Coq on SEAS Systems

On any SEAS Linux machine, including the ones in the labs (Moore 100A, 100C, and 207), you should be able to start up CoqIDE by typing something like this at a command prompt:

         coqide Basics.v
      

Using CoqIDE

The CoqIDE user interface is pretty self-explanatory. Use the up/down buttons at the top of the window to send parts of your proof script to Coq for processing (down) or to retract parts that have already been sent so that you can edit them again (up).

Documentation

The main Coq page includes a comprehensive reference manual, an FAQ, and pointers to some other useful resources.

For those who wish to go deeper with Coq, the Coq'Art book Interactive Theorem Proving and Program Development, by Yves Bertot and Pierre Castéran is recommended, as is Adam Chlipala's Certified Programming with Dependent Types.

Installing Coq on your own machine

Easy-install packages are available from the Coq download page. You should install version 8.4.

Note that you'll need both Coq itself and some development environmnent -- either CoqIDE (try this first, since it is simpler to use, but may be tricky to install on some platforms) or Proof General for emacs.

Using ProofGeneral

There are only a few commands you need to know to use ProofGeneral effectively. They are:

• C-c C-n: send the next command to Coq.
• C-c C-u: undo (retract) the most recently executed command.
• C-c C-RET: submit everything up to the current cursor location to Coq for processing.
• C-c C-. : move the cursor to the end of the last command which has been processed by Coq.
• C-c . : toggle "electric terminator mode". When this mode is turned on, simply typing a period will send the current command to Coq (normally you have to type a period and then type C-c C-n).