What follows is an excerpt of a sample lesson on one-to-one correspondence. The full lesson may be found in the appendix. Because of space limitations here, we must elide some of the material, and show only a few pages of it. The starting point for this lesson is the following documentation object, which is mostly informal text with formal mathematical notation embedded.
From here, the reader continues to a discussion of inverse functions:
The various references to definitions and theorems are special links that show the actual content of the proofs and definition objects they refer to, rather than being entered as part of the text. Through these links the further content of the objects may be accessed on demand. The lesson continues with a discussion of bijections and the possibility of using them to define the concept of one-to-one correspondence; we skip that page here and move on to the discussion of the equivalence of the two approaches to defining one-to-one correspondence.
When the user clicks on the theorem references, either the formal proof or an informal gloss of it is viewed. Here is a gloss of the last proof mentioned.
The purpose of this gloss is informally imitate the main content of the formal proof, to which the reader may refer if further detail or resolution of ambiguity in the gloss is desired. Note that, as usual in Nuprl, the mathematical expressions are formal, rather than simply text, and so their definitions can be followed, and the way these abstract terms happen to be displayed is easily changed.
Now, let us turn to the formal proof. Proofs in Nuprl are trees of assertions, each of which is entailed by its children, or subgoals. There are two main modes for viewing Nuprl's formal proofs; one may either view the whole proof in a compact notation, or one may ``walk'' the proof tree, focusing on one inference step at a time.
There are a number of formats for these compressed representations of whole proofs; the one we shall use here shows the subproofs underneath the goal inferred from them, indenting them if there is more than one subproof.
In this proof format, any numbered assumptions that are the same for the child as for the parent are not shown again; this simplifies the reading.
Now, let us see what it's like to focus on the proof one inference at a time. The top inference looks like this:
The ``* top'' indicates that the proof is complete and that this is the top of the proof tree. The goal is followed by the tactic used for the inference, and the numbered list of subgoals automatically generated from the goal and the tactic. The inference step shown here is typical of the top of a proof; it break down the goal into the obvious assumptions and conclusion, and makes explicit the types of the variables used in the goal. If the user wishes to see the proof of a subgoal, clicking on it will show the inference step leading it from its subgoals.
The ``* top 1'' indicates that the proof of this goal is complete, and also indicates its location within the tree of inference steps, namely, the first subgoal below the top of the proof. This step corresponds to splitting the conclusion into the two conjuncts after expanding its definition; the subgoals are numbered. The user would simply continue reading down the various branches of the proof until a goal with no subgoals is reached, or until he or she is satisfied.
It would take too much space here to walk the whole proof, so we will
just show a couple other inference nodes.
Here is the formal step which, in the gloss above, was expressed as
trying to show that
f(a1) = f(a2) a1 = a2
by first applying g to both sides of the premise.
The subgoal differs from the goal simply by actually performing this application to the appropriate assumption. Notice that all the assumptions in force at each point in the proof are explicitly shown when walking the proof. Proceeding down to the proof of the new subgoal:
This goal is proved, as was glossed above, simply by rewriting assumption 8 to a1 = a2, as is justified by assumption 5. This would generate a new subgoal in which the conclusion appears as an assumption, which the system recognizes as trivially justified, so there are no more subgoals below this point.