An Introduction to Coq: Part 1

Recently (as in, yesterday), I began playing around with Coq. I decided to write this quick tutorial to help people get started with Coq, since good documentation seems to be sparse, but it should be noted that I'm a Coq beginner myself, and this post may contain a factual error here and there.

Coq is a rather interesting piece of software. It is primarily designed to be an interactive theorem prover: you start by giving it a conjecture that you want to prove, called a Goal. You then use built-in commands called Tactics to simplify your Goal into Subgoals until it can be proven by your given Axioms.

Despite being a heavily theoretical tool, Coq can be used to create real programs that have some interesting properties. For example, you could define a function that wouldn't run until it was given a proof that showed it was correct.

Let's walk through a simple Coq session. We'll start by examining two built-ins, O and S:

Coq < Check O.
0
     : nat

Coq < Check S.
S
     : nat -> nat

Note that your input to Coq is terminated by a period.

As you can see, the Check command is used to examine the type of a constant. In this case, we see that O (the letter, not the number) is a natural number (zero to be precise), and S is a function that takes a natural number as an argument and returns a natural number.

Let's see if we can figure out what S is supposed to do:

Coq < Eval compute in S O.
     = 1
     : nat

Coq < Eval compute in S 1.
     = 2
     : nat

The first command tells us that S(O) returns 1 (which is of type nat), and S(1) returns 2 (also of type nat). S is the "succ" function: it increments its argument by 1. Symbols like 1 and 2 are just syntactic sugar in Coq; all numbers are formed by successive calls on S(O).

Suppose that we want to prove a very simple theorem: that S(O) is equal to S(O). To do that, we need to define an axiom:

Coq < Axiom NEquality:
Coq < forall n:nat, n = n.
NEquality is assumed

The first line simply states that we are defining an Axiom called NEquality. The second line is the axiom itself; in English, it says "for each natural number n, n is equal to n".

Now that Coq knows that each natural number is equal to itself, we can set about proving that S(O) = S(O):

Coq < Goal S O = S O.
1 subgoal

  ============================
   1 = 1

Unnamed_thm < 

What happened? When we stated that we had a Goal that we wanted to prove, Coq dropped us into the proof-editing mode. It then evaluated S(O) and told us that our current subgoal is proving 1 = 1. This fits perfectly with our axiom, so let's tell that to Coq:

Unnamed_thm < apply NEquality.
Proof completed.

Using the "apply" tactic to use our axiom on the current subgoal was all that was needed to finish the proof. Now we can save our theorem for later use:

Unnamed_thm < Save theorem1.
apply NEquality.
theorem1 is defined

Coq < 

That's the basic way of proving things in Coq: state a Goal and use tactics to prove each of the conjecture's subgoals.

Now we can try proving something a little bigger: S(x) = S(x).

First, we need to state that x is a natural number:

Coq < Parameter x : nat.
x is assumed

This just says "anywhere a natural number is expected, x can be used in its place". Note that we could have also used the Variable command.

Now we state our goal:

Coq < Goal S x = S x.
1 subgoal

  ============================
   S x = S x

And we can prove it using the congruence tactic:

Unnamed_thm < congruence.
Proof completed.

Congruence can be used wherever your Subgoal can be solved with a rewrite. In this case, the two S calls cancel out, and we're left with x = x.

That's all until Part 2. If you want to learn more about Coq, you should check out the Coq tutorial and the Coq reference manual.