Enumerated Types

In Coq's programming language, almost nothing is built in -- not even booleans or numbers! Instead, it provides powerful tools for defining new types of data and functions that process and transform them.

Days of the Week

Let's start with a very simple example. The following declaration tells Coq that we are defining a new set of data values -- a "type." The type is called day, and its members are monday, tuesday, etc. The lines of the definition can be read "monday is a day, tuesday is a day, etc."

Having defined day, we can write functions that operate on days.

One thing to note is that the argument and return types of this function are explicitly declared. Like most functional programming languages, Coq can often work out these types even if they are not given explicitly -- i.e., it performs some type inference -- but we'll always include them to make reading easier. Having defined a function, we should check that it works on some examples. There are actually three different ways to do this in Coq. First, we can use the command Eval simpl to evaluate a compound expression involving next_weekday. Uncomment the following and see what they do.

If you have a computer handy, now would be an excellent moment to fire up the Coq interpreter under your favorite IDE -- either CoqIde or Proof General -- and try this for yourself. Load this file (Basics.v) from the book's accompanying Coq sources, find the above example, submit it to Coq, and observe the result. The keyword simpl ("simplify") tells Coq precisely how to evaluate the expression we give it. For the moment, simpl is the only one we'll need; later on we'll see some alternatives that are sometimes useful. Second, we can record what we expect the result to be in the form of a Coq example:

The details are not important for now (we'll come back to them in a bit), but essentially this can be read as "The assertion we've just made can be proved by observing that both sides of the equality are the same after simplification." Third, we can ask Coq to "extract," from a Definition, a program in some other, more conventional, programming language (OCaml, Scheme, or Haskell) with a high-performance compiler. This facility is very interesting, since it gives us a way to construct fully certified programs in mainstream languages. Indeed, this is one of the main uses for which Coq was developed. We won't have space to dig further into this topic, but more information can be found in the Coq'Art book by Bertot and Castéran, as well as the Coq reference manual.

Booleans

In a similar way, we can define the type bool of booleans, with members true and false.

Although we are rolling our own booleans here for the sake of building up everything from scratch, Coq does, of course, provide a default implementation of the booleans in its standard library, together with a multitude of useful functions and lemmas. (Take a look at Coq.Init.Datatypes in the Coq library documentation if you're interested.) Whenever possible, we'll name our own definitions and theorems so that they exactly coincide with the ones in the standard library. Functions over booleans can be defined in the same way as above:

The last two illustrate the syntax for multi-argument function definitions. The following four "unit tests" constitute a complete specification -- a truth table -- for the orb function:

A note on notation: We use square brackets to delimit fragments of Coq code in comments in .v files; this convention, also used by the coqdoc documentation tool, keeps them visually separate from the surrounding text. In the html version of the files, these pieces of text appear in a different font. The following bit of Coq hackery defines a magic value called admit that can fill a hole in an incomplete definition or proof. We'll use it in the definition of nandb in the following exercise. In general, your job in the exercises is to replace admit or Admitted with real definitions or proofs.

Exercise: 1 star (nandb)

Complete the definition of the following function, then make sure that the Example assertions below each can be verified by Coq. This function should return true if either or both of its inputs are false.

Remove "Admitted." and fill in each proof with "Proof. simpl. reflexivity. Qed."

☐

Exercise: 1 star (andb3)

☐

Function Types

The Check command causes Coq to print the type of an expression. For example, the type of negb true is bool.

Functions like negb itself are also data values, just like true and false. Their types are called function types, and they are written with arrows.

The type of negb, written bool -> bool and pronounced "bool arrow bool," can be read, "Given an input of type bool, this function produces an output of type bool." Similarly, the type of andb, written bool -> bool -> bool, can be read, "Given two inputs, both of type bool, this function produces an output of type bool."

Numbers

Technical digression: Coq provides a fairly fancy module system, to aid in organizing large developments. In this course, we won't need most of its features, but one of them is useful: if we enclose a collection of declarations between Module X and End X markers, then, in the remainder of the file after the End, all these definitions will be referred to by names like X.foo instead of just foo. This means that the new definition will not clash with the unqualified name foo later, which would otherwise be an error (a name can only be defined once in a given scope). Here, we use this feature to introduce the definition of the type nat in an inner module so that it does not shadow the one from the standard library.

The types we have defined so far are examples of "enumerated types": their definitions explicitly enumerate a finite set of elements. A more interesting way of defining a type is to give a collection of "inductive rules" describing its elements. For example, we can define the natural numbers as follows:

The clauses of this definition can be read:

• O is a natural number (note that this is the letter "O," not the numeral "0").
• S is a "constructor" that takes a natural number and yields another one -- that is, if n is a natural number, then S n is too.

Let's look at this in a little more detail. Every inductively defined set (weekday, nat, bool, etc.) is actually a set of expressions. The definition of nat says how expressions in the set nat can be constructed:

• the expression O belongs to the set nat;
• if n is an expression belonging to the set nat, then S n is also an expression belonging to the set nat; and
• expressions formed in these two ways are the only ones belonging to the set nat.

These three conditions are the precise force of the Inductive declaration. They imply that the expression O, the expression S O, the expression S (S O), the expression S (S (S O)), and so on all belong to the set nat, while other expressions like true, andb true false, and S (S false) do not. We can write simple functions that pattern match on natural numbers just as we did above -- for example, predecessor: