In the preceding chapter we described
how to create theorem objects and how to
enter the main goal of such an object;
in this section we will talk about the Nuprl
\
commands for viewing and changing
proof trees.
One builds proofs of theorems using red, the refinement editor.
Red is a syntax--directed and rule--driven editor;
the proof is developed by specifying instances of rules, such as
elim and arith, and
the editor ensures
that the rule instances are appropriate and calculates the new subgoals.
The remainder of this section is a tutorial
which develops most of the proof of
>> All x,y:int.Some z:int.
(x<y => z=0 in int) & (~x<y => z=1 in int)
Starting in the command window, type
create t thm top; this command creates the
theorem object and places it in the library.
Now type ml. This activates the ML
subsystem;
Nuprl
indicates this by giving the prompt ML>.
Type `` set_auto_tactic `COMPLETE immediate`;;'' (note
that the quotes are back quotes) and then hit RETURN
.
This has
Nuprl
show the steps of any proof that it automatically constructs
using the auto--tactic immediate,
an ML program which performs simple reasoning automatically.
The ML
subsystem will be discussed later.
Now return to the command mode by typing 
and
type view t to bring up the window:
,----------------------------------------, |EDIT THM t | |----------------------------------------| |? top | |<main proof goal> | '----------------------------------------'
As described in the preceding chapter, enter the main goal; this will result in a window that looks like the following.
,----------------------------------------------------, |EDIT THM t | |----------------------------------------------------| |# top | |>> All x,y:int.Some z:int. | | x<y => (z=0 in int) & ~x<y => (z=1 in int) | | | |BY <refinement rule> | '----------------------------------------------------'
Note the status ; it indicates that the main goal has been successfully parsed and that the proof can proceed. Also note that the statement of the theorem now appears in the library window. Now, the first step of the proof will be to apply an introduction rule. Since a universally quantified formula is, by definition, a dependent function
type, the function--introduction rule is required.
It suffices, however, to enter intro as the rule; the system
will determine from the context exactly which type of introduction
is to be applied.
The rule is entered into an edit window, which can be
brought up in two ways. The first way is to type LONG
\
in order to move the cursor
from the main goal
to `` BY <refinement rule>'' and to then type SEL
SEL
}. The
other way is to position the mouse pointer over `` BY
<refinement rule>'' and then do a mouse SEL
,
i.e., a left--click
on the mouse.
The system displays the following windows.
,-------------------------------,--------------, |EDIT THM t |EDIT rule of t| |-------------------------------|--------------| |# top | _ | |>> All x,y:int.Some z:int. | | | x<y => (z=0 in int) & | | | ~x<y => (z=1 in int) | | | | | |BY <refinement rule> | | '-------------------------------'--------------'
Now type the rule name intro, finishing with a
. In general, a 
causes the entered text to
be processed and, unless certain errors have occurred, removes the
rule window. If the first word of the text was a rule name,
then the text which follows, if any, is checked to make sure that it is
appropriate to the rule, and if it is, the rule is applied and
the resulting subgoals, if any, are displayed.
The proof window is now:
,------------------------------------------------------, |EDIT THM t | |------------------------------------------------------| |# top | |>> All x,y:int.Some z:int. | | x<y => (z=0 in int) & ~x<y => (z=1 in int) | | | |BY intro | | | |1# 1. x:(int) | | >> (All y:int.Some z:int. | | x<y => (z=0 in int) & ~x<y => (z=1 in int)) | | | |2* >> (int) in U1 | | | '------------------------------------------------------'
Nuprl
has generated the two subgoals specified by the
function--introduction rule.
Now try moving the cursor around
using LONG
and LONG
, and note that
it stops at the four major entries of the window. If
a proof window is not big enough to display all the subgoals,
moving the cursor down will force the window to
be scrolled. Note that the status of subgoal 2 above is
``complete''.
This indicates that the auto--tactic
has completely
proven the second subgoal.
Now position the cursor over the first subgoal
and type 
,
or position the mouse pointer over it and
right--click ; either action has the effect
of moving the
theorem window down the proof tree to the indicated subgoal.
Alternatively, one may
type LONG
; this will always
move the window to
the next (in an order to be described later)
unproved leaf of the proof tree.
The window should now look like:
,--------------------------------------------------------, |EDIT THM t | |--------------------------------------------------------| |# top 1 | |1. x:(int) | |>> (All y:int.Some z:int. | | x<y => (z=0 in int) & ~x<y => (z=1 in int)) | | | |BY <refinement rule> | '--------------------------------------------------------'
To strip off another quantifier, proceed as before
(i.e., type LONG
SEL
or position
the mouse pointer and left--click, then enter
the rule intro followed by 
).
Move to the first of the subgoals by typing
LONG
. The current goal is now:
,--------------------------------------------------------, |EDIT THM t | |--------------------------------------------------------| |# top 1 1 | |1. x:(int) | |2. y:(int) | |>> (Some z:int. | | x<y => (z=0 in int) & ~x<y => (z=1 in int)) | | | |BY <refinement rule> | '--------------------------------------------------------'
Using an introduction rule here would require that a value for z be supplied. Since the choice of that value depends on whether or not x<y, a case analysis is required. Enter the following as the rule:
seq x<y | ~x<y
In general, this rule, called the sequence rule, introduces a new fact into the proof. The window below shows the two new subgoals; one is to prove the new fact, and the other is to prove the previous goal assuming the new fact.
,---------------------------------------------------------, |EDIT THM t | |---------------------------------------------------------| |# top 1 1 | |1. x:(int) | |2. y:(int) | |>> (Some z:int. | | x<y => (z=0 in int) & ~x<y => (z=1 in int)) | | | |BY seq x<y | ~x<y | | | |1* 1. x:(int) | | 2. y:(int) | | >> x<y | ~x<y | | | |2# 1. x:(int) | | 2. y:(int) | | 3. x<y | ~x<y | | >> (Some z:int. | | x<y => (z=0 in int) & ~x<y => (z=1 in int)) | '---------------------------------------------------------'
Note that the auto--tactic has proven
the first subgoal.
To see the proof it constructed, move the
window to the first subgoal (LONG
LONG
).
,---------------------------------------------------------, |EDIT THM t | |---------------------------------------------------------| |* top 1 1 1 | |1. x:(int) | |2. y:(int) | |>> x<y | ~x<y | | | |BY arith at U1 | | | |1* 1. x:(int) | | 2. y:(int) | | >> x in int | | | |2* 1. x:(int) | | 2. y:(int) | | >> y in int | '---------------------------------------------------------'
The auto--tactic applied the arith rule
to the subgoal and then proved the
subgoals (using intro). Now go back
to the previous node (i.e., the parent of the current one)
by typing 
, or by positioning the
mouse pointer over the main goal of the window and
right--clicking, and proceed to the second subgoal of that node.
The window now becomes:
,---------------------------------------------------------, |EDIT THM t | |---------------------------------------------------------| |# top 1 1 2 | |1. x:(int) | |2. y:(int) | |3. x<y | ~x<y | |>> (Some z:int. | | x<y => (z=0 in int) & ~x<y => (z=1 in int)) | | | |BY <refinement rule> | '---------------------------------------------------------'
A case analysis on hypothesis 3 above is now required; this is done by entering the rule elim 3.
,---------------------------------------------------------, |EDIT THM t | |---------------------------------------------------------| |# top 1 1 2 | |1. x:(int) | |2. y:(int) | |3. x<y | ~x<y | |>> (Some z:int. | | x<y => (z=0 in int) & ~x<y => (z=1 in int)) | | | |BY elim 3 | | | |1# 1. x:(int) | | 2. y:(int) | | 3. x<y | ~x<y | | 4. x<y | | >> (Some z:int. | | x<y => (z=0 in int) & ~x<y => (z=1 in int)) | | | |2# 1. x:(int) | | 2. y:(int) | | 3. x<y | ~x<y | | 4. ~x<y | | >> (Some z:int. | | x<y => (z=0 in int) & ~x<y => (z=1 in int)) | '---------------------------------------------------------'
Note
the pattern of rule usage---to break down the conclusion
of the goal we use intro, and to break down a
hypothesis we use elim.
We continue by proving the first subgoal. The second,
which is very similar, is left to the reader.
Type LONG
to get:
,---------------------------------------------------------, |EDIT THM t | |---------------------------------------------------------| |# top 1 1 2 1 | |1. x:(int) | |2. y:(int) | |3. x<y | ~x<y | |4. x<y | |>> (Some z:int. | | x<y => (z=0 in int) & ~x<y => (z=1 in int)) | | | |BY <refinement rule> | '---------------------------------------------------------'
It is now possible to specify a value for z, since x<y is a hypothesis. Entering `` intro 0'' as the rule causes z to be instantiated with 0:
,---------------------------------------------------------, |EDIT THM t | |---------------------------------------------------------| |* top 1 1 2 1 | |1. x:(int) | |2. y:(int) | |3. x<y | ~x<y | |4. x<y | |>> (Some z:int. | | x<y => (z=0 in int) & ~x<y => (z=1 in int)) | | | |BY intro 0 | | | |1* 1. x:(int) | | 2. y:(int) | | 3. x<y | ~x<y | | 4. x<y | | >> 0 in (int) | | | |2* 1. x:(int) | | 2. y:(int) | | 3. x<y | ~x<y | | 4. x<y | | >> ((x<y )->(0=0 in int))#((~x<y ))->(0=1 in int) | | | |3* 1. x:(int) | | 2. y:(int) | | 3. x<y | ~x<y | | 4. x<y | | 5. z:(int) | | >> (x<y => (z=0 in int) & ~x<y => (z=1 in int)) in U1 | '---------------------------------------------------------'
The auto--tactic now finishes the proof of this subgoal.
The rest of the proof is left as an exercise. (Use LONG
to
get to the remaining unproved subgoal.)