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.

Why it’s so Hard for Imperative Programmers to Learn Functional Languages

Note: I wrote this entry about a year ago, and it got circulated around the internets for a little while. I'm reposting it here so I can have all of my "important" entries in one place.

I’m not currently using any functional languages like Haskell and Lisp, but I’m certainly comfortable with them. I’m certainly no Haskell guru, but I’m good enough to use higher-order functions, ADTs, monads, etc. While I have a good grasp of functional programming concepts now, I had to travel a long, hard road to get to this point.

Picture if you will a programmer with a C-family background discovering Haskell for the first time. He’s heard some smart people talk about how cool it is, and it says right there on haskell.org that it will substantially boost your productivity, so he momentarily puts down his Java Enterprise Web Framework With a Really Long Name and starts reading a Haskell tutorial.

At first, everything goes well. He’s impressed by the fact that you don’t have to constantly compile code to see the effects of your program. But after using the REPL as a calculator for a few minutes, he decides to check out how you write Hello World. This is where things start going downhill.

He notices that the chapter on I/O is tucked away in the Advanced section. Curiously, he flips to it and discovers, not an explanation of console and file I/O, but a disscussion of type classes, monads, and the like. He wonders if everything will make more sense if he just visits the appropriate chapters, but no luck; Haskell looks like one big incomprehensible mess. Our imperative programmer goes back to his Java Enterprise Framework, and that is the end of that.

It’s very difficult for a programmer used to imperative programming to find a good Haskell tutorial, or a good tutorial on any other functional language for that matter. It’s not that they explain Haskell badly; many of them explain it rather well. It’s just that they explain the wrong parts of Haskell. Procedural programmers are more often interested in how to do I/O and create GUIs rather than in how to use Parsec or write monads.

This is one of the major barriers to adoption of the more esoteric languages; lack of learning material for “normal people”. To rectify this, I thought about how I would write a Haskell tutorial.

I figured I would start off with a discussion about how to use the REPL to develop simple functions, and to test programs. From there, we would talk about how functions are side-effect free. We might take a detour into recursion, and then go on to topics such as monads and type classes. It would just be a Really Good Tutorial.

Then I realized something: in this great tutorial of mine, there were no sections on how to do I/O. There wasn’t even a Hello World program. Therein lies the problem.

The only people who can write a Haskell tutorial are the people who know Haskell. Ironically, someone who knows Haskell won’t be able to write a tutorial for the average programmer. They’ll focus too much on the features that make Haskell cool, rather than how to do practical things with it; which is just what the average programmer wants. Haskell gurus have spent so much time in their theoretical wonderlands, they’ve forgotten what it’s like to be an outsider.

We really need a Haskell, or Lisp, or ML tutorial aimed at the rest of the world, not just at functional gurus. Although I’m certainly not going to write it; I’ve got my own projects to worry about.