TP0: A First Step into
the Coq Proof Assistant

Aim of this self-taught first experiment with Coq

The aim of this "TP0" is to have you start in a "empirical" way to use the Coq proof assistant:

• first by executing some Coq code and observing the behaviour of the proof assistant and
• have you start writing your first definitions, theorems and proofs in Coq by adapting the code provided.

The most important thing to keep in mind is that we will come back to all this material in the next lecture and the following ones: if it looks difficult to you, if you cannot solve the exercises proposed here, it is not a problem at all: this is just to propose you to enter your learning phase about Coq in an autonomous way, doing things at your speed, experimenting additional things if it the appropriate time for you, etc. The Coq file supporting this TP is available at https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/TP/TP0.v. More generally, the Coq documents and related material will be available on this gitlab repository also linked from the main course webpage.

Installing Coq

Installing instruction are available on the Coq website: https://coq.inria.fr/download I recommend that you follow the recommended installation method (top of the webpage). Once Coq is installed, you may opt for various ways interacting with the proof assistant (see below). While using coqide or jsCoq do not require any additional installation, if you consider using emacs with the proofgeneral mode or VSCode, you will find relevant information on their installation in the page linked below: https://coq.inria.fr/user-interfaces.html

Getting Documentation about Coq

There is a large body of documentation on the Coq proof assistant. In this paragraph, I list some of it but I do not recommend that you immediately dive into this documentation. The course will start smoothly and you might experience some frustration otherwise. On the other hand, I suggest that you get familiar with the structure of the reference manual and od the documentation of the standard library as you will have to start using them in some weeks:

• Reference manual
• Documentation of the standard library
• More documentation.

Launching Coq

There are several ways to use Coq:

• via coqide, a graphical interface based on gtk
• via proofgeneral, which is a plugin for emacs
• via VSCode
• directly in a browser via jsCoq, for instance https://jscoq.github.io/node_modules/jscoq/examples/scratchpad.html (see https://github.com/ejgallego/jscoq for usage instructions)
• or perhaps via coqtop, a read-eval-print loop (repl) which is quite bare, similar to the ocaml interactive loop.

Each method has its advocates (even the last one...). The coq source files are always named with .v as extension (for "vernacular"...). After launch, both coqide and proofgeneral and jsCoq provide interfaces with a similar layout :

• the file being edited is in the left half of the screen,
• while proofs in progress are in right top and
• system messages are in right bottom (Coq answers, error messages, etc).

In the source file, colors are used to indicate which part of the file has already been processed by Coq, and this colored zone will grow when we send more phrases to Coq. Conversely the colored zone may also shrink if we "undo" and get Coq back to some earlier state. With coqide and jsCoq, the navigation shortcuts are almost the same: Ctrl+Down / Ctrl+Up or Alt+Down / Alt+Up to go forward or backward in the file. It is also possible to ask Coq to check the file till your cursor, or till the end of the file. (You can also use the corresponding buttons, but you will soon notice that the shortcuts are very convenient!)

Today's program

First, you should download the Coq file of the TP0 linked above in this page. (The html page of the TP0 is automatically generated from the TP0.v file thanks to a tool called coqdoc. You can go back and forth between the two documents: reading will be smoother in the html page while the .v file can be played in coqide, jscoq, or your prefered IDE, standing for integrated development environment.) Then, open this TP0.v file in your IDE or copy/paste it in jscoq if you prefer using jscoq scratchpad for now. You will notice immediately that Coq comments are written between : everything that is between those signs will be ignored by Coq. It will usually be presented in your IDE with a different font / color to make it easier to distinguish from the actual code. Today, you will mostly experiment the following commands:

• Definition : binds some name with a (non-recursive) Coq term
• Fixpoint : same, for a recursive definition
• Inductive : creates a new inductive type and its constructors
• Check : displays the type of a Coq term
• Print : displays the body of a definition or the details of an inductive type
• Compute : reduces a term (i.e. determines its normal form) and prints it.

A dot . is mandatory to end each Coq phrase. This experiment will consist mostly in playing this Coq file in you IDE and adding some variants when requested. (feel free to test more variants if you want!) I also advise you to take notes about the questions you may have while playing the document: you can either keep a separate file, or add your own comments in your file, it is up to you.

What is not in today's program

Essentially, today is mostly an experiment for you. The present files do not contain formal concepts introduced rigorously, nor theoretical results. We will see this in class over the semester. Also keep in mind that this course aims at two things:

• introducing your to functional programming with Coq
• introducing your to the use of a proof assistant to

"mechanize" proofs. Indeed, Coq as a concrete instance of the Curry-Howard correspondance, is both a programming language and a logic system in which one can write proofs by interacting with Coq IDE. ALso, since the first weeks of the course will focus on programming concepts, the present TP essentially introduces some of those programming ideas: the "proof assistant" part is neglected here (except in the very end of the TP so that you can have a first feeling of a very elementary theorem statement and proof) and will be introduced later: be patient!

First Terms and (Data) Types

In Coq, one builds terms and types. One shall study progressively what are the legal terms and types. This is quite intricate indeed due to the huge expressiveness of Coq framework and its underlying logic, the Calculus of Inductive Constructions, CIC. (Optional, you may skip this at the moment: In particular the use of dependent types, by which we mean that types can depend on terms.) As most recent functional programming languages (e.g OCaml), Coq is strongly typed : the non-well-typed terms will be rejected in Coq during type-checking, that is before running a computation. Coq is functional, in the sense that one of the basic computational constructions is that of a function: in the start of the lectures, the type of a (total) function taking objects from a type a and returns results in b is written a -> b The whole point of Coq is actually to check that the expressions given by the user can indeed be given a type (or: have the type theu user pretends they have). The hear of Coq is that of type-checking. In today's work, we will keep an intuitive (and naive) notion of types, that will be explained and refined in the next lectures. Before turning back to functions, let us first consider two very important types of Coq: the types of booleans and of natural numbers.

bool

Coq provides a type bool and constants true and false:

There is a construction if ... then ... else ..., as well as some predefined boolean operations :

• negation : negb
• logical "and" : andb (syntax &&, after doing Open Scope bool_scope)
• logical "or" : orb (syntax ||, after doing Open Scope bool_scope)

We can also compute, or evaluate, such an expression, which should return a boolean value (this is different from checking its type, in the previous line, which did not involve computing the boolean value):

Exercise 1 :

Write four distinct boolean expressions using negb, andb and orb, including one which uses the three functions at the same time. Check their type and compute their boolean value.

Once one has built an expression e of a given type t, one can define a constant c to hold that expression as: Definition c : t := e. For instance:

The new constant can now be checked, printed or used to build new terms:

Note that computing the value of n does not modify n:

Note that Coq does not always need that we give the type of an expression. It can often infer it:

Note that we cannot check the type of the notation && (Fail is a command that succeed when the body fails, we will come back to this).

... but we can print its definition:

On the other hand, && is defined as an infixed notation for andb, that is, for any boolean expression x and y, x && y is a notation for andb x y. In particular, we can check the type of the function which, to booleans x and y, associates x && y:

Compare with the expression below:

Since we can typecheck functions, we can also typecheck expressions involving such functions, which is different from evaluating them:

Now that we have written a function, we can give it a name by using Definition:

Exercise 2:

Define the function nandb which computes the operator NAND.

We will discuss type-checking in more details in forthcoming lectures, but you should already notice that type-checking and evaluation are very different questions. (Even though the type theory of Coq is so powerful that they must be connected.) The following illustrates this fact:

Beware, unlike usual programming languages, the evaluation of && and || is not necessarily *lazy* in Coq. We can actually specify the type of evaluation strategy in variants of Compute to be studied later in the semester.

nat

Coq provides a type nat for natural numbers. By default, typing 0, 1 and any other positive numeric constant gives you a nat. Beware : this is a "unary" encoding (Peano numerals), hence dramatically slow. In order to get access to operations on natural numbers, we load the Arith library (for more informations on the standard library, visit the corresponding section of the reference manual):

nat corresponds to natural numbers considered Peano's natural arithmetic, built from a constant O (the upper-case letter 'o') and a function symbol S for the successor. The use of the usual notation for natural number is a pretty-printing feature:

The constructor S can itself be typed as:

Some operations defined on nat:

• addition +,
• multiplication *,
• euclidean division /,
• modulo x mod y.
• boolean comparisons of numbers : x =? y or x <? y or x <=? y.

We will see later how to perform efficient arithmetical operations (binary encoding) and how to handle negative numbers (type Z).

Exercise 3:

Define the function succ_add of two arguments which returns the successor of the sum of its two input

Let us know turn our attention to the types and definitions of those operations. Try the following command:

One sees that when asked to print the definition of *, Coq refers to Init.Nat.add. Let's investigate:

Here, we can remark three things:

• the type of Init.Nat.add is nat -> nat -> nat which is to be read nat -> (nat -> nat), that is the type of a function that receives a natural as input and returns a function from nat to <nat as output.
• the definition of Init.Nat.add makes use of a new construction: fix (to define a function recursively) with the {struct n} to indicates that their is an argument, n, that structurally decreases at each recursive call, ensuring that any series of recursive calls will terminate. In fact we will see simpler means to define recursive functions in the following lectures, using the keyword Fixpoint.
• and the use of match ... with | 0 => ... | S n => ... end which allows to define the function to be define by case analysis (actually pattern-matching) on its first argument.

To see the impact of fix, let us try to define add without fix:

In the message The reference addfail was not found in the current environment. addfail refers to the occurrence of addfail in the body of the function definition:
Definition addfail (n m : nat) : nat :=
match n with
| 0 => m
| S p => S **addfail** p m
end.

With using fix or Fixpoint, a function being defined cannot refer to itself.

Exercise 4:

Do the same thing as we did for + with *.

Some observations about recursive functions and inductive types

To end this TP0, we will investigate a little bit how function can be defined by recursion. If an access to recursion, in a way or another, is an essential feature of any programming language, for expressivity purposes, it is a main reason of non-terminating programs. Because Coq aims at being not only a programming language, but also a framework to formalize logic and mathematics, non-termination shall be avoided and the access to recursive definition is constrained. Morally, any fixed point definition should come with a trivial proof of termination, which is the prupose of the {struct n} in the previous example: add terminates because each recursive call involves a strict subterm of the first argument of add: its first argument decreases structurally. Let us consider another example of a recursive function:

Exercise 6:

Define the function fact : nat -> nat which computes the factorial by adapting the above examples. Then do: Check fact. Compute (fact 3). Compute (fact 5). Compute (fact 7). Compute (fact 8). Compute (fact 10). Compute (fact 15). Compute (fact 20). You will see that some of the calls returns erros. Fail to correct that behaviour and have Coq interaction to succeed. (Note that with jscoq, the use of Fail in the case of such a stack overflow does not solve the issue, just erase the problematic cases. The stack overflow is not due to the recursive calls being too numerous, but to the representation of natural numbers. Indeed, we are working with... unary natural numbers... (We will see how to improve this in coming lectures!)

To finish, let us have a look at how the type nat is defined:

In first approximation, we can say that such a declaration will:

• create two new constructors (constants): O and S, that allow to build terms of type nat: O, S O, S (S O), S (S (S O)), etc.
• create a new type nat the elements of which are obtains by using the constructors as specified in the inductive type definition.

In fact, the Inductive type definition does more (remember the axioms of Peano's arithmetic):

• notably ensuring that the constructors are injective (here, S t = S u => t = u for any t and u of type nat) and that two terms starting with different constructors are never equal (S t <> O).
• and last but not least, generating induction principles for type nat.

Notice that when giving this definition to Coq, the system answers:

• nat is defined
• nat_rect is defined
• nat_ind is defined
• nat_rec is defined
• nat_sind is defined

These are nat induction principles which are automatically generated by Coq when defining a new inductive type. Let us just print nat and check the type of the principle nat_ind

If you wish, you can print nat_ind and try to make sense of it. But notice that it is not until few weeks that we will consider this.

Exercise 7:

Define the function pred : nat -> nat which, when given O returns O and when given some successor number (S n) returns its predecessor, that is n.

Exercise 8:

Define the function even : nat -> bool which returns true if its input is even and false if it is odd.

A first theorem

To end, we finish with a first (extremely simple!) theorem.

Theorem is a slight variant of a Definition. (The difference will be analyzed in the second part of the semester.) It simply declares a constant predsucc of type forall n: nat, pred (S n) = n. (that means that there are still plenty of other type constructions to discover!) and instead of providing a term of that type, it enters the interactive mode, aiming and building a proof (or a term). This interactive mode is shown on the top right of the screen, showing the goal that must be proved:
_____________________________________(1/1)
forall n : nat, pred (S n) = n

Here the proof is simply by computation:

• it first introduces n in the context, assuming a generic nat n (as when we declare "let n be a natural number")
• it then uses a proof tactic simpl, which reduces pred (S n) to n and
• finishes the proof by reflexivity, noting that in the left and right hand side of the equality there are identical terms.