Introduction to the Coq Software for Type Theory

Coq is a program designed to have type theory, or similar foundational mathematics written into it. You can define functions and objects, and write out proofs. To read this some idea about type theory might be preferable for the theory, but it is not strictly necessary. I here use excerpts from a program I wrote in which I tried to explain Euclidean Geometry as type theory.

First, a quick note : Coq works very much like a programming software, and like programming languages it has several libraries with notations and functions available. If you make a new Coq file it will start out with the library of natural numbers and functions related to them, some basic operations and such. I am not going to use them in these examples, so they are removed.

Also, if anyone is wondering about the name, it comes from French, where the unfortunate assosiations you get in English do not apply.

Now, the first thing you will use both in Coq and in type theory is a type. Type is here defined the same way as in type theory, any term, or object, used is of some type, and of only one type. For example:

Variable Point : Type.

This line defines a type called Point, and we can now create objects with this type. The types defined this way are primitive type, they are not made in relation to anything else.

Second, a dependent type, for example :

Variable LineThrough : Point -> Point -> Type.

Here Linethrough would geometrically be the line segment between two points. Defined this way any LineThrough is created by two points, and depends on these points. In a similar fasion, I define:

Definition Triangle := Point * Point * Point.

Here, a triangle is defined as a collection of three points, which intuitively would be the corners of the triangle. By using this, we can always match a triangle two three points which define this, and often it is more useful to work with the points than the triangle itself.

Another quick note, notice that much like any line of code has to end with ; in Java, in Coq any statement must end with a punctuation mark.

Next, the identity type. Identity types are not a necessity in all type theory, but in my building of geometry it is very useful. It is simply the statement that two terms are equal. Coq has the idea programmed in, so it is easy define. Note that an identity type is only defined on one type. For example:

Definition EqualPoint (P Q : Point) := identity P Q.

Definition is used to rename the identity type. := means that we define the left side a the right side. Inside the parenthesis we clarify that P and Q are of the type Point.

Let us define:

Variable Angle : Type.

We can now create a function:

Variable CreateAngle : Point -> Point -> Point -> Angle.

This will allow us to take three points and map them to an angle. Note that all points here are taken as parameters of the function, and an angle is the result. Also, the variable CreateAngle is actually of the dependent type Point*Point*Point*Angle. Next comes another variable:

Variable AngleSym : (forall P Q R : Point, EqualAngle (CreateAngle P Q R) (CreateAngle P R Q)).

This one has more in common with a definition or axiom from our understanding of mathematics, but is here a variable or a conversion rule. Now, the only statement made is what is to the right of the last comma, in this case EqualAngle (CreateAngle P Q R) (CreateAngle P R Q)

Everything to the left are requirements for this statement to apply. As you might guess, forall means for all, and after that we define three points P, Q, R. CreateAngle is the same function as earlier, note that the points are simply written after the name of the function with no parenthesis. AngleSym tells us that for any three points, it does not matter in which order you put the two last points in the CreateAngle function, the two terms are equal. This is not true for changing the point P, the first is here intuitively the point at the base of the angle, and changing it may change the angle.

Next I am going to define a ray, so we may look at a slightly more complicated version of such a variable :

Variable Ray : Type.

Variable CreateRay : Point -> Point -> Ray.

Variable StartingPointRay : Ray -> Point.

Definition EqualRay (R S : Ray) := (identity R S).

The startingpoint of the ray is obviously exactly what it seems to mean. Now, look at this variable:

Variable StartingPointRayDef : (forall R : Ray, forall P Q : Point, forall p_q_makeR : EqualRay R (CreateRay P Q), EqualPoint P (StartingPointRay R)).

This one is a little longer, but most of it is obvious, we have any ray and any two points, but another requirement is put in, namely:

forall p_q_makeR : EqualRay R (CreateRay P Q)

The first part is just a name of the requirement and is not important, what the other part states is that the ray R is equal to the ray made by P and Q. With this we can add requirements beyond just what type the different objects should have, and only if this statement is true do we have:

EqualPoint P (StartingPointRay R)

That is to say that P is the starting point of the R if R equals CreateRay P Q.

And that is the basic of writing axioms, functions and types in Coq. Next time I will write about how to prove statements in Coq relying only on previously defined types and variables.