Basic logic and proof, part I

In this article and those immediately following we will begin by using Matita to prove some basic theorems from (intuitionistic) propositional logic.  This will set the stage as an introduction to Matita’s logic, it’s syntax for writing proof scripts and Matita’s selection of tactics (programs that transform proof states).

Open Matita by invoking $MATITA_HOME/matita/matita.opt from a command line.  A window should appear on your screen with three subpanes: one on the left and two stacked vertically on the right.  The pane in the top right should contain the Matita logo, the pane beneath it a text area for useful error and log messages, and the pane on the right should be a tabbed editor pane containing a default comment.

First, save the currently unnamed new file that Matita has created by clicking File > Save As.  Place it in $SCRIPTS_HOME, with the file extension .ma, calling it something suggestive, e.g. lesson2.ma.

In the editor window, delete the default comment that Matita has inserted.  Matita’s style of comments follow the Standard ML and OCaml convention of being bracketed with the lexical tokens (* and *).  Unlike some other programming languages, but following the ML tradition, Matita does not have dedicated line comments.

At the top of the file, insert the following line:

include "basics/logic.ma".

The trailing fullstop (“period” for Americans) is not optional.

Save the file with Ctrl+S and then hit Ctrl+Alt+Page Down or press the button at the top of the Matita window with a downarrow on it.  If the root file has been correctly created and saved in $SCRIPTS_HOME Matita will proceed to whir into life, otherwise will fail with an error message in the bottom right hand pane informing you that the system cannot find basics/logic.ma.   If this happens, return to the previous article and reread the section on the creation of the root file towards the end. On the other hand, if Matita is successful, two things will happen:

1. The bottom righthand pane will spit out numerous informative messages, telling you that the system is (recursively) typechecking and including basics/logic.ma and its dependencies.
2. The first line of the editor pane will turn a light shade of blue.  Further, you will no longer be able to edit any editor line that is highlighted with this blue colour—the lines have become “locked” and persist in a read only state.  To edit lines that have been locked, you must tell the system to retract them by hitting Ctrl+Alt+Page Up to retract a single line, or Ctrl+Alt+Home to retract everything in the current file.

Locked lines in the editor pane signify Matita’s acceptance (and the resulting system state update) of the line.

What has including basics/logic.ma done? The file is a part of Matita’s standard library, containing definitions and lemmas that Matita (and you) need to perform basic logical reasoning.  Matita has now processed the file, checking that every definition and lemma within it is type correct, and added those definitions and lemmas to its working environment.  If you now type:

check True.

in your file and hit Ctrl+Alt+Page Down, a new window should pop up with type information about the constant True. This window should tell you that:

True : Prop

(to be read as “in Matita’s current working environment, the term True can be given the type Prop”).

What is Prop? Prop (short for Proposition) is an impredicative sort (in fact, the only impredicative sort in Matita’s hierarchy). Prop is intended as the type of logical propositions. The statements of all lemmas and theorems within Matita must be in type Prop.

Sorts are types of types. It is important to realise that every well-formed term in Matita can be assigned a type and that every type is also a term of the underlying type theory that Matita implements. As a result, if you type the following in your editor window:

check Prop.

then another popup window should appear telling you that:

Prop : Type[0]

and if you type-check Type[0] you should be told that:

Type[0] : Type[1]

and henceforth Type[1] : Type[2] and Type[2] : Type[3], and so on.

Here the Type[n] are referred to as predicative sorts. What do impredicative and predicative mean? Within (impredicative) Prop we can define propositions as universal quantifications that range over all propositions, including themselves. This circularity makes Prop (hence Matita’s logic) extremely expressive. In predicative sorts this circularity is not possible.

Further, we have already seen that Matita’s predicative sorts are aligned into a hierarchy where Type[0] : Type[1] : Type[2] : .... If we collapsed this hierarchy down into a single predicative sort, Type, where Type : Type, then our type system would be susceptible to Girard’s paradox and consequently inconsistent! Matita’s predicative hierarchy is therefore a means of avoiding inconsistency.

Back to True. In the popup window click on the constant True. The browser page will change to something looking like the following:

inductive True: Prop := I : True.

In basics/logic.ma, True is defined to be an inductive type. True resides in Prop and has a single constructor, I. In Haskell, we’d render True as something like:

data True = I

i.e. a type with a single non-bottom inhabitant.  In actual fact, in Matita, True only has one inhabitant full-stop, due to the fact that every term in Matita’s underlying calculus is guaranteed to be normalising.

Having introduced True we are all set to prove our first lemma in Matita—the simplest possible proof—a proof of True! In your editor pane, type the following:

lemma true: True.

Here, we are telling Matita that we want to prove True. Every (explicit) lemma in Matita must be named, and it’s a good idea to name lemmas something suggestive. Unfortunately, our statement here is so simple that there really isn’t a good name for it, other than true.

In Matita lemma is a keyword instructing the system to typecheck the statement immediately following the colon (here True), make sure it resides in Prop and then open up a goal for us of that type. If we were feeling fancy, we could also have used the theorem or corollary keywords, instead of lemma, to achieve the same ends. Matita makes no semantic check to ensure that our statement is complex enough, or depends on sufficiently many more basic lemmas, to justify being called a theorem; it is entirely up to the user.

Hit Ctrl+Alt+Page Down so that the line above is processed and locked. Matita’s top lefthand pane now changes, opening up a single goal. We are to prove True. We have no assumptions, therefore the proof context above our goal (the part above the dashed line) is empty.

Here, before we proceed, we must talk about what “proof” means in the context of Matita.  In Matita, proving a proposition P is identified with inhabiting P, viewed as a type, with a term from Matita’s underlying dependently typed lambda-calculus. Previously, we saw that there is only one inhabitant of True, the constructor I. Therefore, we are going to “apply” I to close the goal that Matita has opened. Note, in general, when we try to prove things in Matita, we are always working backwards, starting from our goal and attempting to simplify it until we obtain one or more subgoals that can be solved directly. On a new line below the lemma statement, type the following:

@I

Here @ (read: “apply”; as we will see, Matita has a very terse naming style in some respects) is the name of one of Matita’s tactics. Tactics are small programs that transform Matita’s proof state. Here I is the name of the term that we are applying—the argument to @, if you will.

Hit Ctrl+Alt+Page Down so that Matita’s proof state changes. The top lefthand pane should now change to a blank panel, indicating that there are no more goals left to prove. Success! All that remains is to tell the system to perform final checks on the lemma and then index it. Do this with:

qed.

Hit Ctrl+Alt+Page Down so that this line is processed. The bottom righthand pane will spit out some diagnostic information in yellow, before finally stating that a new object has been accepted, i.e. that the proof is complete and that Matita accepts this proof as being legitimate.

Congratulations, you’ve finished your first proof!  All together, your lemma should look like the following:

lemma true: True. @I qed.

A note, now, about terminology. What is the proof here? The tactic application @I is not a proof, but rather a meta-program instructing Matita how to construct the proof. The real proof is the constructor I of the True inductive type, i.e. the term that Matita has constructed that inhabits the type/proposition that we are trying to inhabit/prove. For any lemma, you can view the real proof by typing:

check true.

This will open another popup window with type information about the lemma true. Click true now in this popup window, and you will see the following:

definition true: True := I.

The right hand side of the definition sign (:=), here I, is the real proof that Matita has constructed for the proposition True.

Naturally, for such a simple proof, you do not need to use tactics at all. Matita will accept the following:

definition true: True := I.

just fine as an alternative “proof”. At any point, you can construct proof objects manually by hand, using definitions or recursive functions (which will be properly introduced in a later article). However, when the lemmas that we are trying to prove become more complex, this approach quickly becomes infeasible, and tactics and Matita’s automation features offer an easier approach to constructing proofs.

In the next few articles I hope to pick up the pace somewhat, as you should now be comfortable with starting the system, editing basic proof scripts and type checking definitions.

Troubleshooting

Here are some troubleshooting tips for working with Matita:

• Sometimes it is possible to edit the locked portion of a Matita proof script (i.e. the part that Matita highlights in light blue after processing).  This is a known bug with the GTK libraries.  If this happens, Matita gets confused and will usually not be able to process any more of the proof script.  The solution is to hit Ctrl+Alt+Home to send the cursor back to the top of the proof script, retracting everything, and then start processing again.
• So you try to typecheck Type[4] and Matita complains.  Why, given I stated that there was an ascending hierarchy of predicative universes above Prop of the form Type[0] : Type[1] : Type[2] : .. ?  The simple answer is that I lied (or rather, simplified) and in actual fact this universe hierarchy is not infinite at all.  In fact, it need not be the case that Type[1] : Type[2], as Matita has no inbuilt notion of how this universe hierarchy should be arranged.  With Matita, the user is free to specify the names of universes, design how they are stacked and so on.  Open up $MATITA_HOME/matita/lib/basics/pts.ma to see the default configuration of predicative universes.

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!