Matita is a dependently-typed proof assistant, an environment for writing and checking mathematical proofs with.  Many such similar systems exist: for example, Coq, Agda, Isabelle, the HOL system and HOL Light.  In fact, Matita’s constructive type theory, the Calculus of Coinductive Constructions, is extremely similar to the type theory implemented in INRIA’s Coq proof assistant, and those already familiar with the Coq system should be able to learn Matita quite rapidly.

Matita is under constant development in the Computer Science Department at the University of Bologna in Emilia-Romagna, Italy (“Matita” means “pen” in Italian, and is also a portmanteau of “Mathematics” and “Italy”).  As a result, though teaching materials exist for the system, they seem to fall into one of two categories:

1. They’re written in Italian,
2. They’re written in English, but are significantly out-of-date, referring to an earlier incarnation of the Matita system.

To date, I believe that there exists no English-language up-to-date tutorial for complete novices to read in order for them to get to grips with writing machine-checked proofs with Matita, hence this series of blog posts (along with my desire to not forget everything that I have learned whilst constantly using the system over the last two years!)

The tutorials will assume a modicum of mathematical sophistication (we are dealing with machine-checked mathematics, after all) as well as familiarity with a statically typed functional programming language such as OCaml, Standard ML or Haskell.  Other than that, I will try to keep the tutorials as simple as is possible.

A final note: these articles are being mostly written off-the-cuff.  It is likely that they will contain typographical errors, terminological mistakes and other embarrassing errors that neither my eyes nor WordPress’s spell checker will pick up before publishing.  Any and all corrections will be gratefully received either in the comments below each article or at my e-mail address: dominic.p.mulligan@gmail.com.

Installing Matita

First, we must install Matita.  Matita currently only works on Linux-based systems and the only hope for using Matita on Windows seems to be through the use of a virtual machine.  For the rest of this tutorial I will also assume that the user is running a Debian-based system with APT installed.  Note that on both Debian and Ubuntu systems there is a package called matita in the standard system repositories.  Do not install this as it will install an out-of-date and incompatible version of the Matita system.

First, prepare your system by installing the required dependencies with APT by issuing the following command at a terminal window:

$ apt-get install ocaml ocaml-findlib libgdome2-ocaml-dev liblablgtk2-ocaml-dev liblablgtkmathview-ocaml-dev liblablgtksourceview-ocaml-dev libsqlite3-ocaml-dev libocamlnet-ocaml-dev libzip-ocaml-dev libhttp-ocaml-dev ocaml-ulex08 libexpat-ocaml-dev libmysql-ocaml-dev camlp5

If you are running the latest Ubuntu release the package liblablgtksourceview-ocaml-dev has been superseded by the liblablgtksourceview2-ocaml-dev package so issue the following alternative command:

$ apt-get install ocaml ocaml-findlib libgdome2-ocaml-dev liblablgtk2-ocaml-dev liblablgtkmathview-ocaml-dev liblablgtksourceview2-ocaml-dev libsqlite3-ocaml-dev libocamlnet-ocaml-dev libzip-ocaml-dev libhttp-ocaml-dev ocaml-ulex08 libexpat-ocaml-dev libmysql-ocaml-dev camlp5

Next, prepare a directory for the Matita sources and binaries to reside and enter it.  I usually install Matita in a subdirectory of my /home directory, but this is not required.  For example, issue the following series of commands:

$ cd ~

$ mkdir Matita

$ cd Matita

Henceforth, I’ll refer to whichever directory you created to install the Matita binaries in as $MATITA_HOME.  Download and unpack a relatively recent version of the Matita development source tarball with the following commands:

$ wget http://matita.cs.unibo.it/sources/matita_130312.tar.gz

$ tar -xzf  matita_130312.tar.gz

In $MATITA_HOME you should now be left with two further subdirectories, matita and components, as well as numerous makefiles and auto-configuration scripts.  Build the configuration script with the following command:

$ autoconf configure.ac > configure

$ chmod +x configure

$ ./configure

All being well, the configure script should spit out its usual blurb, checking for the presence of all required libraries and dependencies, and report success.  Now, build the Matita binaries.  Type:

$ make world

This, all being well, will successfully build the various Matita-related binaries and their optimised counterparts and place them in $MATITA_HOME/matita. Now check for the presence of the optimised Matita binary, matita.opt, in this subdirectory.

Congratulations, you have now successfully built and installed Matita from sources.

Preparing a working directory

Before we start editing proof scripts we must prepare a working directory.  This is straightforward.  Create another directory to place proof scripts in.  This can be anywhere in your file system’s file hierarchy and does not need to be a subdirectory of $MATITA_HOME.  For example:

$ cd ~

$ mkdir ProofScripts

$ cd ProofScripts

I will refer to this directory as $SCRIPTS_HOME henceforth.  In $SCRIPTS_HOME create an empty text file called root with the following command:

$ touch root

With your favourite text editor open root, type in the following line of text, save the file and then close:

baseuri=cic:/matita

Congratulations, you now have a working directory set up and are ready to start proving things!