Next: Examples from Introductory Up: Proofs Previous: Structure of Proofs

# Commands Needed for Proofs

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.)

Next: Examples from Introductory Up: Proofs Previous: Structure of Proofs

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995