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:
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:
- 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.
- 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:
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:
then another popup window should appear telling you that:
Prop : Type
and if you type-check Type you should be told that:
Type : Type
and henceforth Type : Type and Type : Type, 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 : Type : Type : .... 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:
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:
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:
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.
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 and Matita complains. Why, given I stated that there was an ascending hierarchy of predicative universes above Prop of the form Type : Type : Type : .. ? 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 : Type, 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.