The Coq Proof Assistant

Table of Contents

1 Proof Assistants

At its most basic level, a proof assistant consists of

  • a DSL (Domain-Specific Language) representing logical objects, as well as definitions and theorems about these objects
  • a software platform for interactively constructing and validating these definitions and proofs.

At more advanced levels, the proof assistant can be “taught” to automate some of the steps of the proofs.

Proof assistants are for theories what calculators are for arithmetic problems. They do not obviate the need for understanding, but help raise it to a higher level of rigour.

1.1 Benefits to researchers

  • Factor out the correctness of the proofs out of your papers: Some reviewers don't have the time or the patience to follow your proofs, others don't really understand them. By using a proof assistant to code proofs, correctness becomes a non-issue. Instead, the researcher can focus on presentation, intuition, and the high-level structure of the proofs, and provide a URL to the proof files for the interested reviewers and reader. This lets the reviewers know that the proofs are correct, and allows them to verify the correctness.
  • Because the details of the proofs can be relegated to an appendix, or to a file the URL of which is quoted in the paper, the paper can shrink in size to fit the tight page-limits some conferences and journals impose.
  • By making the proof files available to readers, a researcher can help others to continue developing on his or her work. The proof files, which can be as short as small as a single proof, or as large as an entire theory, are a genuine contribution to the scientific community.

1.2 Benefits to instructors

In theory courses, the teaching staff must spend a lot of time communiating formally with students, teaching students to communicate formally, and evaluating and grading student work. Today, courses of 250-500 students are common, but the resources to teach and evaluate students in a course have not grown proportionately. This means that instruction is de-personalized, and graders can spend less time trying to follow and evaluate student work. Put otherwise, there is no way to grade thoroughly the work of hundreds of students, with the number of graders and in the timeframe allotted. The quality of grading has declined: It takes longer, there is less feedback, and the grading is sloppier.

Using a proof assistant for homework assignments changes the game entirely:

  • Students can see examples of air-tight, formal proofs, and can follow them, understanding the contribution of each step to the overall proof.
  • Instructors can provide students with skeleton proofs, with the definitions, and statements of the lemmas and proofs already in place (if they so wish). The students can then fill in the details, and see how their proof comes to life.
  • When students submit their proofs, they already know whether the proofs are correct or not. Verifying correctness is trivial.
  • The students can receive instantaneous feedback from the proof assistant.
  • The proofs are all typed up, in text format. It is easy to verify them mechanically, or even manually. It is easier to detect cheating.
  • The correctness of the proofs can be factored out of the homework easily and quickly. If the assignment is to prove some theorem, the graders can focus on the structure, aesthetics, and economy of the proofs, i.e., what kinds of lemmas were used, and how they all fit together.
  • The tediousness of evaluating proofs manually encourages students to write impossibly-long, illegible proofs, in the hope that the grader will give them the benefit of the doubt and just assume their proofs are correct. When a proof is encoded formally using a proof assistant, there is a bottom line, and it is the proof assistant that the student has to convince. No matter how long and how tedious the proof, the student will not be able to get pass the proof assistant unless the proof is correct.
  • The use of proof assistants opens the door towards exciting new ways of teaching. For example, it is possible to divide an assignment among students, each student “in charge” of proving some theorems, and for the total result to be a substantial, meaningful, collaborative work.

1.3 Benefits to students

  • Feedback on assignments often reaches students very late, often too late to be of value. By using a proof assistant, students get instant, meaningful feedback on their ideas. Proof assistants are infinitely patient, very quick, and very pedantic. They are suitable for remote learning and self-learning.
  • Human graders, often in a rush to finish grading, come with pre-conceived notions as to how some result can be proven. This can make them impatient or intolerant of different though correct proofs. With proof assistants, students need not fear that their graders misunderstood their proofs: If their proofs are correct, then the proof assistant will accept it, and so should the human grader.
  • Proof assistants facilitate better, deeper, more meaningful, and more productive interaction with the teaching staff: Rather than saying I have no clue how to prove this, students can try, and when they get stuck, email the proof file to their teaching staff, who can run it through the proof assistant, and suggest how to continue: either add some lemmas, or otherwise re-structure the proof. For example, an instructor may provide the proof of the theorem, based on some lemmas which are left unproven. The student can then try to fill in the proofs for these lemmas.
  • Interacting with a proof assistant is a great way to learn, because they force clarity and precision, and because they verify truth. My own [yet brief] experience with the Coq proof assistant has been very surprising in that respect. While I certainly understood much about the theories I tried to describe in Coq, the experience of encoding them revealed many subtle issues that I had hand-waived away. A proof assistant forces the student to become aware of all the subtleties, all the wrinkles, all the special cases and exceptions, and handle them, one-by-one, until a proof is really complete. The immediate effect on me has been a much greater clarity about what are the real issues in some theory.

2 Online Resources

2.1 The toolset & documentation

  • The Coq system
  • CoqIDE: The default IDE for constructing proofs using Coq. IDE that comes with the Coq system. It is provided for Linux, OSX, and even for MS Windows.
  • The Proof General: An emacs package for working with several proof assistants, including Coq. This is an IDE for constructing proofs using Coq. For emacs users, this is a great alternative to the CoqIDE system. Put otherwise, you should use the Proof General over the Coq IDE unless you absolutely refuse to use Emacs under any circumstances. The Proof General will make you a much more productive Coq user.
  • The coqdoc utility: A utility for converting .v files into HTML, PDF, or any other useful format. Check out the options, by issuing coqdoc --help. Some useful options are --pdf (to generate PDF files), --parse-comments (to include comments in the .v files — I have no idea why this isn't on by default), and -l (for removing the proofs of the theorems and lemmas from the target/output document). The last option is useful, because Coq is a tool for creating proofs interactively, and the details of the proof make more sense when you verify them in CoqIDE or the Proof General. The way I use coqdoc is via a makefile that contains a rule for converting .v files into corresponding .pdf files. Here's a copy of my makews-file:
.SUFFIXES:      .pdf .v

%.pdf:  %.v makefile
        coqdoc --pdf --parse-comments -l -o $*.pdf $*.v
  • Coq Graphs: A tool for visualizing whole files, or just a single proof. Creates a directed graph in dot, which is a part of the Graphviz package. Apparently, this tool is no longer maintained, which is a shame!

3 My own examples of using Coq

4 Useful imports

  • Require Import List. To work with lists.
  • Require Import Setoid. Needed to use the rewrite tactic.
  • Require Import Arith. Needed for doing basic arithmetic.
  • Require Import Ascii.
  • Require Import ClassicalFacts. Needed for proving statements using classical (as opposed to intuitionistic) logic. Defines such things as the law of the excluded middle, propositional extensionality, etc.

Date: 2013-07-27T16:10+0300

Validate XHTML 1.0