In this section we give a detailed presentation of how the system is used
to develop a small example. We define the set of natural numbers, define
addition and the relation
and prove two results: that
is transitive and that for all natural numbers **m** and **n**.

When ALF is started two windows appear on screen: the theory window and the
scratch window. Both are split into subwindows by horizontal lines; the theory
window consists of two subwindows and the scratch window of three.
All five subwindows are initially empty. In the initial state only the
basic type theory is known to the system. A theory is developed by making a
sequence of definitions of various kinds. At the top of the scratch window
we find a menu bar. We use the mouse to select (with any mouse button) the
* Define* entry and the following menu appears:

The different entries represent the kinds of objects that can be defined. We
will introduce them one at a time and start to define the set of natural
numbers. So we move the mouse cursor to the entry * Set...* and release
the mouse button. A small text editor window pops up and prompts us to give
the name of the set to be defined. We type the name * N*:

We then strike the Return key (or click on the Ok button) and the pop-up window disappears. Instead the incomplete definition appears in the scratch area, which is the top subwindow of the scratch window:

The first reason that the definition is incomplete is that the type of the
new constant * N* has not yet been specified, as can be seen from its type
. For the moment we ignore the significance of the subscript. It
suffices to know that we have to complete the definition of this
* placeholder*.
We also ignore the empty pair of brackets following the definition.
So we * select* the placeholder, using the left mouse button. It appears
in inverted video
and we click on the right mouse button to get a menu with the available
options:

The choices ** Set** and ** Prop** represent the two predefined ground types
of sets and propositions, respectively. (These two are actually synonyms,
because of the identification of proposition and sets). The two next choices
represent non-dependent and dependent function types. There is also the
possibility to paste a type from some previous definition or to invoke the
text editor. These six items are always present in this menu when the
selection is a type expression. At the end
there is a context-sensitive part, where additional possibilities may appear.
In our case we choose the first item, i.e. ** Set** and the placeholder
is replaced by our choice. You may wonder at this point why we had to make
this choice since we already had indicated that we wanted to define a set.
This will be explained below, when we define .

It is now clear to the system that the name * N* denotes a set. However,
to complete the definition we have to give the constructors of the
set. In this case the constructors are 0 and the successor function. To define
these, we select * N* (left mouse button!) and invoke the
menu of options (right button!):

It should be obvious that the choice should be * Make constructor...*.
The text editor window pops up and we type * 0* as the name of the first
constructor. When the window closes, we see in the scratch area that we
have to give the type of * 0*. We select the placeholder for the type and
invoke the command menu. Now the final, context-sensitive item
N ** Set** is the correct choice
and the situation is the following:

As should be apparent already now, the ALF user does almost all work by selecting items using the left mouse button and invoking the pop-up menu of commands applicable to the selection with the right button. Occasionally some text has to be typed in the pop-up text editor.

We are not yet finished with * N*; there is one more constructor. So we select
* N*, choose * Make constructor...* from the command menu and type
* succ* in the editor. The next step is to give the type of * succ*.
Since it is a function, we should choose a function type from the command
menu. The type of the successor function is non-dependent, so we could use
the (?)? entry. However, if we have a preferred
variable name to use for an unspecified argument to the function, it is
convenient to indicate this now. This will be explained in more detail below,
so let us for the moment accept that it is a good idea to choose the
(x ?)? entry. The text editor prompts us for a name and we type * n*.
There are now two placeholders in the type for * succ* and we select them in
turn and use the pop up menu to set them to * N*. The definition of the
set of natural numbers is now complete:

Before we continue, we consider briefly what one can do in case of mistakes.
Select the type of * succ*, i.e. * (n N)N*. In doing this, note
that the selection is always a complete subexpression. Thus the best way
of selecting the entire type is to click on one of the parentheses, since
the smallest enclosing expression is then the entire type. Now invoke the
pop up menu and choose * Clear*. The type is replaced by a placeholder and we
may start again to give the type. To do this, we use another
method: We * double-click* on the place-holder and the text editor pops up.
We may now give the entire type (using colon for ): * (n:N)N*.
This is a general feature; by double-clicking when selecting, the text editor
pops up and one may edit the expression as text. Of course, this may produce
a syntactically incorrect
expression. In that case, one gets an error message and may open the
editor again to correct the error.

The definition of * N* is now complete. We select it (click on *
N*) and invoke * Move-to-theory* from the pop-up menu. The
definition disappears from the scratch area and appears instead in the
lower half of the theory window. Completed definitions should be
moved to the theory. If it is necessary to change an already completed
definition one has to move it back to the scratch area first by
selecting it and choosing * Move-to-scratch*. If necessary multiple
definitions have to be selected (* shift left-button*) and moved at
once.

As our next step, we define the constants * 1* and * 2* as abbreviations
or, in ALF terminology, * explicit constants*. To do this, open the
* Define* menu and choose * Explicit constant...*. When prompted
for the name, we answer * 1* and the result in the scratch area is

Both the type and the value of this constant have to be defined. We may start
with either. We choose the type, so we select this placeholder and find
the choice * N* in the pop-up menu. Next, we select the value placeholder
and find * succ* in the menu. Choosing this will have the effect

i.e., a new placeholder is inserted for the argument to * succ*. The
type-checker of ALF has realized that if * 1* is to be a natural number,
it cannot be * succ* itself, but rather * succ* applied to a natural
number. We complete the definition by selecting the remaining placeholder and
choosing * 0* from the menu. Here we can also note that in the menu we are
also offered the choice * 1 N*, which would give the circular
definition * 1 succ(1) N*. If this choice is attempted, an
error message results. We see from this example that the context-sensitive
choices offered are somewhat roughly computed and may not always be
possible to select. In a similar way we define * 2* as * succ(1)*.

We go on to define addition. This can be done by a pair of recursive equations
with case analysis on one of the arguments. In ALF terminology,
this is an * implicit constant*. We note here also that the present version
does not admit infix operators, so we prefer the name * plus*. The first
step is to choose * Implicit constant...* from the * Define* menu
and reply with this name when prompted. The next step is to give the type
of the constant. We choose to do this with the text editor (double-click!):

To fill in the definition, we select the name * plus* and choose
* Make pattern* from the menu. A defining equation with a placeholder as
right-hand side appears. However, we cannot fill in this placeholder yet.
We want to do case analysis on the first argument (the choice of the first
rather than the second is arbitrary), so we select the parameter * m*
in the left-hand side and invoke * Make pattern* again. The equation is
split in two, one for each possible constructor form of * N*. Now
the right hand sides of the equations can be easily filled in, by a sequence of
selections and choices from the pop-up menu.

We have defined * plus* by * pattern-matching* on its
first argument. In such definitions, we allow recursive calls. To ensure
that a recursive definition leads to a well-defined function it is necessary that
there is an argument position in which the recursive call has a
* structurally smaller* argument. In the case of * plus*, the first
argument has this property. ** The present version of ALF does not enforce
this condition**. It is thus possible in ALF to make meaningless recursive
definitions, such as * f(x) = f(x)*. The user must manually check that
recursive definitions are well-formed.

We may now move our completed definitions to the theory and go on to define
* Leq*, the relation ``less than or equal to'' on * N*. For any
two natural numbers * m* and * n*, * Leq(m,n)* is a proposition or,
equivalently, a set. The ALF action to define this is therefore to choose
* Set...* from the * Define* menu and choose the name * Leq* when
prompted by the text editor. This leaves us in the situation

and we now see why we have to give the type of * Leq* also in the
* Set...* case. * Leq* is not a set itself; rather it is a function
that given two natural numbers produces a set. We say that * Leq* is
a * family of sets*. So we may double-click on the
placeholder for the type and type * (m,n:N)Set*.
We note that we have our first example of a * dependent* set;
for each choice of * m* and * n* we have a distinct set (proposition),
whose elements are the proofs of the proposition. Of course, this will mean
that * Leq(2,1)* will have to be defined to be empty, while * Leq(1,2)*
will be * inhabited*. Next we have to give the constructors. There are
many ways to define * Leq*. A convenient one is an * inductive*
definition: we have * Leq(0,n)* for any * n* and also that
* Leq(succ(m),succ(n))* if * Leq(m,n)*. These two cases will give
the constructors of the set. We have to invent two names for the two cases
and define the constructors as before:

To help understand this definition, we can check that * leq_0(1)* is a proof
(element) of * Leq(0,1)* and * leq_succ(0,1,leq_0(1))* a proof of
* Leq(1,2)*. As a more interesting example, we now prove that * Leq*
is transitive. This theorem is represented by the set
* (m,n,k:N; p:Leq(m,n); q:Leq(n,k))Leq(m,k)*. To prove it, we have to
define a constant * leq_trans* of this type.
Since the theorem involves arbitrary natural numbers, we define this
as an implicit (recursive) constant. The first steps, including the first
* Make pattern*, give the situation

It now seems natural, following the ideas in defining * plus*, to
do pattern matching on one of the natural number arguments. However,
it turns out to be even better to do pattern matching on the * proof*
arguments * p* and * q*. To do this, we first have to move the
definition of the family * Leq* to the theory, since we are not
permitted to do pattern matching on an argument whose type is in the scratch
area. (Such a definition could later be extended with another constructor,
which would invalidate the pattern matching done). After having done this,
we select * p* and invoke * Make pattern*. The following happens:

The two constructors for * Leq* appear in the respective cases, but some
arguments have been replaced by a * wildcard* `_`

. This is
because there is a dependency between the arguments. In the first equation,
the third argument * leq_0(_)* has (according to the typing of
* leq_trans*) type * Leq(m,n)*. On the other hand, according to the
definition of * Leq*, * leq_0(x)* has for any * x* type
* Leq(0,x)*. These two types are now * unified* and ALF is able to
conclude that * m* must be * 0* and that also * x=n*. The latter
is enforced by choosing * n* as argument to * leq_0*. Such inferred
arguments are not displayed by the system but instead shown as a wildcard.
This device maintains the patterns in * linear* form, i.e. no variable
appears more than once.

The first equation can now easily be completed. To do this, we select the
right hand side. Here we note a fact that we have not mentioned before.
The small bottom subwindow of the scratch window displays the type of the
selection, in this case * Leq(0,k)*. An element of this type is obvious: it
is * leq_0(k)*, which we construct by choosing * leq_0* from the
pop-up menu. The argument * k* is inferred by the system and filled in
automatically. It remains to define the right hand side of the second
equation. Selecting it we see its type * Leq(succ(m1),k))* at the
bottom of the theory window. We cannot directly give a proof of this;
* leq_succ* requires both its first two arguments to be on successor form.
Thus we do pattern matching on * q*. Now something interesting happens;
only one of the cases appear:

The reason for this is apparent when the situation is analyzed: Since * p*
now has constructor * leq_succ*, * n* cannot be * 0* and thus the
proof * q:Leq(n,k)* cannot have constructor * leq_0*. The type
of the right hand side of the remaining case is * Leq(succ(m1),succ(n))*
and an application of * leq_succ* seems appropriate. We try this and the
right hand side is partly completed to * leq_succ(m,n,?)*, where the
remaining placeholder has type * Leq(m1,n)*. The situation is the following,
where we have opened the pop-up menu to see what is available to us:

We see that we have * p1* and * p* available, which would give us
a term of the required type by a recursive application of * leq_trans*
itself. We make this choice and have to fill in the arguments * p1* and
* p*, which cannot be inferred by the system. This completes the proof and
it remains only to check that the recursive call is on a structurally smaller
argument. This is indeed the case, as the third argument in the recursive
call is on * p1*, which is one of the arguments to the constructor in
the corresponding position on the left hand side.

Finally, we prove the simple result * leq_plus:(m,n:N)Leq(m,plus(m,n))*.
We define this as an implicit constant and do pattern matching on * m*.
This gives us

Selecting the right hand side of the first equation, we find that its type is
* Leq(0,plus(0,n))*. But according to the definition of * plus*,
* plus(0,n)* is * definitionally equal* to * n*, which means that
the required type is the same as * Leq(0,n)*, for which we can easily
find the proof * leq_0(n)*. Similarly, in the second case, ALF
can use the second defining equality for * plus* to compute the type of the
right hand side to * Leq(succ(m),succ(plus(m,n)))* and we can complete the
proof with * leq_succ*, using a recursive call to * leq_plus* as
third argument:

Wed Mar 20 13:05:14 MET 1996