At the core of Coq lies a purely functional language with a really funky type system. Before we delve into the logical aspects of the language, we go through a quick overview of Coq's syntax from the computational perspective.

Inductive definitions

In Coq, everything is either a function or data. All data is represented with inductive datatypes. The inductive datatypes of Coq are similar to the datatypes found in e.g. Haskell or ML, but they have more expressive power, as we shall eventually see.

There are no "primitive" data types in Coq. All data types, even numbers, are defined inductively in user-level code.

Booleans

We begin with the standard boolean type.

Inductive types are created with the Inductive command. A Coq source file is composed from a sequence of commands, each of them terminated with a period.

The above command introduces three new variables into the current scope: bool, the newly defined type, and true and false, the two constructors of the type. We can verify that both of them are of the type bool by using the Check command:

Now that we have defined the booleans, we can operate on them. Here is the basic negation operation:

There are a number of new things here. Firstly, a Definition command defines a new variable. Here we define the function negb which takes one parameter, b. In the body of the function, b is matched so that if b is true, we return false, and vice versa. In a match expression we must handle all the possible cases, after which the match expression must be terminated with the end keyword. In simple cases like this one, pattern matching works just like it does in Haskell or ML.

Pattern matching relies on the fact that Inductive creates the smallest type that has the given constructors. We know not only that true and false are in bool, but also that no other values are in bool. Hence, when our function handles both the case that b is true, and the case that b is false, it handles every possible b such that b : bool.

Incidentally, in the above definition we did not say that the type of b is bool. Coq can often infer types of variables when we don't give them explicitly. We can use the Check command to see the type that Coq inferred for negb.

In addition, the Print command can be used to show the entire definition of a variable:

In the following, we often leave out type annotations when they are obvious from the context both to Coq and (hopefully) the reader. Whenever you are uncertain, use the Check command to see the inferred types.

Function application

Function application is expressed with the plain juxtaposition syntax that is common in many functional languages: to apply function f to argument a, we simply write f a. In many contexts, though, surrounding parentheses are needed: (f a).

Notice that the Check command didn't evaluate the expression. In general, Coq doesn't evaluate anything until we explicitly request it. There are good reasons for this: our purpose is ultimately to reason about the terms, and evaluation doesn't always make reasoning easier.

We can ask Coq to show us the result of an evaluation with the Eval command:

We can also write multi-parameter functions:

Note the type:

This actually means bool -> (bool -> bool), i.e. a two-parameter function is actually an ordinary function that takes one parameter and returns a new function that takes another parameter.

The parameters in a Definition command are actually just syntactic sugar for a fun-expression, which creates a function that doesn't need to be named.

Finally, we can match multiple expressions at the same time, and we can also use the wildcard underscore _ that matches all the remaining cases:

Natural numbers

The boolean type is finite: there are only two elements, true and false. In general, we are much more interested in (potentially) infinite structures. The simplest of these is the type of natural numbers.

We use the standard formulation. There is a number O (zero), and for every number n, there is another number S n (the successor of n, or n + 1). So e.g. the number four would be written as S (S (S (S O))). The corresponding inductive data type is as follows:

We here enclosed the definition in a Module. This prevents it from shadowing Coq's standard definition of natural numbers, which is identical to this one, except that it has some special built-in syntactic support: we can use ordinary decimal numerals in expressions and Coq parses them as a repeated application of S to O. In particular, 0 is a synonym for O. In a similar fashion, Coq also prints values of type nat with ordinary numerals.

Sometimes Coq's syntactic conveniences can be confusing. They can be disabled with Set Printing All, and re-enabled with Unset Printing All.

In our definition of nat, we indicate that S is a constructor that takes a single nat as an argument by explicitly giving the full type of S. This is a bit different from common functional languages like Haskell or ML. In Haskell, we'd write the above as:

data Nat = O | S Nat

There is a good reason for the syntax that Coq uses for inductive definitions, since it can be generalized in ways that the Haskell style cannot. We shall see this later on.

As with booleans, we can operate on natural numbers using simple pattern matching. The following function returns the predecessor of a number, or O if the argument is 0:

Structural recursion

The number of things we can do on numbers with plain pattern matching is limited. To do anything really interesting, we have to have to use recursion over the structure of the numbers.

In Coq, recursive functions have to be explicitly declared as such with the Fixpoint command. An ordinary function defined with a Definition cannot call itself. Apart from the different keyword, the syntax of a recursive definition is outwardly the same.

The following function returns true if the argument is even, and false if it is odd:

We can also define multi-parameter functions such as addition and multiplication:

We can check that these indeed do what they're supposed to.

Comparing two numbers for equality is also straightforward: O and O are equal, and S n and S m are equal exactly when n and m are equal. S n and O are not equal.

There's a subtle but extremely important difference between Coq and ordinary programming languages regarding recursion. In Coq, the recursive call must be applied to a strictly smaller argument. That is, in the above definition of beq_nat, it's crucial that we pattern match on n to get n', which is structurally smaller than n, and apply the recursive call to n'.

Suppose we try to find the square root of a number n by searching through different values m, beginning from zero, until m * m = n. We would define it like this:


Fixpoint sqrt_aux m n :=
  match beq_nat (mult m m) n with
  | true => m
  | false => sqrt_aux (S m) n
  end.

Definition sqrt n := sqrt_aux O n.


However, Coq won't accept this definition, because S m, the recursive argument to sqrt_aux is not smaller than m, the original parameter.

We can still implement this function by searching downwards, from m to O:

We see that this indeed does the right thing:

However, we were forced to define our function so that if n is not the square of any natural number, then sqrt n evaluates to 0:

Thus, for any argument, our function will return something. When given a non-square number, it won't go into an infinite loop like the original version that would be rejected by Coq.

This, in fact, is one of the most fundamental differences between Coq and ordinary programming languages. Coq is a total language: the evaluation of every well-typed term will eventually terminate. There won't be any infinite loops, nor any run-time errors. This is absolutely essential for the logical aspects of Coq to work properly, but it also means that some kinds of programs become harder or even impossible to write.