using the ProofGeneral plugin for Emacs. I'll also provide detailed
instructions for installing the three components on Ubuntu 11.10.
Coq is two things in one: a rather esoteric programming language and
proof assistant. The programming language is somewhat similar to
(Oca)ML and Haskell. The proof assistant allows to write formal
mathematical proofs that the computer automatically checks. More
interestingly, the proof assistant can be used to reason about
programs written in Coq itself.
Coq can be invoked either as a REPL (like the one in Python, Ocaml,
Haskell or Scheme) called coqtop or as a compiler called coqc that
turns coq source files (usually stored in .v files) into coq object
files (stored in .vo files) containing machine-checked proofs.
However, the best way to develop in Coq is by using an advanced editor
(we will be using Emacs) which can interact with the coq toplevel
(coqtop). This allows to combine the advantages of an editor (moving
source code around, moving around source code) with the advantages of
the REPL (checking if code works).
Emacs is an advanced, highly customizable and somewhat esoteric
editor. People who use it are usually very proficient at text editing
due to its streamlined non-standard interface. This tutorial does not
advocate the use of Emacs throughout, but I do think that it provides
the best interface for editing Coq developments.
Emacs itself cannot talk to the Coq REPL and it needs a plugin called
ProofGeneral which can do this. In fact ProofGeneral is a more general
plugin which enables Emacs to talk to proof assistants other than Coq,
but we will use it here only for Coq.
Under Ubuntu 11.10, to install everything you need, the single command
line:
sudo apt-get install emacs coq proofgeneral proofgeneral-doc
proofgeneral-coq
will do the trick. On Ubuntu 11.10, this will install Coq 8.3pl2,
ProofGeneral 3.7 and Emacs 23.3.1.
The proofgeneral package helpfully includes a command
/usr/bin/proofgeneral that will start Emacs with the ProofGeneral
plugin already loaded. Therefore, assuming that /usr/bin is in your
PATH variable, you can issue the command:
proofgeneral
to start up your environment (Emacs w/ the ProofGeneral plugin).
To open a file (or "visit" a file in Emacs-speak) where you save your
Coq development, type C-x C-f (this means keep the control key pressed
while typing 'x', following by the same action with 'f' instead of
'x'). Type the name of the file you want to open (let's say the
filename is "test1.v") followed by Enter. By convention, Coq files end
with the extension ".v".
Next type in the following Coq code:
Inductive bool : Set :=
| true
| false.
Theorem bool_only : forall b : bool, b = true \/ b = false.
intros.
destruct b.
constructor 1. reflexivity.
constructor 2. reflexivity.
Qed.
This Coq code defines an inductive data type "bool" much like an ADT
in Ocaml or Haskell (or in this simple case like an enum in
C/C++/Java). The data type contains (exactly) two constructors "true"
and "false". Then a trivial theorem is proven showing that any value
of this type is either "true" or "false".
To run the above code in Coq up to a certain point, you should move
the cursor up to that point (say immediately after a command ending
with a ".") and type C-c C-ENTER. This command will send the code to
coqtop, which will start up and reply in a different window (the Emacs
screen will split into two -- one part with your code and the other
part where coqtop writes the response). To send the remainder of the
code to coqtop, go to the end of the file and type C-c C-ENTER.
To save the file, type C-x C-s. To exit Emacs, type C-x C-c. If you
find yourself issuing an Emacs command by mistake and you don't know
how to continue, usually C-g (you may press it several times) will get
you out and back to editing the file. I encourage you to find more
about Emacs by typing C-h t (control + "h", following by "t" (without
control)), which will open the Emacs tutorial.
To learn Coq, I suggest taking a look at the official Coq
documentation: http://coq.inria.fr/documentation.
