The Nuprl system is a proof assistant which helps users create formal proofs
of theorems. Within the Nuprl language, one defines mathematical objects and
then states theorems to prove about these objects. The language which Nuprl
uses is typed; that is, every mathematical object is explicitly required
to have a type.
In order to prove a theorem which has been entered into Nuprl, the user
specifies a sequence of tactics to apply. A tactic is a strategy for
proving the current goal given the current hypotheses. The user specifies
a tactic to apply and the tactic runs on the current goal and hypotheses to
create a set of new subgoals. The subgoals created are labeled as "main",
"aux" for auxiliary or "wf" for wellformedness (this is a subset of the
"aux" subgoals). Intuitively, auxiliary
subgoals prove supplementary facts which are needed for the main branch of
the proof to hold and wellformedness subgoals prove that the statements made
respect the type information given for the theorem (this is necessary because
Nuprl uses a typed language). The user then specifies tactics to use to
prove the new subgoals. This process is repeated until every subgoal is
proved, in which case the entire theorem is proved.
Nuprl also has objects called conversions which can be used to rewrite
clauses or parts of clauses. Conversions are rewrite rules that take a
term and rewrite it to an equivalent term. These may be used to manipulate
hypotheses to facilitate matching. Once a conversion has been defined,
tactics are used to run these conversions and perform the actual rewriting.
The user often knows a sequence of tactics that they wish to apply,
such as knowing that once they apply tactic T they want to apply tactic
"Auto" to the auxiliary subgoals in order to prove them automatically as they
will be simple enough to prove in this manner (this occurs often). Nuprl
allows the user to combine the application of tactics, for example by using
the "THEN" tactic which takes two tactics as arguments, one to apply first
to the current goal and the second to apply to all of the generated subgoals.
The only subgoals which are shown are those that remain to be proved after
all of the listed tactics are run one the specified subgoals.
Nuprl allows the user to make reference to previously proved theorems, or,
as Nuprl refers to them, lemmas. A lemma is invoked by using the name under
which the theorem was proved as an argument to a tactic that acts on lemmas.
the formal statement of the lemma does not need to be given again. Similarly,
mathematical objects such as functions do not need to be defined within a
proof but rather are defined outside of proofs and given names. In order to
use the definition of such an object, one uses the name under which it was
defined as an argument to a relevant tactic.
