Proofs in informal mathematics generally have a linear form; one proceeds by deducing new facts from established ones until the desired result has been reached. Proofs in Nuprl , however, have a structure geared toward top--down development. This means, for example, that facts established earlier in the course of a proof are not immediately available. In this section we discuss this problem and others which arise from the structure of Nuprl proofs.
If in the middle of a proof one discovers that the current subgoal is similar to one proved previously, the pair of tactics mark and copy can be used. As mentioned in the preceding chapter, they are used by running mark as a transformation tactic on the subgoal which is thought to be similar and then running copy as a transformation tactic on the subgoal to be proved. The tactic copy will attempt to reproduce the proof of the marked subgoal, making simple modifications if the subgoals are not identical. Using mark and copy is not, however, a complete solution to the problem; it is often difficult to locate the required subgoal, and it can be time consuming to use the proof editor to get to it even when one has a very good idea of where it is.
Fortunately,
this problem can to a large extent be avoided with
a bit of planning. First, the linear style of informal
mathematics can be approximated using the library
by proving separately, as lemmas,
those things of which it is
anticipated that several uses will be made.
Well--formedness goals, i.e., those of the form
>> T in Ui, are by far the most common
type of duplicated subgoal.
The tactic immediate
can handle a good number of these, but many are
quite nontrivial.
Therefore, it is often wise at the outset to
prove the appropriate
well--formedness theorems for
the basic objects of a theory. For example,
if the constructive reals, R, and addition of
real numbers have been defined then the theorems
>> R in U1
>> All x,y:R.(x+y in R)
should be proved. If one is building a reasonably large theory then a much better solution is to define the basic objects of the theory to be extractions from theorems, for then such well--formedness subgoals can be handled automatically. This is discussed in more detail in the next section.
There is no ``thinning'' rule in Nuprl , i.e., a rule which would allow one to remove hypotheses from a goal. This means that it can be difficult for a tactic to assemble a proof in a bottom--up fashion; an already constructed proof cannot be used to prove a goal with the same conclusion unless the hypothesis lists are identical. A solution to this is to arrange things so that what are constructed bottom--up are tactics, not proofs. This was the approach taken in the writing of the term--rewriting package described in chapter 9. A function which rewrites a term t produces not a proof of t=u in T, for some u, T, but u and a tactic which can be applied to goals of the form >> t=u in T. This approach also provides some flexibility with respect to the containing type T.
We conclude this section by making a few points of a more minor nature. First, if in the middle of a proof one realizes that a particular unproven fact will be required several times in the subproof, the sequence rule, seq, can be used to get it into the hypothesis list. If one is reasonably careful in choosing what lemmas to prove, however, the need for this use of the sequence rule does not appear to arise too often. Second, it is a good idea to be attentive to the timing of elim's. Often a considerable amount of work can be saved by doing them before other branching of the proof occurs. Also, an elim involves a substitution in the conclusion; since this substitution is not done in the hypotheses following the eliminated hypothesis, it may be desirable to do eliminations before the left part of a function type is moved into the hypothesis list via an introduction. Third, one should try to arrange things so that the hypothesis list does not become unnecessarily large, especially when writing tactics. For example, if one wants to use an instantiation of a universally quantified theorem, using the lemma rule and then doing the appropriate number of eliminations will give as many extra hypotheses as there are universal quantifiers to remove; this can badly clutter up a proof. This can be avoided by first sequencing in the instantiated form of the lemma. The first goal will be to prove the instantiated version, which is done with the lemma rule, and the second subgoal will have just the desired version of the lemma added to the hypothesis list. Finally, when proving a conjunct A & B both A and B need to be proven, but it might be easier, or necessary, to have A as a hypothesis in the proof of B. If the first step in the proof of A & B is seq A B, then the nontrivial subgoals will be >> A and A >> B.