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 ` mark`ed 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

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

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

Thu Sep 14 08:45:18 EDT 1995