next up previous contents index
Next: Commands Needed for Up: Proofs Previous: Proofs

Structure of Proofs

A proof in Nuprl may be thought of as a tree . Associated with each node of the tree is a sequent  and, if the node is not a leaf, a rule. A sequent is in turn composed of a numbered list of hypotheses and a goal. The children of a node are uniquely determined by the sequent and rule of that node. If no rule is present, or if the rule is incorrect or not applicable, the node has no children; otherwise, the children correspond to the subgoals  generated by the application of the rule to the sequent. Note the departure from conventional usage; a proof need not be complete.

The following example from a Nuprl session was obtained by using the command view example to create a window for the theorem object example and then using the refinement editor,   or red  for short, to navigate through the proof tree.

|EDIT THM example                     |                                         
|# top 1 1                            |                                         
|1. x:int                             |                                         
|2. y:int                             |                                         
|>> z:int->(x*(y+z)=x*y+x*z in int)   |                                         
|                                     |                                         
|BY intro                             |                                         
|                                     |                                         
|1# 1. x:int                          |                                         
|   2. y:int                          |                                         
|   3. z:int                          |                                         
|   >> (x*(y+z)=x*y+x*z in int)       |                                         
|                                     |                                         
|2# 1. x:int                          |                                         
|   2. y:int                          |                                         
|   >> int in U1                      |                                         

Displayed in the window above is the sequent to be proven, or main  goal, associated with the current node, the rule of the node (preceded by BY), and the sequents corresponding to the two children of the node. This is the way that the system displays a proof tree in a theorem window; it shows a sequent, the rule  applied to it (if any), and the immediate subgoals. The location of the node in the tree is given by the header, top 1 1 in this case; this means that the node is the first child of the first child of the root of the proof tree. The sign ``#'' indicates that the status   of the subproof is incomplete . Other possible statuses are: `` -'' for bad , meaning that some descendant (leaf) has an incorrect rule application, or that the main goal was not acceptable; ``?'' for raw , which is the status of the proof before the main goal has been parsed; and ``*'' for complete , which indicates that the subproof has been finished.

One usually visualizes a tree as having its root at the top (or bottom) with the branches going downward (upward). In Nuprl , however, a proof tree should be viewed  as lying on its side, with the root at the left and with the first child of a given node being at the same height as its parent, and having its siblings below it. Keeping this in mind will make the commands for moving around in proof trees easier to remember.

next up previous contents index
Next: Commands Needed for Up: Proofs Previous: Proofs

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